SUMO   View all facts   Glossary   Help

Entity > Abstract > Class > Relation > Function > BinaryFunction > MereologicalSumFn

MereologicalSumFn
subject			fact

MereologicalSumFn	documentation (MereologicalSumFn ?OBJ1 ?OBJ2) denotes the Object consisting of the parts which belong to either ?OBJ1 or ?OBJ2
	has axiom (<=> (instance ?OBJ SelfConnectedObject) (forall (?PART1 ?PART2) (=> (equal ?OBJ (MereologicalSumFn ?PART1 ?PART2)) (connected ?PART1 ?PART2))))
	has axiom (=> (and (hole ?HOLE1 ?OBJ) (hole ?HOLE2 ?OBJ)) (forall (?HOLE3) (=> (part ?HOLE3 (MereologicalSumFn ?HOLE1 ?HOLE2)) (hole ?HOLE3 ?OBJ))))
	has axiom (=> (equal ?OBJ3 (MereologicalSumFn ?OBJ1 ?OBJ2)) (forall (?PART) (<=> (part ?PART ?OBJ3) (or (part ?PART ?OBJ1) (part ?PART ?OBJ2)))))
	has domain1 Object
	has domain2 Object
	has range Object
	has relatedInternalConcept MereologicalDifferenceFn
	has relatedInternalConcept MereologicalProductFn
	is an instance of BinaryFunction
	is an instance of SpatialRelation
BinaryFunction	is first domain of distributes
	is first domain of identityElement
	is second domain of distributes
Class	is third domain of domain
	is third domain of domainSubclass
Abstract	is disjoint from Physical

Next BinaryFunction: MinuteFn    Up: BinaryFunction, SpatialRelation    Previous BinaryFunction: MereologicalProductFn