and (and)
The truth-functional connective of conjunction.
Ontology
SUMO / STRUCTURAL-ONTOLOGYClass(es)
Coordinate term(s)
<=>
=>
entails
exists
forall
not
or
Type restrictions
and(formula, formula)
Related WordNet synsets
See more related synsets on a separate page.
Axioms (483)
If entity is an immediate instance of class, then there doesn't exist class subclass so that entity is an instance of subclass.
(=>
(immediateInstance ?ENTITY ?CLASS)
(not
(exists
(?SUBCLASS)
(and
(subclass ?SUBCLASS ?CLASS)
(instance ?ENTITY ?SUBCLASS)))))
subclass is a subclass of class if and only if
(<=>
(subclass ?SUBCLASS ?CLASS)
(and
(instance ?SUBCLASS SetOrClass)
(instance ?CLASS SetOrClass)
(forall
(?INST)
(=>
(instance ?INST ?SUBCLASS)
(instance ?INST ?CLASS)))))
If class1 is an immediate subclass of class2, then there doesn't exist class2 class3 so that class1 is a subclass of class3 and class2 is not equal to class3 and class1 is not equal to class3.
(=>
(immediateSubclass ?CLASS1 ?CLASS2)
(not
(exists
(?CLASS3)
(and
(subclass ?CLASS3 ?CLASS2)
(subclass ?CLASS1 ?CLASS3)
(not
(equal ?CLASS2 ?CLASS3))
(not
(equal ?CLASS1 ?CLASS3))))))
If pred1 is a subrelation of pred2 and pred1 %&has number argument(s), then pred2 %&has number argument(s).
(=>
(and
(subrelation ?PRED1 ?PRED2)
(valence ?PRED1 ?NUMBER))
(valence ?PRED2 ?NUMBER))
If pred1 is a subrelation of pred2 and the number number argument of pred2 is an instance of class1, then the number number argument of pred1 is an instance of class1.
(=>
(and
(subrelation ?PRED1 ?PRED2)
(domain ?PRED2 ?NUMBER ?CLASS1))
(domain ?PRED1 ?NUMBER ?CLASS1))
If rel1 is a subrelation of rel2 and rel1() holds, then rel2() holds.
(=>
(and
(subrelation ?REL1 ?REL2)
(holds ?REL1 @ROW))
(holds ?REL2 @ROW))
If pred1 is a subrelation of pred2 and pred2 is an instance of class and class is an instance of inheritable relation, then pred1 is an instance of class.
(=>
(and
(subrelation ?PRED1 ?PRED2)
(instance ?PRED2 ?CLASS)
(instance ?CLASS InheritableRelation))
(instance ?PRED1 ?CLASS))
If the number number argument of rel is an instance of class1 and the number number argument of rel is an instance of class2, then class1 is a subclass of class2 or class2 is a subclass of class1.
(=>
(and
(domain ?REL ?NUMBER ?CLASS1)
(domain ?REL ?NUMBER ?CLASS2))
(or
(subclass ?CLASS1 ?CLASS2)
(subclass ?CLASS2 ?CLASS1)))
If rel1 is a subrelation of rel2 and the number number argument of rel2 is a subclass of class1, then the number number argument of rel1 is a subclass of class1.
(=>
(and
(subrelation ?REL1 ?REL2)
(domainSubclass ?REL2 ?NUMBER ?CLASS1))
(domainSubclass ?REL1 ?NUMBER ?CLASS1))
If the number number argument of rel is a subclass of class1 and the number number argument of rel is a subclass of class2, then class1 is a subclass of class2 or class2 is a subclass of class1.
(=>
(and
(domainSubclass ?REL ?NUMBER ?CLASS1)
(domainSubclass ?REL ?NUMBER ?CLASS2))
(or
(subclass ?CLASS1 ?CLASS2)
(subclass ?CLASS2 ?CLASS1)))
(=>
(equal ?OBJ1 ?OBJ2)
(=>
(and
(equal
?OBJ1
(ListOrderFn
(ListFn @ROW1)
?NUMBER))
(equal
?OBJ2
(ListOrderFn
(ListFn @ROW2)
?NUMBER))
(equal
(ListFn @ROW1)
(ListFn @ROW2)))
(<=>
(holds @ROW1)
(holds @ROW2))))
- if list1 is equal to list2,
- then if list1 is equal to "()" and list2 is equal to "()", then for all number holds: "numberth element of "()"" is equal to "numberth element of "()""
.
(=>
(equal ?LIST1 ?LIST2)
(=>
(and
(equal
?LIST1
(ListFn @ROW1))
(equal
?LIST2
(ListFn @ROW2)))
(forall
(?NUMBER)
(equal
(ListOrderFn
(ListFn @ROW1)
?NUMBER)
(ListOrderFn
(ListFn @ROW2)
?NUMBER)))))
If range of function is an instance of class and "function()" is equal to value, then value is an instance of class.
(=>
(and
(range ?FUNCTION ?CLASS)
(equal
(AssignmentFn ?FUNCTION @ROW)
?VALUE))
(instance ?VALUE ?CLASS))
If rel1 is a subrelation of rel2 and range of rel2 is an instance of class1, then range of rel1 is an instance of class1.
(=>
(and
(subrelation ?REL1 ?REL2)
(range ?REL2 ?CLASS1))
(range ?REL1 ?CLASS1))
If range of rel is an instance of class1 and range of rel is an instance of class2, then class1 is a subclass of class2 or class2 is a subclass of class1.
(=>
(and
(range ?REL ?CLASS1)
(range ?REL ?CLASS2))
(or
(subclass ?CLASS1 ?CLASS2)
(subclass ?CLASS2 ?CLASS1)))
If the values returned by function are subclasses of class and "function()" is equal to value, then value is a subclass of class.
(=>
(and
(rangeSubclass ?FUNCTION ?CLASS)
(equal
(AssignmentFn ?FUNCTION @ROW)
?VALUE))
(subclass ?VALUE ?CLASS))
If rel1 is a subrelation of rel2 and the values returned by rel2 are subclasses of class1, then the values returned by rel1 are subclasses of class1.
(=>
(and
(subrelation ?REL1 ?REL2)
(rangeSubclass ?REL2 ?CLASS1))
(rangeSubclass ?REL1 ?CLASS1))
If the values returned by rel are subclasses of class1 and the values returned by rel are subclasses of class2, then class1 is a subclass of class2 or class2 is a subclass of class1.
(=>
(and
(rangeSubclass ?REL ?CLASS1)
(rangeSubclass ?REL ?CLASS2))
(or
(subclass ?CLASS1 ?CLASS2)
(subclass ?CLASS2 ?CLASS1)))
class1 is disjoint from class2 if and only if
(<=>
(disjoint ?CLASS1 ?CLASS2)
(and
(instance ?CLASS1 SetOrClass)
(instance ?CLASS2 SetOrClass)
(forall
(?INST)
(not
(and
(instance ?INST ?CLASS1)
(instance ?INST ?CLASS2))))))
If and ? are disjoint and rel is a member of "()", then rel is an instance of relation.
(=>
(and
(disjointRelation @ROW)
(inList
?REL
(ListFn @ROW)))
(instance ?REL Relation))
If and ? are disjoint and rel1 is a member of "()" and rel2 is a member of "()" and rel1 %&has number argument(s), then rel2 %&has number argument(s).
(=>
(and
(disjointRelation @ROW)
(inList
?REL1
(ListFn @ROW))
(inList
?REL2
(ListFn @ROW))
(valence ?REL1 ?NUMBER))
(valence ?REL2 ?NUMBER))
If the number number argument of rel1 is an instance of class1 and the number number argument of rel2 is an instance of class2 and class1 is disjoint from class2, then rel1 and rel2 are disjoint.
(=>
(and
(domain ?REL1 ?NUMBER ?CLASS1)
(domain ?REL2 ?NUMBER ?CLASS2)
(disjoint ?CLASS1 ?CLASS2))
(disjointRelation ?REL1 ?REL2))
If the number number argument of rel1 is a subclass of class1 and the number number argument of rel2 is a subclass of class2 and class1 is disjoint from class2, then rel1 and rel2 are disjoint.
(=>
(and
(domainSubclass ?REL1 ?NUMBER ?CLASS1)
(domainSubclass ?REL2 ?NUMBER ?CLASS2)
(disjoint ?CLASS1 ?CLASS2))
(disjointRelation ?REL1 ?REL2))
If range of rel1 is an instance of class1 and range of rel2 is an instance of class2 and class1 is disjoint from class2, then rel1 and rel2 are disjoint.
(=>
(and
(range ?REL1 ?CLASS1)
(range ?REL2 ?CLASS2)
(disjoint ?CLASS1 ?CLASS2))
(disjointRelation ?REL1 ?REL2))
If the values returned by rel1 are subclasses of class1 and the values returned by rel2 are subclasses of class2 and class1 is disjoint from class2, then rel1 and rel2 are disjoint.
(=>
(and
(rangeSubclass ?REL1 ?CLASS1)
(rangeSubclass ?REL2 ?CLASS2)
(disjoint ?CLASS1 ?CLASS2))
(disjointRelation ?REL1 ?REL2))
If and ? are disjoint and rel1 is a member of "()" and rel2 is a member of "()" and rel1 is not equal to rel2 and rel1() holds, then rel2() doesn't hold.
(=>
(and
(disjointRelation @ROW1)
(inList
?REL1
(ListFn @ROW1))
(inList
?REL2
(ListFn @ROW1))
(not
(equal ?REL1 ?REL2))
(holds ?REL1 @ROW2))
(not
(holds ?REL2 @ROW2)))
- if is opposed to ?,
- then for all attr1,attr2 holds:
.
(=>
(contraryAttribute @ROW)
(forall
(?ATTR1 ?ATTR2)
(=>
(and
(equal
?ATTR1
(ListOrderFn
(ListFn @ROW)
?NUMBER1))
(equal
?ATTR2
(ListOrderFn
(ListFn @ROW)
?NUMBER2))
(not
(equal ?NUMBER1 ?NUMBER2)))
(=>
(property ?OBJ ?ATTR1)
(not
(property ?OBJ ?ATTR2))))))
(=>
(exhaustiveAttribute ?CLASS @ROW)
(forall
(?OBJ)
(=>
(instance ?ATTR1 ?CLASS)
(exists
(?ATTR2)
(and
(inList
?ATTR2
(ListFn @ROW))
(equal ?ATTR1 ?ATTR2))))))
is exhaustively partitioned into if and only if is covered by and is disjointly decomposed into .
(<=>
(partition @ROW)
(and
(exhaustiveDecomposition @ROW)
(disjointDecomposition @ROW)))
If attr1 is a subattribute of attr2 and attr2 is an instance of class, then attr1 is an instance of class.
(=>
(and
(subAttribute ?ATTR1 ?ATTR2)
(instance ?ATTR2 ?CLASS))
(instance ?ATTR1 ?CLASS))
If attr1 is an immediate successor attribute of attr2 and entity has an attribute attr2 during time1, then there exists time2 so that time2 is a part of "before time1" and entity has an attribute attr1 during time2.
(=>
(and
(successorAttribute ?ATTR1 ?ATTR2)
(holdsDuring
?TIME1
(property ?ENTITY ?ATTR2)))
(exists
(?TIME2)
(and
(temporalPart
?TIME2
(PastFn ?TIME1))
(holdsDuring
?TIME2
(property ?ENTITY ?ATTR1)))))
If rel(,inst) holds and rel is an instance of function, then "rel()" is equal to inst.
(=>
(and
(holds ?REL @ROW ?INST)
(instance ?REL Function))
(equal
(AssignmentFn ?REL @ROW)
?INST))
phys is an instance of physical if and only if there exist loc,time so that phys is located at loc and phys exists during time.
(<=>
(instance ?PHYS Physical)
(exists
(?LOC ?TIME)
(and
(located ?PHYS ?LOC)
(time ?PHYS ?TIME))))
obj1 is a properPart of obj2 if and only if obj1 is a part of obj2 and obj2 is not a part of obj1.
(<=>
(properPart ?OBJ1 ?OBJ2)
(and
(part ?OBJ1 ?OBJ2)
(not
(part ?OBJ2 ?OBJ1))))
If objecttype is a subclass of substance and object is an instance of objecttype and part is a part of object, then part is an instance of objecttype.
(=>
(and
(subclass ?OBJECTTYPE Substance)
(instance ?OBJECT ?OBJECTTYPE)
(part ?PART ?OBJECT))
(instance ?PART ?OBJECTTYPE))
If obj is an instance of substance and attr is an attribute of obj and part is a part of obj, then attr is an attribute of part.
(=>
(and
(instance ?OBJ Substance)
(attribute ?OBJ ?ATTR)
(part ?PART ?OBJ))
(attribute ?PART ?ATTR))
If atom is an instance of atom, then there exist proton proton,electron electron so that proton is a component of atom and electron is a component of atom.
(=>
(instance ?ATOM Atom)
(exists
(?PROTON ?ELECTRON)
(and
(component ?PROTON ?ATOM)
(component ?ELECTRON ?ATOM)
(instance ?PROTON Proton)
(instance ?ELECTRON Electron))))
(=>
(instance ?ATOM Atom)
(forall
(?NUCLEUS1 ?NUCLEUS2)
(=>
(and
(component ?NUCLEUS1 ?ATOM)
(component ?NUCLEUS2 ?ATOM)
(instance ?NUCLEUS1 AtomicNucleus)
(instance ?NUCLEUS2 AtomicNucleus))
(equal ?NUCLEUS1 ?NUCLEUS2))))
If particle is an instance of subatomic particle, then there exists atom atom so that particle is a part of atom.
(=>
(instance ?PARTICLE SubatomicParticle)
(exists
(?ATOM)
(and
(instance ?ATOM Atom)
(part ?PARTICLE ?ATOM))))
If nucleus is an instance of atomic nucleus, then there exist neutron neutron,proton proton so that neutron is a component of nucleus and proton is a component of nucleus.
(=>
(instance ?NUCLEUS AtomicNucleus)
(exists
(?NEUTRON ?PROTON)
(and
(component ?NEUTRON ?NUCLEUS)
(component ?PROTON ?NUCLEUS)
(instance ?NEUTRON Neutron)
(instance ?PROTON Proton))))
If mixture is an instance of mixture, then there exist pure substance pure1,pure substance pure2 so that pure1 is not equal to pure2 and pure1 is a piece of mixture and pure2 is a piece of mixture.
(=>
(instance ?MIXTURE Mixture)
(exists
(?PURE1 ?PURE2)
(and
(subclass ?PURE1 PureSubstance)
(subclass ?PURE2 PureSubstance)
(not
(equal ?PURE1 ?PURE2))
(piece ?PURE1 ?MIXTURE)
(piece ?PURE2 ?MIXTURE))))
If obj is an instance of corpuscular object, then there exist substance substance1,substance substance2 so that substance1 is made of obj and substance2 is made of obj and substance1 is not equal to substance2.
(=>
(instance ?OBJ CorpuscularObject)
(exists
(?SUBSTANCE1 ?SUBSTANCE2)
(and
(subclass ?SUBSTANCE1 Substance)
(subclass ?SUBSTANCE2 Substance)
(material ?SUBSTANCE1 ?OBJ)
(material ?SUBSTANCE2 ?OBJ)
(not
(equal ?SUBSTANCE1 ?SUBSTANCE2)))))
coll1 is a proper sub-collection of coll2 if and only if
(<=>
(subCollection ?COLL1 ?COLL2)
(and
(instance ?COLL1 Collection)
(instance ?COLL2 Collection)
(forall
(?MEMBER)
(=>
(member ?MEMBER ?COLL1)
(member ?MEMBER ?COLL2)))))
If string is an instance of symbolic string, then there exists character part so that part is a part of string.
(=>
(instance ?STRING SymbolicString)
(exists
(?PART)
(and
(part ?PART ?STRING)
(instance ?PART Character))))
If lang is an instance of animal language and proc is an agent of agent and lang is an instrument for proc, then agent is an instance of animal and agent is not an instance of human.
(=>
(and
(instance ?LANG AnimalLanguage)
(agent ?PROC ?AGENT)
(instrument ?PROC ?LANG))
(and
(instance ?AGENT Animal)
(not
(instance ?AGENT Human))))
If lang is an instance of computer language and proc is an agent of agent and lang is an instrument for proc, then agent is an instance of machine.
(=>
(and
(instance ?LANG ComputerLanguage)
(agent ?PROC ?AGENT)
(instrument ?PROC ?LANG))
(instance ?AGENT Machine))
If lang is an instance of human language and proc is an agent of agent and lang is an instrument for proc, then agent is an instance of human.
(=>
(and
(instance ?LANG HumanLanguage)
(agent ?PROC ?AGENT)
(instrument ?PROC ?LANG))
(instance ?AGENT Human))
If lang is an instance of constructed language, then there exists planning plan so that lang is a result of plan.
(=>
(instance ?LANG ConstructedLanguage)
(exists
(?PLAN)
(and
(instance ?PLAN Planning)
(result ?PLAN ?LANG))))
If process is an instance of dual object process, then there exist obj1,obj2 so that obj1 is a patient of process and obj2 is a patient of process and obj1 is not equal to obj2.
(=>
(instance ?PROCESS DualObjectProcess)
(exists
(?OBJ1 ?OBJ2)
(and
(patient ?PROCESS ?OBJ1)
(patient ?PROCESS ?OBJ2)
(not
(equal ?OBJ1 ?OBJ2)))))
If number is an instance of imaginary number, then there exists real number real so that number is equal to "real*"the square root of "".
(=>
(instance ?NUMBER ImaginaryNumber)
(exists
(?REAL)
(and
(instance ?REAL RealNumber)
(equal
?NUMBER
(MultiplicationFn
?REAL
(SquareRootFn -1))))))
number is an instance of nonnegative real number if and only if number is greater than or equal to and number is an instance of real number.
(<=>
(instance ?NUMBER NonnegativeRealNumber)
(and
(greaterThanOrEqualTo ?NUMBER 0)
(instance ?NUMBER RealNumber)))
number is an instance of positive real number if and only if number is greater than and number is an instance of real number.
(<=>
(instance ?NUMBER PositiveRealNumber)
(and
(greaterThan ?NUMBER 0)
(instance ?NUMBER RealNumber)))
number is an instance of negative real number if and only if number is less than and number is an instance of real number.
(<=>
(instance ?NUMBER NegativeRealNumber)
(and
(lessThan ?NUMBER 0)
(instance ?NUMBER RealNumber)))
If number is an instance of complex number, then there exist real number real1,real number real2 so that number is equal to "(real1+"real2*"the square root of "")".
(=>
(instance ?NUMBER ComplexNumber)
(exists
(?REAL1 ?REAL2)
(and
(instance ?REAL1 RealNumber)
(instance ?REAL2 RealNumber)
(equal
?NUMBER
(AdditionFn
?REAL1
(MultiplicationFn
?REAL2
(SquareRootFn -1)))))))
If function is an instance of unary constant functionquantity, then the number argument of function is an instance of constant quantity and range of function is an instance of constant quantity.
(=>
(instance ?FUNCTION UnaryConstantFunctionQuantity)
(and
(domain ?FUNCTION 1 ConstantQuantity)
(range ?FUNCTION ConstantQuantity)))
rel is an instance of single valued relation if and only if for all ,item1,item2 holds: if rel(,item1) holds and rel(,item2) holds, then item1 is equal to item2.
(<=>
(instance ?REL SingleValuedRelation)
(forall
(@ROW ?ITEM1 ?ITEM2)
(=>
(and
(holds ?REL @ROW ?ITEM1)
(holds ?REL @ROW ?ITEM2))
(equal ?ITEM1 ?ITEM2))))
rel is an instance of total valued relation if and only if there exists valence so that rel is an instance of relation and rel %&has valence argument(s) and - if for all number,element,class holds: if number is less than valence and the number number argument of rel is an instance of class and element is equal to "numberth element of "()"", then element is an instance of class,
- then there exists item so that rel(,item) holds
.
(<=>
(instance ?REL TotalValuedRelation)
(exists
(?VALENCE)
(and
(instance ?REL Relation)
(valence ?REL ?VALENCE)
(=>
(forall
(?NUMBER ?ELEMENT ?CLASS)
(=>
(and
(lessThan ?NUMBER ?VALENCE)
(domain ?REL ?NUMBER ?CLASS)
(equal
?ELEMENT
(ListOrderFn
(ListFn @ROW)
?NUMBER)))
(instance ?ELEMENT ?CLASS)))
(exists
(?ITEM)
(holds ?REL @ROW ?ITEM))))))
If , then rel is an instance of asymmetric relation.
(=>
(and
(instance ?REL BinaryRelation)
(or
(domain ?REL 1 ?CLASS1)
(domainSubclass ?REL 1 ?CLASS1))
(or
(domain ?REL 2 ?CLASS2)
(domainSubclass ?REL 2 ?CLASS2)
(range ?REL ?CLASS2)
(rangeSubclass ?REL ?CLASS2))
(disjoint ?CLASS1 ?CLASS2))
(instance ?REL AsymmetricRelation))
(=>
(instance ?REL AntisymmetricRelation)
(forall
(?INST1 ?INST2)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST1))
(equal ?INST1 ?INST2))))
(=>
(instance ?REL TransitiveRelation)
(forall
(?INST1 ?INST2 ?INST3)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST3))
(holds ?REL ?INST1 ?INST3))))
(=>
(instance ?REL IntransitiveRelation)
(forall
(?INST1 ?INST2 ?INST3)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST3))
(not
(holds ?REL ?INST1 ?INST3)))))
If formula1 increases likelihood of formula2 and "the probability of formula2" is equal to number1 and probability of formula1 provided that formula2 holds is formula2, then number2 is greater than number1.
(=>
(and
(increasesLikelihood ?FORMULA1 ?FORMULA2)
(equal
(ProbabilityFn ?FORMULA2)
?NUMBER1)
(conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
(greaterThan ?NUMBER2 ?NUMBER1))
If formula1 decreases likelihood of formula2 and "the probability of formula2" is equal to number1 and probability of formula1 provided that formula2 holds is formula2, then number2 is less than number1.
(=>
(and
(decreasesLikelihood ?FORMULA1 ?FORMULA2)
(equal
(ProbabilityFn ?FORMULA2)
?NUMBER1)
(conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
(lessThan ?NUMBER2 ?NUMBER1))
If probability of formula1 and formula2 is independent and "the probability of formula2" is equal to number1 and probability of formula1 provided that formula2 holds is formula2, then number2 is equal to number1.
(=>
(and
(independentProbability ?FORMULA1 ?FORMULA2)
(equal
(ProbabilityFn ?FORMULA2)
?NUMBER1)
(conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
(equal ?NUMBER2 ?NUMBER1))
If formula1 is an instance of formula and formula2 is an instance of formula, then formula1 increases likelihood of formula2 or formula1 decreases likelihood of formula2 or probability of formula1 and formula2 is independent.
(=>
(and
(instance ?FORMULA1 Formula)
(instance ?FORMULA2 Formula))
(or
(increasesLikelihood ?FORMULA1 ?FORMULA2)
(decreasesLikelihood ?FORMULA1 ?FORMULA2)
(independentProbability ?FORMULA1 ?FORMULA2)))
If rel is an instance of intentional relation and rel(agent,) holds and obj is a member of "()", then agent is interested in obj.
(=>
(and
(instance ?REL IntentionalRelation)
(holds ?REL ?AGENT @ROW)
(inList
?OBJ
(ListFn @ROW)))
(inScopeOfInterest ?AGENT ?OBJ))
- if list is an instance of list,
- then there exists number1 so that there exists item1 so that "number1th element of list" is not equal to item1 and for all number2 holds: if number2 is an instance of positive integer and number2 is less than number1, then there exists item2 so that "number2th element of list" is equal to item2
.
(=>
(instance ?LIST List)
(exists
(?NUMBER1)
(exists
(?ITEM1)
(and
(not
(equal
(ListOrderFn ?LIST ?NUMBER1)
?ITEM1))
(forall
(?NUMBER2)
(=>
(and
(instance ?NUMBER2 PositiveInteger)
(lessThan ?NUMBER2 ?NUMBER1))
(exists
(?ITEM2)
(equal
(ListOrderFn ?LIST ?NUMBER2)
?ITEM2))))))))
- if class is covered by ,
- then for all obj holds: if obj is an instance of class, then there exists item so that item is a member of "()" and obj is an instance of item
.
(=>
(exhaustiveDecomposition ?CLASS @ROW)
(forall
(?OBJ)
(=>
(instance ?OBJ ?CLASS)
(exists
(?ITEM)
(and
(inList
?ITEM
(ListFn @ROW))
(instance ?OBJ ?ITEM))))))
- if class is disjointly decomposed into ,
- then for all item1,item2 holds: if item1 is a member of "()" and item2 is a member of "()" and item1 is not equal to item2, then item1 is disjoint from item2
.
(=>
(disjointDecomposition ?CLASS @ROW)
(forall
(?ITEM1 ?ITEM2)
(=>
(and
(inList
?ITEM1
(ListFn @ROW))
(inList
?ITEM2
(ListFn @ROW))
(not
(equal ?ITEM1 ?ITEM2)))
(disjoint ?ITEM1 ?ITEM2))))
If list1 is an instance of list and list2 is an instance of list and for all number holds: "numberth element of list1" is equal to "numberth element of list2", then list1 is equal to list2.
(=>
(and
(instance ?LIST1 List)
(instance ?LIST2 List)
(forall
(?NUMBER)
(equal
(ListOrderFn ?LIST1 ?NUMBER)
(ListOrderFn ?LIST2 ?NUMBER))))
(equal ?LIST1 ?LIST2))
If the number number argument of rel is an instance of class and rel() holds, then "numberth element of "()"" is an instance of class.
(=>
(and
(domain ?REL ?NUMBER ?CLASS)
(holds ?REL @ROW))
(instance
(ListOrderFn
(ListFn @ROW)
?NUMBER)
?CLASS))
If the number number argument of rel is a subclass of class and rel() holds, then "numberth element of "()"" is a subclass of class.
(=>
(and
(domainSubclass ?REL ?NUMBER ?CLASS)
(holds ?REL @ROW))
(subclass
(ListOrderFn
(ListFn @ROW)
?NUMBER)
?CLASS))
If "length of list1" is equal to number, then there exists list2 so that list1 starts list2 and "(number+1)" is equal to "length of list2" and ""(number+1)"th element of list2" is equal to item.
(=>
(equal
(ListLengthFn ?LIST1)
?NUMBER)
(exists
(?LIST2)
(and
(initialList ?LIST1 ?LIST2)
(equal
(SuccessorFn ?NUMBER)
(ListLengthFn ?LIST2))
(equal
(ListOrderFn
?LIST2
(SuccessorFn ?NUMBER))
?ITEM))))
list3 is equal to "the list composed of list1 and list2" if and only if for all number1,number2 holds: if number1 is less than or equal to "length of list1" and number2 is less than or equal to "length of list2" and number1 is an instance of positive integer and number2 is an instance of positive integer, then "number1th element of list3" is equal to "number1th element of list1" and ""("length of list1"+number2)"th element of list3" is equal to "number2th element of list2".
(<=>
(equal
?LIST3
(ListConcatenateFn ?LIST1 ?LIST2))
(forall
(?NUMBER1 ?NUMBER2)
(=>
(and
(lessThanOrEqualTo
?NUMBER1
(ListLengthFn ?LIST1))
(lessThanOrEqualTo
?NUMBER2
(ListLengthFn ?LIST2))
(instance ?NUMBER1 PositiveInteger)
(instance ?NUMBER2 PositiveInteger))
(and
(equal
(ListOrderFn ?LIST3 ?NUMBER1)
(ListOrderFn ?LIST1 ?NUMBER1))
(equal
(ListOrderFn
?LIST3
(AdditionFn
(ListLengthFn ?LIST1)
?NUMBER2))
(ListOrderFn ?LIST2 ?NUMBER2))))))
- if list1 is a sublist of list2,
- then there exists number3 so that for all item holds: if item is a member of list1, then there exist number1,number2 so that "number1th element of list1" is equal to item and "number2th element of list2" is equal to item and number2 is equal to "(number1+number3)"
.
(=>
(subList ?LIST1 ?LIST2)
(exists
(?NUMBER3)
(forall
(?ITEM)
(=>
(inList ?ITEM ?LIST1)
(exists
(?NUMBER1 ?NUMBER2)
(and
(equal
(ListOrderFn ?LIST1 ?NUMBER1)
?ITEM)
(equal
(ListOrderFn ?LIST2 ?NUMBER2)
?ITEM)
(equal
?NUMBER2
(AdditionFn ?NUMBER1 ?NUMBER3))))))))
- if list1 starts list2,
- then for all number1,number2 holds: if "length of list1" is equal to number1 and number2 is less than or equal to number1, then "number2th element of list1" is equal to "number2th element of list2"
.
(=>
(initialList ?LIST1 ?LIST2)
(forall
(?NUMBER1 ?NUMBER2)
(=>
(and
(equal
(ListLengthFn ?LIST1)
?NUMBER1)
(lessThanOrEqualTo ?NUMBER2 ?NUMBER1))
(equal
(ListOrderFn ?LIST1 ?NUMBER2)
(ListOrderFn ?LIST2 ?NUMBER2)))))
(=>
(instance ?FUN OneToOneFunction)
(forall
(?ARG1 ?ARG2)
(=>
(and
(domain ?FUN 1 ?CLASS)
(instance ?ARG1 ?CLASS)
(instance ?ARG2 ?CLASS)
(not
(equal ?ARG1 ?ARG2)))
(not
(equal
(AssignmentFn ?FUN ?ARG1)
(AssignmentFn ?FUN ?ARG2))))))
If seq is an instance of sequence function and range of seq is an instance of class, then class is a subclass of integer.
(=>
(and
(instance ?SEQ SequenceFunction)
(range ?SEQ ?CLASS))
(subclass ?CLASS Integer))
- if function is an instance of associative function,
- then for all inst1,inst2,inst3 holds: if the number argument of function is an instance of class and inst1 is an instance of class and inst2 is an instance of class and inst3 is an instance of class, then "function(inst1,"function(inst2,inst3)")" is equal to "function("function(inst1,inst2)",inst3)"
.
(=>
(instance ?FUNCTION AssociativeFunction)
(forall
(?INST1 ?INST2 ?INST3)
(=>
(and
(domain ?FUNCTION 1 ?CLASS)
(instance ?INST1 ?CLASS)
(instance ?INST2 ?CLASS)
(instance ?INST3 ?CLASS))
(equal
(AssignmentFn
?FUNCTION
?INST1
(AssignmentFn ?FUNCTION ?INST2 ?INST3))
(AssignmentFn
?FUNCTION
(AssignmentFn ?FUNCTION ?INST1 ?INST2)
?INST3)))))
(=>
(instance ?FUNCTION CommutativeFunction)
(forall
(?INST1 ?INST2)
(=>
(and
(domain ?FUNCTION 1 ?CLASS)
(instance ?INST1 ?CLASS)
(instance ?INST2 ?CLASS))
(equal
(AssignmentFn ?FUNCTION ?INST1 ?INST2)
(AssignmentFn ?FUNCTION ?INST2 ?INST1)))))
(=>
(and
(closedOn ?FUNCTION ?CLASS)
(instance ?FUNCTION UnaryFunction))
(forall
(?INST)
(=>
(instance ?INST ?CLASS)
(instance
(AssignmentFn ?FUNCTION ?INST)
?CLASS))))
(=>
(and
(closedOn ?FUNCTION ?CLASS)
(instance ?FUNCTION BinaryFunction))
(forall
(?INST1 ?INST2)
(=>
(and
(instance ?INST1 ?CLASS)
(instance ?INST2 ?CLASS))
(instance
(AssignmentFn ?FUNCTION ?INST1 ?INST2)
?CLASS))))
If relation is partial ordering on class, then relation is reflexive on class and relation is an instance of transitive relation and relation is an instance of antisymmetric relation.
(=>
(partialOrderingOn ?RELATION ?CLASS)
(and
(reflexiveOn ?RELATION ?CLASS)
(instance ?RELATION TransitiveRelation)
(instance ?RELATION AntisymmetricRelation)))
relation is total ordering on class if and only if relation is partial ordering on class and relation is trichotomizing on class.
(<=>
(totalOrderingOn ?RELATION ?CLASS)
(and
(partialOrderingOn ?RELATION ?CLASS)
(trichotomizingOn ?RELATION ?CLASS)))
- if relation is trichotomizing on class,
- then for all inst1,inst2 holds: if inst1 is an instance of class and inst2 is an instance of class, then relation(inst1,inst2) holds or relation(inst2,inst1) holds or inst1 is equal to inst2
.
(=>
(trichotomizingOn ?RELATION ?CLASS)
(forall
(?INST1 ?INST2)
(=>
(and
(instance ?INST1 ?CLASS)
(instance ?INST2 ?CLASS))
(or
(holds ?RELATION ?INST1 ?INST2)
(holds ?RELATION ?INST2 ?INST1)
(equal ?INST1 ?INST2)))))
If relation is equivalence relation on class, then relation is an instance of transitive relation and relation is an instance of symmetric relation and relation is reflexive on class.
(=>
(equivalenceRelationOn ?RELATION ?CLASS)
(and
(instance ?RELATION TransitiveRelation)
(instance ?RELATION SymmetricRelation)
(reflexiveOn ?RELATION ?CLASS)))
- if function1 is distributive over function2,
- then for all inst1,inst2,inst3 holds: if the number argument of function1 is an instance of class1 and inst1 is an instance of class1 and inst2 is an instance of class1 and inst3 is an instance of class1 and the number argument of function2 is an instance of class2 and inst1 is an instance of class2 and inst2 is an instance of class2 and inst3 is an instance of class2, then "function1(inst1,"function2(inst2,inst3)")" is equal to "function2("function1(inst1,inst2)","function1(inst1,inst3)")"
.
(=>
(distributes ?FUNCTION1 ?FUNCTION2)
(forall
(?INST1 ?INST2 ?INST3)
(=>
(and
(domain ?FUNCTION1 1 ?CLASS1)
(instance ?INST1 ?CLASS1)
(instance ?INST2 ?CLASS1)
(instance ?INST3 ?CLASS1)
(domain ?FUNCTION2 1 ?CLASS2)
(instance ?INST1 ?CLASS2)
(instance ?INST2 ?CLASS2)
(instance ?INST3 ?CLASS2))
(equal
(AssignmentFn
?FUNCTION1
?INST1
(AssignmentFn ?FUNCTION2 ?INST2 ?INST3))
(AssignmentFn
?FUNCTION2
(AssignmentFn ?FUNCTION1 ?INST1 ?INST2)
(AssignmentFn ?FUNCTION1 ?INST1 ?INST3))))))
- if causes subclass(proc1,proc2) holds,
- then for all inst2 holds: if inst2 is an instance of proc2, then there exists proc1 inst1 so that inst1 causes inst2
.
(=>
(causesSubclass ?PROC1 ?PROC2)
(forall
(?INST2)
(=>
(instance ?INST2 ?PROC2)
(exists
(?INST1)
(and
(instance ?INST1 ?PROC1)
(causes ?INST1 ?INST2))))))
If situation1 holds during time and situation1 entails situation2, then situation2 holds during time.
(=>
(and
(holdsDuring ?TIME ?SITUATION1)
(entails ?SITUATION1 ?SITUATION2))
(holdsDuring ?TIME ?SITUATION2))
If role is an instance of case role and role(arg1,arg2) holds and arg1 is an instance of proc, then arg2 is capable to do proc in role role.
(=>
(and
(instance ?ROLE CaseRole)
(holds ?ROLE ?ARG1 ?ARG2)
(instance ?ARG1 ?PROC))
(capability ?PROC ?ROLE ?ARG2))
If obj exploits agent, then there exists process so that process is an agent of agent and obj is a resource for process.
(=>
(exploits ?OBJ ?AGENT)
(exists
(?PROCESS)
(and
(agent ?PROCESS ?AGENT)
(resource ?PROCESS ?OBJ))))
If obj is partly located in region, then there exists subobj so that subobj is a part of obj and subobj is exactly located in region.
(=>
(partlyLocated ?OBJ ?REGION)
(exists
(?SUBOBJ)
(and
(part ?SUBOBJ ?OBJ)
(exactlyLocated ?SUBOBJ ?REGION))))
If obj is exactly located in region, then there doesn't exist otherobj so that otherobj is exactly located in region and otherobj is not equal to obj.
(=>
(exactlyLocated ?OBJ ?REGION)
(not
(exists
(?OTHEROBJ)
(and
(exactlyLocated ?OTHEROBJ ?REGION)
(not
(equal ?OTHEROBJ ?OBJ))))))
- if person posesses obj,
- then there exists type so that type has the right to perform person and for all process holds: if process is an instance of type, then obj is a patient of process
.
(=>
(possesses ?PERSON ?OBJ)
(exists
(?TYPE)
(and
(holdsRight ?PERSON ?TYPE)
(forall
(?PROCESS)
(=>
(instance ?PROCESS ?TYPE)
(patient ?PROCESS ?OBJ))))))
If time is an instance of time position and agent1 posesses obj during time and agent2 posesses obj during time, then agent1 is equal to agent2.
(=>
(and
(instance ?TIME TimePosition)
(holdsDuring
?TIME
(possesses ?AGENT1 ?OBJ))
(holdsDuring
?TIME
(possesses ?AGENT2 ?OBJ)))
(equal ?AGENT1 ?AGENT2))
If proc1 inhibits proc2, then for all time,place holds: "there exists proc1 inst1 so that inst1 is located at place during time" decreases likelihood of "there exists proc2 inst2 so that inst2 is located at place during time".
(=>
(inhibits ?PROC1 ?PROC2)
(forall
(?TIME ?PLACE)
(decreasesLikelihood
(holdsDuring
?TIME
(exists
(?INST1)
(and
(instance ?INST1 ?PROC1)
(located ?INST1 ?PLACE))))
(holdsDuring
?TIME
(exists
(?INST2)
(and
(instance ?INST2 ?PROC2)
(located ?INST2 ?PLACE)))))))
- if proc1 prevents the occurrence of proc2,
- then for all time,place holds: if there exists proc1 inst1 so that inst1 is located at place during time, then there exists proc2 inst2 so that inst2 is located at place during time
.
(=>
(prevents ?PROC1 ?PROC2)
(forall
(?TIME ?PLACE)
(=>
(holdsDuring
?TIME
(exists
(?INST1)
(and
(instance ?INST1 ?PROC1)
(located ?INST1 ?PLACE))))
(not
(holdsDuring
?TIME
(exists
(?INST2)
(and
(instance ?INST2 ?PROC2)
(located ?INST2 ?PLACE))))))))
class1 subsumes the content of class2 and class2 subsumes the content of class1 if and only if class1 is equivalent to class2.
(<=>
(and
(subsumesContentClass ?CLASS1 ?CLASS2)
(subsumesContentClass ?CLASS2 ?CLASS1))
(equivalentContentClass ?CLASS1 ?CLASS2))
class1 subsumes the content of class2 if and only if for all obj2,info holds: if obj2 is an instance of class2 and obj2 contains information info, then there exists class1 obj1 so that obj1 contains information info.
(<=>
(subsumesContentClass ?CLASS1 ?CLASS2)
(forall
(?OBJ2 ?INFO)
(=>
(and
(instance ?OBJ2 ?CLASS2)
(containsInformation ?OBJ2 ?INFO))
(exists
(?OBJ1)
(and
(instance ?OBJ1 ?CLASS1)
(containsInformation ?OBJ1 ?INFO))))))
obj1 subsumes the content of obj2 and obj2 subsumes the content of obj1 if and only if obj1 is equivalent to obj2.
(<=>
(and
(subsumesContentInstance ?OBJ1 ?OBJ2)
(subsumesContentInstance ?OBJ2 ?OBJ1))
(equivalentContentInstance ?OBJ1 ?OBJ2))
If process expresses the content of prop, then there exists content bearing object obj so that obj contains information prop.
(=>
(realization ?PROCESS ?PROP)
(exists
(?OBJ)
(and
(instance ?OBJ ContentBearingObject)
(containsInformation ?OBJ ?PROP))))
- if prop1 is a sub-proposition of prop2,
- then for all obj1,obj2 holds: if obj1 contains information prop1 and obj2 contains information prop2, then obj2 subsumes the content of obj1
.
(=>
(subProposition ?PROP1 ?PROP2)
(forall
(?OBJ1 ?OBJ2)
(=>
(and
(containsInformation ?OBJ1 ?PROP1)
(containsInformation ?OBJ2 ?PROP2))
(subsumesContentInstance ?OBJ2 ?OBJ1))))
If agent uses obj, then there exists proc so that proc is an agent of agent and obj is an instrument for proc.
(=>
(uses ?OBJ ?AGENT)
(exists
(?PROC)
(and
(agent ?PROC ?AGENT)
(instrument ?PROC ?OBJ))))
If number is an instance of rational number, then there exist integer int1,integer int2 so that number is equal to "int1/int2".
(=>
(instance ?NUMBER RationalNumber)
(exists
(?INT1 ?INT2)
(and
(instance ?INT1 Integer)
(instance ?INT2 Integer)
(equal
?NUMBER
(DivisionFn ?INT1 ?INT2)))))
"the absolute value of number1" is equal to number2 and number1 is an instance of real number and number2 is an instance of real number if and only if
(<=>
(and
(equal
(AbsoluteValueFn ?NUMBER1)
?NUMBER2)
(instance ?NUMBER1 RealNumber)
(instance ?NUMBER2 RealNumber))
(or
(and
(instance ?NUMBER1 NonnegativeRealNumber)
(equal ?NUMBER1 ?NUMBER2))
(and
(instance ?NUMBER1 NegativeRealNumber)
(equal
?NUMBER2
(SubtractionFn 0 ?NUMBER1)))))
If "the ceiling of number" is equal to int, then there doesn't exist integer otherint so that otherint is greater than or equal to number and otherint is less than int.
(=>
(equal
(CeilingFn ?NUMBER)
?INT)
(not
(exists
(?OTHERINT)
(and
(instance ?OTHERINT Integer)
(greaterThanOrEqualTo ?OTHERINT ?NUMBER)
(lessThan ?OTHERINT ?INT)))))
If "the largest integer less than or equal to number" is equal to int, then there doesn't exist integer otherint so that otherint is less than or equal to number and otherint is greater than int.
(=>
(equal
(FloorFn ?NUMBER)
?INT)
(not
(exists
(?OTHERINT)
(and
(instance ?OTHERINT Integer)
(lessThanOrEqualTo ?OTHERINT ?NUMBER)
(greaterThan ?OTHERINT ?INT)))))
- if "the greatest common divisor of " is equal to number,
- then there doesn't exist greater so that greater is greater than number and for all element holds: if element is a member of "()", then "element mod greater" is equal to
.
(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(not
(exists
(?GREATER)
(and
(greaterThan ?GREATER ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?GREATER)
0)))))))
If number is an instance of complex number, then there exist part1,part2 so that part1 is equal to "the real part of number" and part2 is equal to "the imaginary part of number".
(=>
(instance ?NUMBER ComplexNumber)
(exists
(?PART1 ?PART2)
(and
(equal
?PART1
(RealNumberFn ?NUMBER))
(equal
?PART2
(ImaginaryPartFn ?NUMBER)))))
- if "the least common multiple of " is equal to number,
- then there doesn't exist less so that less is less than number and for all element holds: if element is a member of "()", then "less mod element" is equal to
.
(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(not
(exists
(?LESS)
(and
(lessThan ?LESS ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?LESS ?ELEMENT)
0)))))))
If "the larger of number1 and number2" is equal to number, then - number is equal to number1 and number1 is greater than number2
or - number is equal to number2 and number2 is greater than number1
or - number is equal to number1 and number is equal to number2
.
(=>
(equal
(MaxFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(or
(and
(equal ?NUMBER ?NUMBER1)
(greaterThan ?NUMBER1 ?NUMBER2))
(and
(equal ?NUMBER ?NUMBER2)
(greaterThan ?NUMBER2 ?NUMBER1))
(and
(equal ?NUMBER ?NUMBER1)
(equal ?NUMBER ?NUMBER2))))
If "the smaller of number1 and number2" is equal to number, then - number is equal to number1 and number1 is less than number2
or - number is equal to number2 and number2 is less than number1
or - number is equal to number1 and number is equal to number2
.
(=>
(equal
(MinFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(or
(and
(equal ?NUMBER ?NUMBER1)
(lessThan ?NUMBER1 ?NUMBER2))
(and
(equal ?NUMBER ?NUMBER2)
(lessThan ?NUMBER2 ?NUMBER1))
(and
(equal ?NUMBER ?NUMBER1)
(equal ?NUMBER ?NUMBER2))))
- if id is an identity element of function,
- then for all inst holds: if the number argument of function is an instance of class and inst is an instance of class, then "function(id,inst)" is equal to inst
.
(=>
(identityElement ?FUNCTION ?ID)
(forall
(?INST)
(=>
(and
(domain ?FUNCTION 1 ?CLASS)
(instance ?INST ?CLASS))
(equal
(AssignmentFn ?FUNCTION ?ID ?INST)
?INST))))
If int1 is an instance of integer and int2 is an instance of integer, then int1 is not less than int2 or int2 is not less than "(int1+1)".
(=>
(and
(instance ?INT1 Integer)
(instance ?INT2 Integer))
(not
(and
(lessThan ?INT1 ?INT2)
(lessThan
?INT2
(SuccessorFn ?INT1)))))
If int1 is an instance of integer and int2 is an instance of integer, then int2 is not less than int1 or "(int1+2)" is not less than int2.
(=>
(and
(instance ?INT1 Integer)
(instance ?INT2 Integer))
(not
(and
(lessThan ?INT2 ?INT1)
(lessThan
(PredecessorFn ?INT1)
?INT2))))
If set is an instance of finite set, then there exists nonnegative integer number so that number is equal to "the number of instances in set".
(=>
(instance ?SET FiniteSet)
(exists
(?NUMBER)
(and
(instance ?NUMBER NonnegativeInteger)
(equal
?NUMBER
(CardinalityFn ?SET)))))
(=>
(instance ?SUPERCLASS PairwiseDisjointClass)
(forall
(?CLASS1 ?CLASS2)
(=>
(and
(instance ?CLASS1 ?SUPERCLASS)
(instance ?CLASS2 ?SUPERCLASS))
(or
(equal ?CLASS1 ?CLASS2)
(disjoint ?CLASS1 ?CLASS2)))))
(=>
(instance ?CLASS MutuallyDisjointClass)
(forall
(?INST1 ?INST2)
(=>
(and
(instance ?INST1 ?CLASS)
(instance ?INST2 ?INST1))
(exists
(?INST3)
(and
(instance ?INST3 ?CLASS)
(not
(instance ?INST2 ?INST3)))))))
If graph is an instance of graph and node1 is an instance of graph node and node2 is an instance of graph node and node1 is a part of graph and node2 is a part of graph and node1 is not equal to node2, then there exist arc,path so that - arc links node1 and node2
or .
(=>
(and
(instance ?GRAPH Graph)
(instance ?NODE1 GraphNode)
(instance ?NODE2 GraphNode)
(graphPart ?NODE1 ?GRAPH)
(graphPart ?NODE2 ?GRAPH)
(not
(equal ?NODE1 ?NODE2)))
(exists
(?ARC ?PATH)
(or
(links ?NODE1 ?NODE2 ?ARC)
(and
(subGraph ?PATH ?GRAPH)
(instance ?PATH GraphPath)
(or
(and
(equal
(BeginNodeFn ?PATH)
?NODE1)
(equal
(EndNodeFn ?PATH)
?NODE2))
(and
(equal
(BeginNodeFn ?PATH)
?NODE2)
(equal
(EndNodeFn ?PATH)
?NODE1)))))))
If graph is an instance of graph, then there exist node1,node2,node3,arc1,arc2 so that node1 is a part of graph and node2 is a part of graph and node3 is a part of graph and arc1 is a part of graph and arc2 is a part of graph and node2 links arc1 and node1 and node3 links arc2 and node2 and node1 is not equal to node2 and node2 is not equal to node3 and node1 is not equal to node3 and arc1 is not equal to arc2.
(=>
(instance ?GRAPH Graph)
(exists
(?NODE1 ?NODE2 ?NODE3 ?ARC1 ?ARC2)
(and
(graphPart ?NODE1 ?GRAPH)
(graphPart ?NODE2 ?GRAPH)
(graphPart ?NODE3 ?GRAPH)
(graphPart ?ARC1 ?GRAPH)
(graphPart ?ARC2 ?GRAPH)
(links ?ARC1 ?NODE1 ?NODE2)
(links ?ARC2 ?NODE2 ?NODE3)
(not
(equal ?NODE1 ?NODE2))
(not
(equal ?NODE2 ?NODE3))
(not
(equal ?NODE1 ?NODE3))
(not
(equal ?ARC1 ?ARC2)))))
If graph is an instance of directed graph and arc is an instance of graph arc and arc is a part of graph, then there exist node1,node2 so that "the starting node of arc" is equal to node1 and "the terminal node of arc" is equal to node2.
(=>
(and
(instance ?GRAPH DirectedGraph)
(instance ?ARC GraphArc)
(graphPart ?ARC ?GRAPH))
(exists
(?NODE1 ?NODE2)
(and
(equal
(InitialNodeFn ?ARC)
?NODE1)
(equal
(TerminalNodeFn ?ARC)
?NODE2))))
If graph is an instance of tree, then there doesn't exist graph loop loop so that loop is a part of graph.
(=>
(instance ?GRAPH Tree)
(not
(exists
(?LOOP)
(and
(instance ?LOOP GraphLoop)
(graphPart ?LOOP ?GRAPH)))))
(=>
(and
(instance ?GRAPH GraphPath)
(instance ?ARC GraphArc)
(graphPart ?ARC ?GRAPH))
(=>
(equal
(InitialNodeFn ?ARC)
?NODE)
(not
(exists
(?OTHER)
(and
(equal
(InitialNodeFn ?OTHER)
?NODE)
(not
(equal ?OTHER ?ARC)))))))
(=>
(and
(instance ?GRAPH GraphPath)
(instance ?ARC GraphArc)
(graphPart ?ARC ?GRAPH))
(=>
(equal
(TerminalNodeFn ?ARC)
?NODE)
(not
(exists
(?OTHER)
(and
(equal
(TerminalNodeFn ?OTHER)
?NODE)
(not
(equal ?OTHER ?ARC)))))))
graph is an instance of graph circuit if and only if there exists node so that "the beginning of graph" is equal to node and "the end of graph" is equal to node.
(<=>
(instance ?GRAPH GraphCircuit)
(exists
(?NODE)
(and
(equal
(BeginNodeFn ?GRAPH)
?NODE)
(equal
(EndNodeFn ?GRAPH)
?NODE))))
graph is an instance of multi graph if and only if there exist arc1,arc2,node1,node2 so that arc1 is a part of graph and arc2 is a part of graph and node1 is a part of graph and node2 is a part of graph and arc1 links node1 and node2 and arc2 links node1 and node2 and arc1 is not equal to arc2.
(<=>
(instance ?GRAPH MultiGraph)
(exists
(?ARC1 ?ARC2 ?NODE1 ?NODE2)
(and
(graphPart ?ARC1 ?GRAPH)
(graphPart ?ARC2 ?GRAPH)
(graphPart ?NODE1 ?GRAPH)
(graphPart ?NODE2 ?GRAPH)
(links ?NODE1 ?NODE2 ?ARC1)
(links ?NODE1 ?NODE2 ?ARC2)
(not
(equal ?ARC1 ?ARC2)))))
graph is an instance of pseudo graph if and only if there exists graph loop loop so that loop is a part of graph.
(<=>
(instance ?GRAPH PseudoGraph)
(exists
(?LOOP)
(and
(instance ?LOOP GraphLoop)
(graphPart ?LOOP ?GRAPH))))
If part is an instance of graph element, then there exists graph graph so that part is a part of graph.
(=>
(instance ?PART GraphElement)
(exists
(?GRAPH)
(and
(instance ?GRAPH Graph)
(graphPart ?PART ?GRAPH))))
If "the starting node of arc" is equal to node and "the terminal node of arc" is equal to node, then arc is an instance of graph loop.
(=>
(and
(equal
(InitialNodeFn ?ARC)
?NODE)
(equal
(TerminalNodeFn ?ARC)
?NODE))
(instance ?ARC GraphLoop))
If graph1 is a subgraph of graph2 and element is a part of graph1, then element is a part of graph2.
(=>
(and
(subGraph ?GRAPH1 ?GRAPH2)
(graphPart ?ELEMENT ?GRAPH1))
(graphPart ?ELEMENT ?GRAPH2))
- if
- "the value of path" is equal to sum
and - subpath is a subgraph of path
and - arc1 is a part of path
and - the value of arc1 is number1
and - for all arc2 holds: if arc2 is a part of path, then arc2 is a part of subpath or arc2 is equal to arc1
, - then sum is equal to "("the value of subpath"+number1)"
.
(=>
(and
(equal
(PathWeightFn ?PATH)
?SUM)
(subGraph ?SUBPATH ?PATH)
(graphPart ?ARC1 ?PATH)
(arcWeight ?ARC1 ?NUMBER1)
(forall
(?ARC2)
(=>
(graphPart ?ARC2 ?PATH)
(or
(graphPart ?ARC2 ?SUBPATH)
(equal ?ARC2 ?ARC1)))))
(equal
?SUM
(AdditionFn
(PathWeightFn ?SUBPATH)
?NUMBER1)))
- if
- "the value of path" is equal to sum
and - arc1 is a part of path
and - arc2 is a part of path
and - the value of arc1 is number1
and - the value of arc2 is number2
and - for all arc3 holds: if arc3 is a part of path, then arc3 is equal to arc1 or arc3 is equal to arc2
, - then "the value of path" is equal to "(number1+number2)"
.
(=>
(and
(equal
(PathWeightFn ?PATH)
?SUM)
(graphPart ?ARC1 ?PATH)
(graphPart ?ARC2 ?PATH)
(arcWeight ?ARC1 ?NUMBER1)
(arcWeight ?ARC2 ?NUMBER2)
(forall
(?ARC3)
(=>
(graphPart ?ARC3 ?PATH)
(or
(equal ?ARC3 ?ARC1)
(equal ?ARC3 ?ARC2)))))
(equal
(PathWeightFn ?PATH)
(AdditionFn ?NUMBER1 ?NUMBER2)))
- if "the lowest cost path between node1 and node2" is equal to path and "the value of path" is equal to number,
- then for all path2 holds: if path2 is an instance of "the set of paths between node1 and node2" and "the value of path2" is equal to number2, then number2 is greater than or equal to number1
.
(=>
(and
(equal
(MinimalWeightedPathFn ?NODE1 ?NODE2)
?PATH)
(equal
(PathWeightFn ?PATH)
?NUMBER))
(forall
(?PATH2)
(=>
(and
(instance
?PATH2
(GraphPathFn ?NODE1 ?NODE2))
(equal
(PathWeightFn ?PATH2)
?NUMBER2))
(greaterThanOrEqualTo ?NUMBER2 ?NUMBER1))))
- if "the highest cost path between node1 and node2" is equal to path and "the value of path" is equal to number,
- then for all path2 holds: if path2 is an instance of "the set of paths between node1 and node2" and "the value of path2" is equal to number2, then number2 is less than or equal to number1
.
(=>
(and
(equal
(MaximalWeightedPathFn ?NODE1 ?NODE2)
?PATH)
(equal
(PathWeightFn ?PATH)
?NUMBER))
(forall
(?PATH2)
(=>
(and
(instance
?PATH2
(GraphPathFn ?NODE1 ?NODE2))
(equal
(PathWeightFn ?PATH2)
?NUMBER2))
(lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))
If path is a part of graph and graph is not an instance of directed graph, then "the set of paths between node1 and node2" is equal to path if and only if "the set of paths between node2 and node1" is equal to path.
(=>
(and
(graphPart ?PATH ?GRAPH)
(not
(instance ?GRAPH DirectedGraph)))
(<=>
(equal
(GraphPathFn ?NODE1 ?NODE2)
?PATH)
(equal
(GraphPathFn ?NODE2 ?NODE1)
?PATH)))
There don't exist the set of paths that partition graph into two separate graphs path1,the set of minimal paths that partition graph into two separate graphs path2 so that the length of path1 is number1 and the length of path2 is number2 and number1 is less than number2.
(not
(exists
(?PATH1 ?PATH2)
(and
(instance
?PATH1
(CutSetFn ?GRAPH))
(instance
?PATH2
(MinimalCutSetFn ?GRAPH))
(pathLength ?PATH1 ?NUMBER1)
(pathLength ?PATH2 ?NUMBER2)
(lessThan ?NUMBER1 ?NUMBER2))))
If "number unit(s)" is equal to quant and unit is a subclass of quanttype, then quant is an instance of quanttype.
(=>
(and
(equal
(MeasureFn ?NUMBER ?UNIT)
?QUANT)
(subclass ?UNIT ?QUANTTYPE))
(instance ?QUANT ?QUANTTYPE))
(=>
(and
(instance ?REL RelationExtendedToQuantities)
(instance ?REL TernaryRelation)
(instance ?NUMBER1 RealNumber)
(instance ?NUMBER2 RealNumber)
(holds ?REL ?NUMBER1 ?NUMBER2 ?VALUE))
(forall
(?UNIT)
(=>
(instance ?UNIT UnitOfMeasure)
(holds
?REL
(MeasureFn ?NUMBER1 ?UNIT)
(MeasureFn ?NUMBER2 ?UNIT)
(MeasureFn ?VALUE ?UNIT)))))
(=>
(and
(instance ?REL RelationExtendedToQuantities)
(instance ?REL BinaryRelation)
(instance ?NUMBER1 RealNumber)
(instance ?NUMBER2 RealNumber)
(holds ?REL ?NUMBER1 ?NUMBER2))
(forall
(?UNIT)
(=>
(instance ?UNIT UnitOfMeasure)
(holds
?REL
(MeasureFn ?NUMBER1 ?UNIT)
(MeasureFn ?NUMBER2 ?UNIT)))))
quantity is an instance of "the interval from from to to" if and only if quantity is greater than or equal to from and quantity is less than or equal to to.
(<=>
(instance
?QUANTITY
(IntervalFn ?FROM ?TO))
(and
(greaterThanOrEqualTo ?QUANTITY ?FROM)
(lessThanOrEqualTo ?QUANTITY ?TO)))
If number is an instance of real number and unit is an instance of unit of measure, then "the magnitude of "number unit(s)"" is equal to number.
(=>
(and
(instance ?NUMBER RealNumber)
(instance ?UNIT UnitOfMeasure))
(equal
(MagnitudeFn
(MeasureFn ?NUMBER ?UNIT))
?NUMBER))
If the altitude of obj1 is obj2, then there exists top so that the top of obj1 is top and the distance between top and obj2 is height.
(=>
(altitude ?OBJ1 ?OBJ2 ?HEIGHT)
(exists
(?TOP)
(and
(top ?TOP ?OBJ1)
(distance ?TOP ?OBJ2 ?HEIGHT))))
If depth(obj1,obj2,depth) holds, then there exists bottom so that the bottom of obj1 is bottom and the distance between bottom and obj2 is depth.
(=>
(depth ?OBJ1 ?OBJ2 ?DEPTH)
(exists
(?BOTTOM)
(and
(bottom ?BOTTOM ?OBJ1)
(distance ?BOTTOM ?OBJ2 ?DEPTH))))
(=>
(larger ?OBJ1 ?OBJ2)
(forall
(?QUANT1 ?QUANT2)
(=>
(and
(measure
?OBJ1
(MeasureFn ?QUANT1 LengthMeasure))
(measure
?OBJ2
(MeasureFn ?QUANT2 LengthMeasure)))
(greaterThan ?QUANT1 ?QUANT2))))
If point is an instance of time point and point is not equal to positive infinity, then point happen?{s} before positive infinity.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT PositiveInfinity)))
(before ?POINT PositiveInfinity))
If point is an instance of time point and point is not equal to positive infinity, then there exists otherpoint so that otherpoint is between point and positive infinity.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT PositiveInfinity)))
(exists
(?OTHERPOINT)
(temporallyBetween ?POINT ?OTHERPOINT PositiveInfinity)))
If point is an instance of time point and point is not equal to negative infinity, then negative infinity happen?{s} before point.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT NegativeInfinity)))
(before NegativeInfinity ?POINT))
If point is an instance of time point and point is not equal to negative infinity, then there exists otherpoint so that otherpoint is between negative infinity and point.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT NegativeInfinity)))
(exists
(?OTHERPOINT)
(temporallyBetween NegativeInfinity ?OTHERPOINT ?POINT)))
- if proc occurs every time1,
- then for all time2 holds: if duration of time2 is time1, then there exists position so that position is a part of time2 and there exists inst so that inst is an instance of proc during position
.
(=>
(frequency ?PROC ?TIME1)
(forall
(?TIME2)
(=>
(duration ?TIME2 ?TIME1)
(exists
(?POSITION)
(and
(temporalPart ?POSITION ?TIME2)
(holdsDuring
?POSITION
(exists
(?INST)
(instance ?INST ?PROC))))))))
If point is an instance of time point, then there exists time interval interval so that point is a part of interval.
(=>
(instance ?POINT TimePoint)
(exists
(?INTERVAL)
(and
(instance ?INTERVAL TimeInterval)
(temporalPart ?POINT ?INTERVAL))))
If interval is an instance of time interval, then there exists time point point so that point is a part of interval.
(=>
(instance ?INTERVAL TimeInterval)
(exists
(?POINT)
(and
(instance ?POINT TimePoint)
(temporalPart ?POINT ?INTERVAL))))
If situation holds during time1 and time2 is a part of time1, then situation holds during time2.
(=>
(and
(holdsDuring ?TIME1 ?SITUATION)
(temporalPart ?TIME2 ?TIME1))
(holdsDuring ?TIME2 ?SITUATION))
If rel(inst1,inst2) holds during interval and inst1 is an instance of physical and inst2 is an instance of physical, then inst1 exists during interval and inst2 exists during interval.
(=>
(and
(holdsDuring
?INTERVAL
(holds ?REL ?INST1 ?INST2))
(instance ?INST1 Physical)
(instance ?INST2 Physical))
(and
(time ?INST1 ?INTERVAL)
(time ?INST2 ?INTERVAL)))
- if "the beginning of interval" is equal to point,
- then for all otherpoint holds: if otherpoint is a part of interval and otherpoint is not equal to point, then point happen?{s} before otherpoint
.
(=>
(equal
(BeginFn ?INTERVAL)
?POINT)
(forall
(?OTHERPOINT)
(=>
(and
(temporalPart ?OTHERPOINT ?INTERVAL)
(not
(equal ?OTHERPOINT ?POINT)))
(before ?POINT ?OTHERPOINT))))
- if "the end of interval" is equal to point,
- then for all otherpoint holds: if otherpoint is a part of interval and otherpoint is not equal to point, then otherpoint happen?{s} before point
.
(=>
(equal
(EndFn ?INTERVAL)
?POINT)
(forall
(?OTHERPOINT)
(=>
(and
(temporalPart ?OTHERPOINT ?INTERVAL)
(not
(equal ?OTHERPOINT ?POINT)))
(before ?OTHERPOINT ?POINT))))
interval1 starts interval2 if and only if "the beginning of interval1" is equal to "the beginning of interval2" and "the end of interval1" happen?{s} before "the end of interval2".
(<=>
(starts ?INTERVAL1 ?INTERVAL2)
(and
(equal
(BeginFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(before
(EndFn ?INTERVAL1)
(EndFn ?INTERVAL2))))
interval1 finishes interval2 if and only if "the beginning of interval2" happen?{s} before "the beginning of interval1" and "the end of interval2" is equal to "the end of interval1".
(<=>
(finishes ?INTERVAL1 ?INTERVAL2)
(and
(before
(BeginFn ?INTERVAL2)
(BeginFn ?INTERVAL1))
(equal
(EndFn ?INTERVAL2)
(EndFn ?INTERVAL1))))
(=>
(instance ?OBJ Object)
(exists
(?TIME1 ?TIME2)
(and
(instance ?TIME1 TimePoint)
(instance ?TIME2 TimePoint)
(before ?TIME1 ?TIME2)
(forall
(?TIME)
(=>
(and
(beforeOrEqual ?TIME1 ?TIME)
(beforeOrEqual ?TIME ?TIME2))
(time ?OBJ ?TIME))))))
point2 is between point1 and point3 if and only if point1 happen?{s} before point2 and point2 happen?{s} before point3.
(<=>
(temporallyBetween ?POINT1 ?POINT2 ?POINT3)
(and
(before ?POINT1 ?POINT2)
(before ?POINT2 ?POINT3)))
point2 is between or at point1 and point3 if and only if point1 happen?{s} before or at point2 and point2 happen?{s} before or at point3.
(<=>
(temporallyBetweenOrEqual ?POINT1 ?POINT2 ?POINT3)
(and
(beforeOrEqual ?POINT1 ?POINT2)
(beforeOrEqual ?POINT2 ?POINT3)))
phys exists during time and time is an instance of time point if and only if time is between or at "the beginning of "the time of existence of phys"" and "the end of "the time of existence of phys"".
(<=>
(and
(time ?PHYS ?TIME)
(instance ?TIME TimePoint))
(temporallyBetweenOrEqual
(BeginFn
(WhenFn ?PHYS))
?TIME
(EndFn
(WhenFn ?PHYS))))
interval2 overlaps interval1 if and only if there exists time interval interval3 so that interval3 is a part of interval1 and interval3 is a part of interval2.
(<=>
(overlapsTemporally ?INTERVAL1 ?INTERVAL2)
(exists
(?INTERVAL3)
(and
(instance ?INTERVAL3 TimeInterval)
(temporalPart ?INTERVAL3 ?INTERVAL1)
(temporalPart ?INTERVAL3 ?INTERVAL2))))
If rel is an instance of spatial relation and rel(obj1,obj2) holds, then "the time of existence of obj2" overlaps "the time of existence of obj1".
(=>
(and
(instance ?REL SpatialRelation)
(holds ?REL ?OBJ1 ?OBJ2))
(overlapsTemporally
(WhenFn ?OBJ1)
(WhenFn ?OBJ2)))
If interval1 takes place during interval2, then "the end of interval1" happen?{s} before "the end of interval2" and "the beginning of interval2" happen?{s} before "the beginning of interval1".
(=>
(during ?INTERVAL1 ?INTERVAL2)
(and
(before
(EndFn ?INTERVAL1)
(EndFn ?INTERVAL2))
(before
(BeginFn ?INTERVAL2)
(BeginFn ?INTERVAL1))))
If "the beginning of interval1" is equal to "the beginning of interval2" and "the end of interval1" is equal to "the end of interval2", then interval1 is equal to interval2.
(=>
(and
(equal
(BeginFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(equal
(EndFn ?INTERVAL1)
(EndFn ?INTERVAL2)))
(equal ?INTERVAL1 ?INTERVAL2))
If "interval between point1 and point2" is equal to interval, then "the beginning of interval" is equal to point1 and "the end of interval" is equal to point2.
(=>
(equal
(TimeIntervalFn ?POINT1 ?POINT2)
?INTERVAL)
(and
(equal
(BeginFn ?INTERVAL)
?POINT1)
(equal
(EndFn ?INTERVAL)
?POINT2)))
If interval is an instance of "the recurring period from timeclass1 to timeclass2", then there exist timeclass1 time1,timeclass2 time2 so that time1 starts interval and time2 finishes interval.
(=>
(instance
?INTERVAL
(RecurrentTimeIntervalFn ?TIMECLASS1 ?TIMECLASS2))
(exists
(?TIME1 ?TIME2)
(and
(instance ?TIME1 ?TIMECLASS1)
(instance ?TIME2 ?TIMECLASS2)
(starts ?TIME1 ?INTERVAL)
(finishes ?TIME2 ?INTERVAL))))
If obj is a resource for proc and the measure of obj is quant1 immediately before "the time of existence of proc" and the measure of obj is quant2 immediately after "the time of existence of proc", then quant1 is greater than quant2.
(=>
(and
(resource ?PROC ?OBJ)
(holdsDuring
(ImmediatePastFn
(WhenFn ?PROC))
(measure ?OBJ ?QUANT1))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?PROC))
(measure ?OBJ ?QUANT2)))
(greaterThan ?QUANT1 ?QUANT2))
If day1 is an instance of "the day number1" and day2 is an instance of "the day number2" and "(number2-number1)" is equal to , then day1 meets day2.
(=>
(and
(instance
?DAY1
(DayFn ?NUMBER1 ?MONTH))
(instance
?DAY2
(DayFn ?NUMBER2 ?MONTH))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?DAY1 ?DAY2))
If hour1 is an instance of "the hour number1" and hour2 is an instance of "the hour number2" and "(number2-number1)" is equal to , then hour1 meets hour2.
(=>
(and
(instance
?HOUR1
(HourFn ?NUMBER1 ?DAY))
(instance
?HOUR2
(HourFn ?NUMBER2 ?DAY))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?HOUR1 ?HOUR2))
If minute1 is an instance of "the minute number1" and minute2 is an instance of "the minute number2" and "(number2-number1)" is equal to , then minute1 meets minute2.
(=>
(and
(instance
?MINUTE1
(MinuteFn ?NUMBER1 ?HOUR))
(instance
?MINUTE2
(MinuteFn ?NUMBER2 ?HOUR))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?MINUTE1 ?MINUTE2))
If second1 is an instance of "the second number1" and second2 is an instance of "the second number2" and "(number2-number1)" is equal to , then second1 meets second2.
(=>
(and
(instance
?SECOND1
(SecondFn ?NUMBER1 ?MINUTE))
(instance
?SECOND2
(SecondFn ?NUMBER2 ?MINUTE))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?SECOND1 ?SECOND2))
If year1 is an instance of year and year2 is an instance of year and "(year2-year1)" is equal to , then year1 meets year2.
(=>
(and
(instance ?YEAR1 Year)
(instance ?YEAR2 Year)
(equal
(SubtractionFn ?YEAR2 ?YEAR1)
1))
(meetsTemporally ?YEAR1 ?YEAR2))
If leap is an instance of leap year and leap is equal to "number year(s)", then
(=>
(and
(instance ?LEAP LeapYear)
(equal
?LEAP
(MeasureFn ?NUMBER Year)))
(or
(and
(equal
(RemainderFn ?NUMBER 4)
0)
(not
(equal
(RemainderFn ?NUMBER 100)
0)))
(equal
(RemainderFn ?NUMBER 400)
0)))
If month1 is equal to "the month january" and month2 is equal to "the month february", then month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn January ?YEAR))
(equal
?MONTH2
(MonthFn February ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If "the month february" is equal to month and year is not an instance of leap year, then duration of month is " day duration(s)".
(=>
(and
(equal
(MonthFn February ?YEAR)
?MONTH)
(not
(instance ?YEAR LeapYear)))
(duration
?MONTH
(MeasureFn 28 DayDuration)))
If "the month february" is equal to month and year is an instance of leap year, then duration of month is " day duration(s)".
(=>
(and
(equal
(MonthFn February ?YEAR)
?MONTH)
(instance ?YEAR LeapYear))
(duration
?MONTH
(MeasureFn 29 DayDuration)))
If month1 is equal to "the month february" and month2 is equal to "the month march", then month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn February ?YEAR))
(equal
?MONTH2
(MonthFn March ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 is equal to "the month march" and month2 is equal to "the month april", then month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn March ?YEAR))
(equal
?MONTH2
(MonthFn April ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 is equal to "the month april" and month2 is equal to "the month may", then month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn April ?YEAR))
(equal
?MONTH2
(MonthFn May ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 is equal to "the month may" and month2 is equal to "the month june", then month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn May ?YEAR))
(equal
?MONTH2
(MonthFn June ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 is equal to "the month june" and month2 is equal to "the month july", then month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn June ?YEAR))
(equal
?MONTH2
(MonthFn July ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 is equal to "the month july" and month2 is equal to "the month august", then month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn July ?YEAR))
(equal
?MONTH2
(MonthFn August ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 is equal to "the month august" and month2 is equal to "the month september", then month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn August ?YEAR))
(equal
?MONTH2
(MonthFn September ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 is equal to "the month september" and month2 is equal to "the month october", then month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn September ?YEAR))
(equal
?MONTH2
(MonthFn October ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 is equal to "the month october" and month2 is equal to "the month november", then month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn October ?YEAR))
(equal
?MONTH2
(MonthFn November ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 is equal to "the month november" and month2 is equal to "the month december", then month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn November ?YEAR))
(equal
?MONTH2
(MonthFn December ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 is equal to "the month december" and month2 is equal to "the month january" and year1 meets year2, then month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn December ?YEAR1))
(equal
?MONTH2
(MonthFn January ?YEAR2))
(meetsTemporally ?YEAR1 ?YEAR2))
(meetsTemporally ?MONTH1 ?MONTH2))
If day1 is an instance of monday and day2 is an instance of tuesday and week is an instance of week and day1 is a part of week and day2 is a part of week, then day1 meets day2.
(=>
(and
(instance ?DAY1 Monday)
(instance ?DAY2 Tuesday)
(instance ?WEEK Week)
(temporalPart ?DAY1 ?WEEK)
(temporalPart ?DAY2 ?WEEK))
(meetsTemporally ?DAY1 ?DAY2))
If day1 is an instance of tuesday and day2 is an instance of wednesday and week is an instance of week and day1 is a part of week and day2 is a part of week, then day1 meets day2.
(=>
(and
(instance ?DAY1 Tuesday)
(instance ?DAY2 Wednesday)
(instance ?WEEK Week)
(temporalPart ?DAY1 ?WEEK)
(temporalPart ?DAY2 ?WEEK))
(meetsTemporally ?DAY1 ?DAY2))
If day1 is an instance of wednesday and day2 is an instance of thursday and week is an instance of week and day1 is a part of week and day2 is a part of week, then day1 meets day2.
(=>
(and
(instance ?DAY1 Wednesday)
(instance ?DAY2 Thursday)
(instance ?WEEK Week)
(temporalPart ?DAY1 ?WEEK)
(temporalPart ?DAY2 ?WEEK))
(meetsTemporally ?DAY1 ?DAY2))
If day1 is an instance of thursday and day2 is an instance of friday and week is an instance of week and day1 is a part of week and day2 is a part of week, then day1 meets day2.
(=>
(and
(instance ?DAY1 Thursday)
(instance ?DAY2 Friday)
(instance ?WEEK Week)
(temporalPart ?DAY1 ?WEEK)
(temporalPart ?DAY2 ?WEEK))
(meetsTemporally ?DAY1 ?DAY2))
If day1 is an instance of friday and day2 is an instance of saturday and week is an instance of week and day1 is a part of week and day2 is a part of week, then day1 meets day2.
(=>
(and
(instance ?DAY1 Friday)
(instance ?DAY2 Saturday)
(instance ?WEEK Week)
(temporalPart ?DAY1 ?WEEK)
(temporalPart ?DAY2 ?WEEK))
(meetsTemporally ?DAY1 ?DAY2))
If day1 is an instance of saturday and day2 is an instance of sunday and week is an instance of week and day1 is a part of week and day2 is a part of week, then day1 meets day2.
(=>
(and
(instance ?DAY1 Saturday)
(instance ?DAY2 Sunday)
(instance ?WEEK Week)
(temporalPart ?DAY1 ?WEEK)
(temporalPart ?DAY2 ?WEEK))
(meetsTemporally ?DAY1 ?DAY2))
If day1 is an instance of sunday and day2 is an instance of monday and week1 is an instance of week and week2 is an instance of week and day1 is a part of week1 and day2 is a part of week2 and week1 meets week2, then day1 meets day2.
(=>
(and
(instance ?DAY1 Sunday)
(instance ?DAY2 Monday)
(instance ?WEEK1 Week)
(instance ?WEEK2 Week)
(temporalPart ?DAY1 ?WEEK1)
(temporalPart ?DAY2 ?WEEK2)
(meetsTemporally ?WEEK1 ?WEEK2))
(meetsTemporally ?DAY1 ?DAY2))
- if "decomposition of interval into ? interval-types" is equal to class,
- then for all time1,time2 holds: if time1 is an instance of interval-type and time2 is an instance of class, then there exists duration so that duration of time1 is duration and duration of time2 is duration
.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(forall
(?TIME1 ?TIME2)
(=>
(and
(instance ?TIME1 ?INTERVAL-TYPE)
(instance ?TIME2 ?CLASS))
(exists
(?DURATION)
(and
(duration ?TIME1 ?DURATION)
(duration ?TIME2 ?DURATION))))))
- if "decomposition of interval into ? interval-types" is equal to class,
- then for all time1,time2 holds: if time1 is an instance of class and time2 is an instance of class and time1 is not equal to time2, then time1 meets time2 or time2 meets time1 or time1 happens earlier than time2 or time2 happens earlier than time1
.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(forall
(?TIME1 ?TIME2)
(=>
(and
(instance ?TIME1 ?CLASS)
(instance ?TIME2 ?CLASS)
(not
(equal ?TIME1 ?TIME2)))
(or
(meetsTemporally ?TIME1 ?TIME2)
(meetsTemporally ?TIME2 ?TIME1)
(earlier ?TIME1 ?TIME2)
(earlier ?TIME2 ?TIME1)))))
If "decomposition of interval into ? interval-types" is equal to class, then there exists class time so that time starts interval.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(exists
(?TIME)
(and
(instance ?TIME ?CLASS)
(starts ?TIME ?INTERVAL))))
If "decomposition of interval into ? interval-types" is equal to class, then there exists class time so that time finishes interval.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(exists
(?TIME)
(and
(instance ?TIME ?CLASS)
(finishes ?TIME ?INTERVAL))))
- if "decomposition of interval into ? interval-types" is equal to class,
- then for all time1 holds: if time1 is an instance of class and time1 doesn't finish interval, then there exists class time2 so that time1 meets time2
.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(forall
(?TIME1)
(=>
(and
(instance ?TIME1 ?CLASS)
(not
(finishes ?TIME1 ?INTERVAL)))
(exists
(?TIME2)
(and
(instance ?TIME2 ?CLASS)
(meetsTemporally ?TIME1 ?TIME2))))))
- if "decomposition of interval into ? interval-types" is equal to class,
- then for all time1 holds: if time1 is an instance of class and time1 doesn't start interval, then there exists class time2 so that time2 meets time1
.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(forall
(?TIME1)
(=>
(and
(instance ?TIME1 ?CLASS)
(not
(starts ?TIME1 ?INTERVAL)))
(exists
(?TIME2)
(and
(instance ?TIME2 ?CLASS)
(meetsTemporally ?TIME2 ?TIME1))))))
- if "decomposition of interval into ? interval-types" is equal to class,
- then for all time holds: if time is an instance of time point and time is a part of interval, then there exists class instance so that time is a part of instance
.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(forall
(?TIME)
(=>
(and
(instance ?TIME TimePoint)
(temporalPart ?TIME ?INTERVAL))
(exists
(?INSTANCE)
(and
(instance ?INSTANCE ?CLASS)
(temporalPart ?TIME ?INSTANCE))))))
If month is an instance of month and duration of month is "number day duration(s)", then "the number of instances in "decomposition of month into ? days"" is equal to number.
(=>
(and
(instance ?MONTH Month)
(duration
?MONTH
(MeasureFn ?NUMBER DayDuration)))
(equal
(CardinalityFn
(TemporalCompositionFn ?MONTH Day))
?NUMBER))
obj1 connects obj2 and obj3 if and only if obj1 is connected to obj2 and obj1 is connected to obj3 and obj2 is not connected to obj3.
(<=>
(connects ?OBJ1 ?OBJ2 ?OBJ3)
(and
(connected ?OBJ1 ?OBJ2)
(connected ?OBJ1 ?OBJ3)
(not
(connected ?OBJ2 ?OBJ3))))
obj1 overlaps with obj2 if and only if there exists obj3 so that obj3 is a part of obj1 and obj3 is a part of obj2.
(<=>
(overlapsSpatially ?OBJ1 ?OBJ2)
(exists
(?OBJ3)
(and
(part ?OBJ3 ?OBJ1)
(part ?OBJ3 ?OBJ2))))
If obj1 is a member of coll and obj2 is a member of coll and obj1 is not equal to obj2, then obj1 doesn't overlap with obj2.
(=>
(and
(member ?OBJ1 ?COLL)
(member ?OBJ2 ?COLL)
(not
(equal ?OBJ1 ?OBJ2)))
(not
(overlapsSpatially ?OBJ1 ?OBJ2)))
If rel is an instance of case role and rel(process,obj) holds, then there exists time so that "the place where process was at time" overlaps with obj.
(=>
(and
(instance ?REL CaseRole)
(holds ?REL ?PROCESS ?OBJ))
(exists
(?TIME)
(overlapsSpatially
(WhereFn ?PROCESS ?TIME)
?OBJ)))
obj1 partially overlaps with obj2 if and only if - obj1 is not a part of obj2
and - obj2 is not a part of obj1
and - there exists obj3 so that obj3 is a part of obj1 and obj3 is a part of obj2
.
(<=>
(overlapsPartially ?OBJ1 ?OBJ2)
(and
(not
(part ?OBJ1 ?OBJ2))
(not
(part ?OBJ2 ?OBJ1))
(exists
(?OBJ3)
(and
(part ?OBJ3 ?OBJ1)
(part ?OBJ3 ?OBJ2)))))
If obj1 is a superficial part of obj2, then obj1 is not a interior part of obj2 and there doesn't exist obj3 so that obj3 is a interior part of obj1.
(=>
(superficialPart ?OBJ1 ?OBJ2)
(and
(not
(interiorPart ?OBJ1 ?OBJ2))
(not
(exists
(?OBJ3)
(interiorPart ?OBJ3 ?OBJ1)))))
If the bottom of object is bottom and part is a part of object and part is not connected to bottom, then part is above to bottom.
(=>
(and
(bottom ?BOTTOM ?OBJECT)
(part ?PART ?OBJECT)
(not
(connected ?PART ?BOTTOM)))
(orientation ?PART ?BOTTOM Above))
If the top of object is top and part is a part of object and part is not connected to top, then part is below to top.
(=>
(and
(top ?TOP ?OBJECT)
(part ?PART ?OBJECT)
(not
(connected ?PART ?TOP)))
(orientation ?PART ?TOP Below))
If a side of object is side and part is a part of object and part is not connected to side, then there exists direct so that side is direct to part.
(=>
(and
(side ?SIDE ?OBJECT)
(part ?PART ?OBJECT)
(not
(connected ?PART ?SIDE)))
(exists
(?DIRECT)
(orientation ?SIDE ?PART ?DIRECT)))
The width of object is width if and only if there exist side1,side2 so that a side of object is side1 and a side of object is side2 and the distance between side1 and side2 is width.
(<=>
(width ?OBJECT ?WIDTH)
(exists
(?SIDE1 ?SIDE2)
(and
(side ?SIDE1 ?OBJECT)
(side ?SIDE2 ?OBJECT)
(distance ?SIDE1 ?SIDE2 ?WIDTH))))
If the height of object is height and the top of object is top and the bottom of object is bottom, then the distance between top and bottom is height.
(=>
(and
(height ?OBJECT ?HEIGHT)
(top ?TOP ?OBJECT)
(bottom ?BOTTOM ?OBJECT))
(distance ?TOP ?BOTTOM ?HEIGHT))
If obj3 is equal to "the intersection of the parts of obj1 and obj2", then for all part holds: part is a part of obj3 if and only if part is a part of obj1 and part is a part of obj2.
(=>
(equal
?OBJ3
(MereologicalProductFn ?OBJ1 ?OBJ2))
(forall
(?PART)
(<=>
(part ?PART ?OBJ3)
(and
(part ?PART ?OBJ1)
(part ?PART ?OBJ2)))))
If obj3 is equal to "the difference between the parts of obj1 and obj2", then for all part holds: part is a part of obj3 if and only if part is a part of obj1 and part is not a part of obj2.
(=>
(equal
?OBJ3
(MereologicalDifferenceFn ?OBJ1 ?OBJ2))
(forall
(?PART)
(<=>
(part ?PART ?OBJ3)
(and
(part ?PART ?OBJ1)
(not
(part ?PART ?OBJ2))))))
If hole is a hole in obj1 and hole is a hole in obj2, then there exists obj3 so that obj3 is a properPart of "the intersection of the parts of obj1 and obj2" and hole is a hole in obj3.
(=>
(and
(hole ?HOLE ?OBJ1)
(hole ?HOLE ?OBJ2))
(exists
(?OBJ3)
(and
(properPart
?OBJ3
(MereologicalProductFn ?OBJ1 ?OBJ2))
(hole ?HOLE ?OBJ3))))
- if hole1 is a hole in obj and hole2 is a hole in obj,
- then for all hole3 holds: if hole3 is a part of "the union of the parts of hole1 and hole2", then hole3 is a hole in obj
.
(=>
(and
(hole ?HOLE1 ?OBJ)
(hole ?HOLE2 ?OBJ))
(forall
(?HOLE3)
(=>
(part
?HOLE3
(MereologicalSumFn ?HOLE1 ?HOLE2))
(hole ?HOLE3 ?OBJ))))
If hole is a hole in obj1 and obj1 is a part of obj2, then hole overlaps with obj2 or hole is a hole in obj2.
(=>
(and
(hole ?HOLE ?OBJ1)
(part ?OBJ1 ?OBJ2))
(or
(overlapsSpatially ?HOLE ?OBJ2)
(hole ?HOLE ?OBJ2)))
If hole1 is a hole in obj1 and hole2 is a hole in obj2 and hole1 overlaps with hole2, then obj1 overlaps with obj2.
(=>
(and
(hole ?HOLE1 ?OBJ1)
(hole ?HOLE2 ?OBJ2)
(overlapsSpatially ?HOLE1 ?HOLE2))
(overlapsSpatially ?OBJ1 ?OBJ2))
If obj1 is equal to "the host of the hole hole", then for all obj2 holds: obj2 overlaps with obj1 if and only if there exists obj3 so that hole is a hole in obj3 and obj2 overlaps with obj3.
(=>
(equal
?OBJ1
(PrincipalHostFn ?HOLE))
(forall
(?OBJ2)
(<=>
(overlapsSpatially ?OBJ2 ?OBJ1)
(exists
(?OBJ3)
(and
(hole ?HOLE ?OBJ3)
(overlapsSpatially ?OBJ2 ?OBJ3))))))
If hole1 is an instance of hole and hole2 is a properPart of hole1, then there exists obj so that hole1 meets obj and hole2 doesn't meet obj.
(=>
(and
(instance ?HOLE1 Hole)
(properPart ?HOLE2 ?HOLE1))
(exists
(?OBJ)
(and
(meetsSpatially ?HOLE1 ?OBJ)
(not
(meetsSpatially ?HOLE2 ?OBJ)))))
fillable is an attribute of hole1 if and only if there exists hole hole2 so that hole1 is a part of hole2.
(<=>
(attribute ?HOLE1 Fillable)
(exists
(?HOLE2)
(and
(instance ?HOLE2 Hole)
(part ?HOLE1 ?HOLE2))))
If obj partially fills hole1, then there exists hole2 so that hole2 is a part of hole1 and obj completely fills hole2.
(=>
(partiallyFills ?OBJ ?HOLE1)
(exists
(?HOLE2)
(and
(part ?HOLE2 ?HOLE1)
(completelyFills ?OBJ ?HOLE2))))
If obj properly fills hole1, then there exists hole2 so that hole2 is a part of hole1 and obj fills hole2.
(=>
(properlyFills ?OBJ ?HOLE1)
(exists
(?HOLE2)
(and
(part ?HOLE2 ?HOLE1)
(fills ?OBJ ?HOLE2))))
If obj1 completely fills hole, then there exists obj2 so that obj2 is a part of obj1 and obj2 fills hole.
(=>
(completelyFills ?OBJ1 ?HOLE)
(exists
(?OBJ2)
(and
(part ?OBJ2 ?OBJ1)
(fills ?OBJ2 ?HOLE))))
If obj1 fills hole and fillable is an attribute of obj2, then obj1 doesn't overlap with obj2.
(=>
(and
(fills ?OBJ1 ?HOLE)
(attribute ?OBJ2 Fillable))
(not
(overlapsSpatially ?OBJ1 ?OBJ2)))
If obj1 properly fills hole and obj2 is connected to obj1, then hole is connected to obj2.
(=>
(and
(properlyFills ?OBJ1 ?HOLE)
(connected ?OBJ2 ?OBJ1))
(connected ?HOLE ?OBJ2))
If obj fills hole1 and hole2 is a properPart of hole1, then obj completely fills hole2.
(=>
(and
(fills ?OBJ ?HOLE1)
(properPart ?HOLE2 ?HOLE1))
(completelyFills ?OBJ ?HOLE2))
If obj1 fills hole and obj2 is a properPart of obj1, then obj2 properly fills hole.
(=>
(and
(fills ?OBJ1 ?HOLE)
(properPart ?OBJ2 ?OBJ1))
(properlyFills ?OBJ2 ?HOLE))
If obj1 is equal to "the surface of the hole hole", then for all obj2 holds: obj2 overlaps with obj1 if and only if there exists obj3 so that obj3 is a superficial part of "the host of the hole hole" and hole meets obj3 and obj2 overlaps with obj3.
(=>
(equal
?OBJ1
(SkinFn ?HOLE))
(forall
(?OBJ2)
(<=>
(overlapsSpatially ?OBJ2 ?OBJ1)
(exists
(?OBJ3)
(and
(superficialPart
?OBJ3
(PrincipalHostFn ?HOLE))
(meetsSpatially ?HOLE ?OBJ3)
(overlapsSpatially ?OBJ2 ?OBJ3))))))
If proc is an instance of process and subproc is a subprocess of proc, then there exists time so that subproc exists during time.
(=>
(and
(instance ?PROC Process)
(subProcess ?SUBPROC ?PROC))
(exists
(?TIME)
(time ?SUBPROC ?TIME)))
If proc is an instance of biological process, then there exists organism obj so that proc is located at obj.
(=>
(instance ?PROC BiologicalProcess)
(exists
(?OBJ)
(and
(instance ?OBJ Organism)
(located ?PROC ?OBJ))))
If proc is an instance of biological process and org experiences proc, then org is an instance of organism.
(=>
(and
(instance ?PROC BiologicalProcess)
(experiencer ?PROC ?ORG))
(instance ?ORG Organism))
If birth is an instance of birth and agent experiences birth, then there exists death death so that agent experiences death.
(=>
(and
(instance ?BIRTH Birth)
(experiencer ?BIRTH ?AGENT))
(exists
(?DEATH)
(and
(instance ?DEATH Death)
(experiencer ?DEATH ?AGENT))))
If death is an instance of death and agent experiences death, then dead is an attribute of agent after "the time of existence of death".
(=>
(and
(instance ?DEATH Death)
(experiencer ?DEATH ?AGENT))
(holdsDuring
(FutureFn
(WhenFn ?DEATH))
(attribute ?AGENT Dead)))
If death is an instance of death and birth is an instance of birth and agent experiences death and agent experiences birth, then there exists time so that "the time of existence of birth" meets time and time meets "the time of existence of death" and living is an attribute of agent during time.
(=>
(and
(instance ?DEATH Death)
(instance ?BIRTH Birth)
(experiencer ?DEATH ?AGENT)
(experiencer ?BIRTH ?AGENT))
(exists
(?TIME)
(and
(meetsTemporally
(WhenFn ?BIRTH)
?TIME)
(meetsTemporally
?TIME
(WhenFn ?DEATH))
(holdsDuring
?TIME
(attribute ?AGENT Living)))))
If act is an instance of ingesting and food is a patient of act, then food is an instance of food.
(=>
(and
(instance ?ACT Ingesting)
(patient ?ACT ?FOOD))
(instance ?FOOD Food))
If act is an instance of eating and food is a patient of act, then solid is an attribute of food.
(=>
(and
(instance ?ACT Eating)
(patient ?ACT ?FOOD))
(attribute ?FOOD Solid))
If digest is an instance of digesting and digest is an agent of organism, then there exists ingesting ingest so that ingest is an agent of organism and "the time of existence of digest" overlaps "the time of existence of ingest".
(=>
(and
(instance ?DIGEST Digesting)
(agent ?DIGEST ?ORGANISM))
(exists
(?INGEST)
(and
(instance ?INGEST Ingesting)
(agent ?INGEST ?ORGANISM)
(overlapsTemporally
(WhenFn ?INGEST)
(WhenFn ?DIGEST)))))
If digest is an instance of digesting, then there exists chemical decomposition decomp so that decomp is a subprocess of digest.
(=>
(instance ?DIGEST Digesting)
(exists
(?DECOMP)
(and
(instance ?DECOMP ChemicalDecomposition)
(subProcess ?DECOMP ?DIGEST))))
If rep is an instance of replication and rep is an agent of parent and child is a result of rep, then parent is a parent of child.
(=>
(and
(instance ?REP Replication)
(agent ?REP ?PARENT)
(result ?REP ?CHILD))
(parent ?CHILD ?PARENT))
If rep is an instance of replication, then there exists reproductive body body so that body is a result of rep.
(=>
(instance ?REP Replication)
(exists
(?BODY)
(and
(instance ?BODY ReproductiveBody)
(result ?REP ?BODY))))
If rep is an instance of sexual reproduction and organism is a result of rep, then there don't exist mother,father so that mother is a mother of organism and father is a father of organism.
(=>
(and
(instance ?REP SexualReproduction)
(result ?REP ?ORGANISM))
(not
(exists
(?MOTHER ?FATHER)
(and
(mother ?ORGANISM ?MOTHER)
(father ?ORGANISM ?FATHER)))))
If rep is an instance of asexual reproduction and organism is a result of rep, then there don't exist parent1,parent2 so that parent1 is a parent of organism and parent2 is a parent of organism and parent1 is not equal to parent2.
(=>
(and
(instance ?REP AsexualReproduction)
(result ?REP ?ORGANISM))
(not
(exists
(?PARENT1 ?PARENT2)
(and
(parent ?ORGANISM ?PARENT1)
(parent ?ORGANISM ?PARENT2)
(not
(equal ?PARENT1 ?PARENT2))))))
If process is an instance of psychological process, then there exists animal animal so that animal experiences process.
(=>
(instance ?PROCESS PsychologicalProcess)
(exists
(?ANIMAL)
(and
(instance ?ANIMAL Animal)
(experiencer ?PROCESS ?ANIMAL))))
If proc is an instance of organ or tissueprocess, then there exists thing so that proc is located at thing and thing is an instance of organ or thing is an instance of tissue.
(=>
(instance ?PROC OrganOrTissueProcess)
(exists
(?THING)
(and
(located ?PROC ?THING)
(or
(instance ?THING Organ)
(instance ?THING Tissue)))))
If path is an instance of pathologic process and org experiences path, then there exist part,disease or syndrome disease so that part is a part of org and disease is an attribute of part.
(=>
(and
(instance ?PATH PathologicProcess)
(experiencer ?PATH ?ORG))
(exists
(?PART ?DISEASE)
(and
(part ?PART ?ORG)
(instance ?DISEASE DiseaseOrSyndrome)
(attribute ?PART ?DISEASE))))
If inj is an instance of injuring, then there exists anatomical structure struct so that struct is a patient of inj.
(=>
(instance ?INJ Injuring)
(exists
(?STRUCT)
(and
(instance ?STRUCT AnatomicalStructure)
(patient ?INJ ?STRUCT))))
inj is an instance of injuring if and only if inj is an instance of damaging and organism is a patient of inj.
(<=>
(instance ?INJ Injuring)
(and
(instance ?INJ Damaging)
(patient ?INJ Organism)))
If poison is an instance of poisoning, then there exists thing so that thing is a patient of poison and thing is an instance of organism or thing is an instance of anatomical structure.
(=>
(instance ?POISON Poisoning)
(exists
(?THING)
(and
(patient ?POISON ?THING)
(or
(instance ?THING Organism)
(instance ?THING AnatomicalStructure)))))
If poison is an instance of poisoning, then there exists biologically active substance substance so that substance is an instrument for poison.
(=>
(instance ?POISON Poisoning)
(exists
(?SUBSTANCE)
(and
(instance ?SUBSTANCE BiologicallyActiveSubstance)
(instrument ?POISON ?SUBSTANCE))))
If proc is an instance of intentional process and proc is an agent of agent, then there exists purp so that proc has &n purpose purp for agent.
(=>
(and
(instance ?PROC IntentionalProcess)
(agent ?PROC ?AGENT))
(exists
(?PURP)
(hasPurposeForAgent ?PROC ?PURP ?AGENT)))
If proc is an instance of intentional process, then there exists cognitive agent agent so that proc is an agent of agent.
(=>
(instance ?PROC IntentionalProcess)
(exists
(?AGENT)
(and
(instance ?AGENT CognitiveAgent)
(agent ?PROC ?AGENT))))
If act is an instance of organizational process and act is an agent of agent, then
(=>
(and
(instance ?ACT OrganizationalProcess)
(agent ?ACT ?AGENT))
(or
(instance ?AGENT Organization)
(exists
(?ORG)
(and
(instance ?ORG Organization)
(member ?AGENT ?ORG)))))
If act is an instance of religious process and act is an agent of agent, then
(=>
(and
(instance ?ACT ReligiousProcess)
(agent ?ACT ?AGENT))
(or
(instance ?AGENT ReligiousOrganization)
(exists
(?ORG)
(and
(member ?AGENT ?ORG)
(instance ?ORG ReligiousOrganization)))))
If join is an instance of joining an organization and org is an instance of organization and join is an agent of org and person is a patient of join, then person is a member of org immediately after "the time of existence of join".
(=>
(and
(instance ?JOIN JoiningAnOrganization)
(instance ?ORG Organization)
(agent ?JOIN ?ORG)
(patient ?JOIN ?PERSON))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?JOIN))
(member ?PERSON ?ORG)))
If leave is an instance of leaving an organization and org is an instance of organization and leave is an agent of org and person is a patient of leave, then person is not a member of org immediately after "the time of existence of leave".
(=>
(and
(instance ?LEAVE LeavingAnOrganization)
(instance ?ORG Organization)
(agent ?LEAVE ?ORG)
(patient ?LEAVE ?PERSON))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?LEAVE))
(not
(member ?PERSON ?ORG))))
If grad is an instance of graduation and grad is an agent of org and person is a patient of grad, then org is an instance of educational organization.
(=>
(and
(instance ?GRAD Graduation)
(agent ?GRAD ?ORG)
(patient ?GRAD ?PERSON))
(instance ?ORG EducationalOrganization))
If mat is an instance of matriculation and mat is an agent of org and person is a patient of mat, then org is an instance of educational organization.
(=>
(and
(instance ?MAT Matriculation)
(agent ?MAT ?ORG)
(patient ?MAT ?PERSON))
(instance ?ORG EducationalOrganization))
If hire is an instance of hiring and org is an instance of organization and hire is an agent of org and person is a patient of hire, then org employs person immediately after "the time of existence of hire".
(=>
(and
(instance ?HIRE Hiring)
(instance ?ORG Organization)
(agent ?HIRE ?ORG)
(patient ?HIRE ?PERSON))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?HIRE))
(employs ?ORG ?PERSON)))
If fire is an instance of terminating employment and org is an instance of organization and fire is an agent of org and person is a patient of fire, then org doesn't employ person immediately after "the time of existence of fire".
(=>
(and
(instance ?FIRE TerminatingEmployment)
(instance ?ORG Organization)
(agent ?FIRE ?ORG)
(patient ?FIRE ?PERSON))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?FIRE))
(not
(employs ?ORG ?PERSON))))
If proc is an instance of political process, then there exists government gov so that proc is an agent of gov or gov is a patient of proc.
(=>
(instance ?PROC PoliticalProcess)
(exists
(?GOV)
(and
(instance ?GOV Government)
(or
(agent ?PROC ?GOV)
(patient ?PROC ?GOV)))))
If increase is an instance of increasing and obj is a patient of increase, then there exist unit,quant1,quant2 so that "obj unit(s)" is equal to quant1 immediately before "the time of existence of increase" and "obj unit(s)" is equal to quant2 immediately after "the time of existence of increase" and quant2 is greater than quant1.
(=>
(and
(instance ?INCREASE Increasing)
(patient ?INCREASE ?OBJ))
(exists
(?UNIT ?QUANT1 ?QUANT2)
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?INCREASE))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT1))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?INCREASE))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT2))
(greaterThan ?QUANT2 ?QUANT1))))
If heat is an instance of heating and obj is a patient of heat, then there exist temperature measure unit,quant1,quant2 so that "obj unit(s)" is equal to quant1 immediately before "the time of existence of heat" and "obj unit(s)" is equal to quant2 immediately after "the time of existence of heat" and quant2 is greater than quant1.
(=>
(and
(instance ?HEAT Heating)
(patient ?HEAT ?OBJ))
(exists
(?UNIT ?QUANT1 ?QUANT2)
(and
(instance ?UNIT TemperatureMeasure)
(holdsDuring
(ImmediatePastFn
(WhenFn ?HEAT))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT1))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?HEAT))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT2))
(greaterThan ?QUANT2 ?QUANT1))))
If decrease is an instance of decreasing and obj is a patient of decrease, then there exist unit,quant1,quant2 so that "obj unit(s)" is equal to quant1 immediately before "the time of existence of decrease" and "obj unit(s)" is equal to quant2 immediately after "the time of existence of decrease" and quant2 is less than quant1.
(=>
(and
(instance ?DECREASE Decreasing)
(patient ?DECREASE ?OBJ))
(exists
(?UNIT ?QUANT1 ?QUANT2)
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?DECREASE))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT1))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?DECREASE))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT2))
(lessThan ?QUANT2 ?QUANT1))))
If cool is an instance of cooling and obj is a patient of cool, then there exist temperature measure unit,quant1,quant2 so that "obj unit(s)" is equal to quant1 immediately before "the time of existence of cool" and "obj unit(s)" is equal to quant2 immediately after "the time of existence of cool" and quant2 is less than quant1.
(=>
(and
(instance ?COOL Cooling)
(patient ?COOL ?OBJ))
(exists
(?UNIT ?QUANT1 ?QUANT2)
(and
(instance ?UNIT TemperatureMeasure)
(holdsDuring
(ImmediatePastFn
(WhenFn ?COOL))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT1))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?COOL))
(equal
(MeasureFn ?OBJ ?UNIT)
?QUANT2))
(lessThan ?QUANT2 ?QUANT1))))
If motion is an instance of motion and obj is a patient of motion and motion origins at place, then obj is located at place immediately before "the time of existence of motion".
(=>
(and
(instance ?MOTION Motion)
(patient ?MOTION ?OBJ)
(origin ?MOTION ?PLACE))
(holdsDuring
(ImmediatePastFn
(WhenFn ?MOTION))
(located ?OBJ ?PLACE)))
If motion is an instance of motion and obj is a patient of motion and motion ends at place, then obj is located at place immediately after "the time of existence of motion".
(=>
(and
(instance ?MOTION Motion)
(patient ?MOTION ?OBJ)
(destination ?MOTION ?PLACE))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?MOTION))
(located ?OBJ ?PLACE)))
- if
- path1 is path along with process occurs
and - process origins at source
and - process ends at dest
and - the length of path1 is measure1
and - there don't exist path2,measure2 so that path2 is path along with process occurs and process origins at origin and process ends at dest and the length of path2 is measure2 and measure2 is less than measure1
, - then for all obj holds: if obj is a part of path1, then obj is between source and dest
.
(=>
(and
(path ?PROCESS ?PATH1)
(origin ?PROCESS ?SOURCE)
(destination ?PROCESS ?DEST)
(length ?PATH1 ?MEASURE1)
(not
(exists
(?PATH2 ?MEASURE2)
(and
(path ?PROCESS ?PATH2)
(origin ?PROCESS ?ORIGIN)
(destination ?PROCESS ?DEST)
(length ?PATH2 ?MEASURE2)
(lessThan ?MEASURE2 ?MEASURE1)))))
(forall
(?OBJ)
(=>
(part ?OBJ ?PATH1)
(between ?SOURCE ?OBJ ?DEST))))
If motion is an instance of body motion, then there exist body part obj,organism agent so that obj is a patient of motion and motion is an agent of agent.
(=>
(instance ?MOTION BodyMotion)
(exists
(?OBJ ?AGENT)
(and
(instance ?OBJ BodyPart)
(patient ?MOTION ?OBJ)
(instance ?AGENT Organism)
(agent ?MOTION ?AGENT))))
If walk is an instance of walking and walk is an agent of agent, then there exists land area area so that agent is located at area.
(=>
(and
(instance ?WALK Walking)
(agent ?WALK ?AGENT))
(exists
(?AREA)
(and
(instance ?AREA LandArea)
(located ?AGENT ?AREA))))
If swim is an instance of swimming and swim is an agent of agent, then there exists water area area so that agent is located at area.
(=>
(and
(instance ?SWIM Swimming)
(agent ?SWIM ?AGENT))
(exists
(?AREA)
(and
(instance ?AREA WaterArea)
(located ?AGENT ?AREA))))
If proc is an instance of direction change, then there exists directional attribute attr so that - proc is performed in the manner attr immediately before "the time of existence of proc" and proc is performed in the manner attr immediately after "the time of existence of proc"
or - proc is performed in the manner attr immediately after "the time of existence of proc" and proc is performed in the manner attr immediately before "the time of existence of proc"
.
(=>
(instance ?PROC DirectionChange)
(exists
(?ATTR)
(and
(instance ?ATTR DirectionalAttribute)
(or
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?PROC))
(manner ?PROC ?ATTR))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?PROC))
(not
(manner ?PROC ?ATTR))))
(and
(holdsDuring
(ImmediateFutureFn
(WhenFn ?PROC))
(manner ?PROC ?ATTR))
(holdsDuring
(ImmediatePastFn
(WhenFn ?PROC))
(not
(manner ?PROC ?ATTR))))))))
If transfer is an instance of transfer and transfer is an agent of agent and patient is a patient of transfer, then agent is not equal to patient.
(=>
(and
(instance ?TRANSFER Transfer)
(agent ?TRANSFER ?AGENT)
(patient ?TRANSFER ?PATIENT))
(not
(equal ?AGENT ?PATIENT)))
If remove is an instance of removing and remove origins at place and obj is a patient of remove, then obj is located at place immediately before "the time of existence of remove" and obj is not located at place immediately after "the time of existence of remove".
(=>
(and
(instance ?REMOVE Removing)
(origin ?REMOVE ?PLACE)
(patient ?REMOVE ?OBJ))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?REMOVE))
(located ?OBJ ?PLACE))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?REMOVE))
(not
(located ?OBJ ?PLACE)))))
If put is an instance of putting and put ends at place and obj is a patient of put, then obj is not located at place immediately before "the time of existence of put" and obj is located at place immediately after "the time of existence of put".
(=>
(and
(instance ?PUT Putting)
(destination ?PUT ?PLACE)
(patient ?PUT ?OBJ))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?PUT))
(not
(located ?OBJ ?PLACE)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?PUT))
(located ?OBJ ?PLACE))))
If sub is an instance of substituting, then there exist putting put,removing remove,obj1,obj2,place so that put is a subprocess of sub and remove is a subprocess of sub and obj1 is a patient of remove and remove origins at place and obj2 is a patient of put and put ends at place and obj1 is not equal to obj2.
(=>
(instance ?SUB Substituting)
(exists
(?PUT ?REMOVE ?OBJ1 ?OBJ2 ?PLACE)
(and
(instance ?PUT Putting)
(instance ?REMOVE Removing)
(subProcess ?PUT ?SUB)
(subProcess ?REMOVE ?SUB)
(patient ?REMOVE ?OBJ1)
(origin ?REMOVE ?PLACE)
(patient ?PUT ?OBJ2)
(destination ?PUT ?PLACE)
(not
(equal ?OBJ1 ?OBJ2)))))
If touch is an instance of touching and touch is an agent of obj1 and obj2 is a patient of touch, then obj1 is connected to obj2 immediately after "the time of existence of touch".
(=>
(and
(instance ?TOUCH Touching)
(agent ?TOUCH ?OBJ1)
(patient ?TOUCH ?OBJ2))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?TOUCH))
(connected ?OBJ1 ?OBJ2)))
If impact is an instance of impacting and obj is a patient of impact, then there exists impelling impel so that obj is a patient of impel and "the time of existence of impel" happens earlier than "the time of existence of impact".
(=>
(and
(instance ?IMPACT Impacting)
(patient ?IMPACT ?OBJ))
(exists
(?IMPEL)
(and
(instance ?IMPEL Impelling)
(patient ?IMPEL ?OBJ)
(earlier
(WhenFn ?IMPEL)
(WhenFn ?IMPACT)))))
If trans is an instance of transportation, then there exists transportation device device so that device is an instrument for trans.
(=>
(instance ?TRANS Transportation)
(exists
(?DEVICE)
(and
(instance ?DEVICE TransportationDevice)
(instrument ?TRANS ?DEVICE))))
If steer is an instance of steering, then there exists transportation device vehicle so that vehicle is a patient of steer.
(=>
(instance ?STEER Steering)
(exists
(?VEHICLE)
(and
(instance ?VEHICLE TransportationDevice)
(patient ?STEER ?VEHICLE))))
If education is an instance of educational process and person is a patient of education, then education has purpose "there exists learning learn so that person is a patient of learn".
(=>
(and
(instance ?EDUCATION EducationalProcess)
(patient ?EDUCATION ?PERSON))
(hasPurpose
?EDUCATION
(exists
(?LEARN)
(and
(instance ?LEARN Learning)
(patient ?LEARN ?PERSON)))))
If change is an instance of change of possession and obj is a patient of change and agent1 posesses obj immediately before "the time of existence of change" and agent2 posesses obj immediately after "the time of existence of change", then agent1 is not equal to agent2.
(=>
(and
(instance ?CHANGE ChangeOfPossession)
(patient ?CHANGE ?OBJ)
(holdsDuring
(ImmediatePastFn
(WhenFn ?CHANGE))
(possesses ?AGENT1 ?OBJ))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?CHANGE))
(possesses ?AGENT2 ?OBJ)))
(not
(equal ?AGENT1 ?AGENT2)))
If change is an instance of change of possession and change origins at agent1 and change ends at agent2 and agent2 is an instance of agent and obj is a patient of change, then agent1 posesses obj immediately before "the time of existence of change" and agent2 posesses obj immediately after "the time of existence of change".
(=>
(and
(instance ?CHANGE ChangeOfPossession)
(origin ?CHANGE ?AGENT1)
(destination ?CHANGE ?AGENT2)
(instance ?AGENT2 Agent)
(patient ?CHANGE ?OBJ))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?CHANGE))
(possesses ?AGENT1 ?OBJ))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?CHANGE))
(possesses ?AGENT2 ?OBJ))))
If give is an instance of giving and give is an agent of agent1 and give ends at agent2 and agent2 is an instance of agent and obj is a patient of give, then there exists getting get so that get is an agent of agent2 and get origins at agent1 and obj is a patient of get.
(=>
(and
(instance ?GIVE Giving)
(agent ?GIVE ?AGENT1)
(destination ?GIVE ?AGENT2)
(instance ?AGENT2 Agent)
(patient ?GIVE ?OBJ))
(exists
(?GET)
(and
(instance ?GET Getting)
(agent ?GET ?AGENT2)
(origin ?GET ?AGENT1)
(patient ?GET ?OBJ))))
If give is an instance of giving and give is an agent of agent, then give origins at agent.
(=>
(and
(instance ?GIVE Giving)
(agent ?GIVE ?AGENT))
(origin ?GIVE ?AGENT))
If give is an instance of unilateral giving, then there doesn't exist transaction trans so that give is a subprocess of trans.
(=>
(instance ?GIVE UnilateralGiving)
(not
(exists
(?TRANS)
(and
(instance ?TRANS Transaction)
(subProcess ?GIVE ?TRANS)))))
There exists borrowing borrow so that borrow is an agent of agent1 and borrow origins at agent2 and object is a patient of borrow if and only if there exists lending lend so that lend is an agent of agent2 and lend ends at agent1 and object is a patient of lend.
(<=>
(exists
(?BORROW)
(and
(instance ?BORROW Borrowing)
(agent ?BORROW ?AGENT1)
(origin ?BORROW ?AGENT2)
(patient ?BORROW ?OBJECT)))
(exists
(?LEND)
(and
(instance ?LEND Lending)
(agent ?LEND ?AGENT2)
(destination ?LEND ?AGENT1)
(patient ?LEND ?OBJECT))))
If get is an instance of getting and get is an agent of agent, then get ends at agent.
(=>
(and
(instance ?GET Getting)
(agent ?GET ?AGENT))
(destination ?GET ?AGENT))
If get is an instance of unilateral getting, then there doesn't exist transaction trans so that get is a subprocess of trans.
(=>
(instance ?GET UnilateralGetting)
(not
(exists
(?TRANS)
(and
(instance ?TRANS Transaction)
(subProcess ?GET ?TRANS)))))
If trans is an instance of transaction, then there exist agent1,agent2,giving give1,giving give2,obj1,obj2 so that give1 is a subprocess of trans and give2 is a subprocess of trans and give1 is an agent of agent1 and give2 is an agent of agent2 and obj1 is a patient of give1 and obj2 is a patient of give2 and give1 ends at agent2 and give2 ends at agent1 and agent1 is not equal to agent2 and obj1 is not equal to obj2.
(=>
(instance ?TRANS Transaction)
(exists
(?AGENT1 ?AGENT2 ?GIVE1 ?GIVE2 ?OBJ1 ?OBJ2)
(and
(instance ?GIVE1 Giving)
(instance ?GIVE2 Giving)
(subProcess ?GIVE1 ?TRANS)
(subProcess ?GIVE2 ?TRANS)
(agent ?GIVE1 ?AGENT1)
(agent ?GIVE2 ?AGENT2)
(patient ?GIVE1 ?OBJ1)
(patient ?GIVE2 ?OBJ2)
(destination ?GIVE1 ?AGENT2)
(destination ?GIVE2 ?AGENT1)
(not
(equal ?AGENT1 ?AGENT2))
(not
(equal ?OBJ1 ?OBJ2)))))
If trans is an instance of financial transaction, then there exists currency measure obj so that obj is a patient of trans.
(=>
(instance ?TRANS FinancialTransaction)
(exists
(?OBJ)
(and
(patient ?TRANS ?OBJ)
(instance ?OBJ CurrencyMeasure))))
If buy is an instance of buying and buy is an agent of agent, then buy ends at agent.
(=>
(and
(instance ?BUY Buying)
(agent ?BUY ?AGENT))
(destination ?BUY ?AGENT))
There exists buying buy so that buy is an agent of agent1 and buy origins at agent2 and object is a patient of buy if and only if there exists selling sell so that sell is an agent of agent2 and sell ends at agent1 and object is a patient of sell.
(<=>
(exists
(?BUY)
(and
(instance ?BUY Buying)
(agent ?BUY ?AGENT1)
(origin ?BUY ?AGENT2)
(patient ?BUY ?OBJECT)))
(exists
(?SELL)
(and
(instance ?SELL Selling)
(agent ?SELL ?AGENT2)
(destination ?SELL ?AGENT1)
(patient ?SELL ?OBJECT))))
If sell is an instance of selling and sell is an agent of agent, then sell origins at agent.
(=>
(and
(instance ?SELL Selling)
(agent ?SELL ?AGENT))
(origin ?SELL ?AGENT))
If learn is an instance of learning and learn is an agent of agent, then agent is an instance of cognitive agent.
(=>
(and
(instance ?LEARN Learning)
(agent ?LEARN ?AGENT))
(instance ?AGENT CognitiveAgent))
If there exists learning learn so that learn is an agent of agent and prop is a patient of learn during time, then agent believes prop immediately after time.
(=>
(holdsDuring
?TIME
(exists
(?LEARN)
(and
(instance ?LEARN Learning)
(agent ?LEARN ?AGENT)
(patient ?LEARN ?PROP))))
(holdsDuring
(ImmediateFutureFn ?TIME)
(believes ?AGENT ?PROP)))
If meas is an instance of measuring and meas is an agent of agent and obj is a patient of meas, then there exist quant,unit so that agent knows "the measure of obj is "quant unit(s)"" immediately after "the time of existence of meas".
(=>
(and
(instance ?MEAS Measuring)
(agent ?MEAS ?AGENT)
(patient ?MEAS ?OBJ))
(exists
(?QUANT ?UNIT)
(holdsDuring
(ImmediateFutureFn
(WhenFn ?MEAS))
(knows
?AGENT
(measure
?OBJ
(MeasureFn ?QUANT ?UNIT))))))
If count is an instance of counting and count is an agent of agent and entity is a patient of count, then there exists number so that agent knows ""the number of instances in entity" is equal to number".
(=>
(and
(instance ?COUNT Counting)
(agent ?COUNT ?AGENT)
(patient ?COUNT ?ENTITY))
(exists
(?NUMBER)
(knows
?AGENT
(equal
(CardinalityFn ?ENTITY)
?NUMBER))))
If predict is an instance of predicting and formula is a patient of predict, then there exists time so that formula holds during time and time happen?{s} before "the time of existence of predict" or time happens earlier than "the time of existence of predict".
(=>
(and
(instance ?PREDICT Predicting)
(patient ?PREDICT ?FORMULA))
(exists
(?TIME)
(and
(holdsDuring ?TIME ?FORMULA)
(or
(before
?TIME
(WhenFn ?PREDICT))
(earlier
?TIME
(WhenFn ?PREDICT))))))
If remember is an instance of remembering and formula is a patient of remember, then there exists time so that formula holds during time and time happen?{s} before "the time of existence of remember" or time happens earlier than "the time of existence of remember".
(=>
(and
(instance ?REMEMBER Remembering)
(patient ?REMEMBER ?FORMULA))
(exists
(?TIME)
(and
(holdsDuring ?TIME ?FORMULA)
(or
(before
?TIME
(WhenFn ?REMEMBER))
(earlier
?TIME
(WhenFn ?REMEMBER))))))
If keep is an instance of keeping and keep is an agent of agent and obj is a patient of keep, then there exists putting put so that put is an agent of agent and obj is a patient of put and "the time of existence of put" happens earlier than "the time of existence of keep".
(=>
(and
(instance ?KEEP Keeping)
(agent ?KEEP ?AGENT)
(patient ?KEEP ?OBJ))
(exists
(?PUT)
(and
(instance ?PUT Putting)
(agent ?PUT ?AGENT)
(patient ?PUT ?OBJ)
(earlier
(WhenFn ?PUT)
(WhenFn ?KEEP)))))
(=>
(and
(instance ?KEEP Keeping)
(patient ?KEEP ?OBJ))
(exists
(?PLACE)
(forall
(?TIME)
(=>
(temporalPart
?TIME
(WhenFn ?KEEP))
(holdsDuring
?TIME
(located ?OBJ ?PLACE))))))
If confine is an instance of confining, then there exists human human so that human is a patient of confine.
(=>
(instance ?CONFINE Confining)
(exists
(?HUMAN)
(and
(instance ?HUMAN Human)
(patient ?CONFINE ?HUMAN))))
If confine is an instance of confining and person is a patient of confine, then person doesn't desire "person is a patient of confine".
(=>
(and
(instance ?CONFINE Confining)
(patient ?CONFINE ?PERSON))
(not
(desires
?PERSON
(patient ?CONFINE ?PERSON))))
If repair is an instance of repairing and obj is a patient of repair, then there exists damaging damage so that obj is a patient of damage and "the time of existence of damage" happens earlier than "the time of existence of repair".
(=>
(and
(instance ?REPAIR Repairing)
(patient ?REPAIR ?OBJ))
(exists
(?DAMAGE)
(and
(instance ?DAMAGE Damaging)
(patient ?DAMAGE ?OBJ)
(earlier
(WhenFn ?DAMAGE)
(WhenFn ?REPAIR)))))
If proc is an instance of therapeutic process and bio is a patient of proc, then
(=>
(and
(instance ?PROC TherapeuticProcess)
(patient ?PROC ?BIO))
(or
(instance ?BIO Organism)
(exists
(?ORG)
(and
(instance ?ORG Organism)
(part ?BIO ?ORG)))))
If act is an instance of surgery and animal is a patient of act, then there exists cutting subact so that animal is an instance of animal and cutting is a patient of animal and subact is a subprocess of act.
(=>
(and
(instance ?ACT Surgery)
(patient ?ACT ?ANIMAL))
(exists
(?SUBACT)
(and
(instance ?SUBACT Cutting)
(instance ?ANIMAL Animal)
(patient ?ANIMAL ?CUTTING)
(subProcess ?SUBACT ?ACT))))
process is an instance of destruction if and only if there exists patient so that patient is a patient of process and patient exists during "immediately before "the time of existence of process"" and patient doesn't exist during "immediately after "the time of existence of process"".
(<=>
(instance ?PROCESS Destruction)
(exists
(?PATIENT)
(and
(patient ?PROCESS ?PATIENT)
(time
?PATIENT
(ImmediatePastFn
(WhenFn ?PROCESS)))
(not
(time
?PATIENT
(ImmediateFutureFn
(WhenFn ?PROCESS)))))))
If kill is an instance of killing and kill is an agent of agent and patient is a patient of kill, then agent is an instance of organism and patient is an instance of organism.
(=>
(and
(instance ?KILL Killing)
(agent ?KILL ?AGENT)
(patient ?KILL ?PATIENT))
(and
(instance ?AGENT Organism)
(instance ?PATIENT Organism)))
If kill is an instance of killing and patient is a patient of kill, then living is an attribute of patient immediately before "the time of existence of kill" and dead is an attribute of patient after "the time of existence of kill".
(=>
(and
(instance ?KILL Killing)
(patient ?KILL ?PATIENT))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?KILL))
(attribute ?PATIENT Living))
(holdsDuring
(FutureFn
(WhenFn ?KILL))
(attribute ?PATIENT Dead))))
If poke is an instance of poking and poke is an agent of agent and obj is a patient of poke and inst is an instrument for poke, then inst connects agent and obj the time of existence of poke.
(=>
(and
(instance ?POKE Poking)
(agent ?POKE ?AGENT)
(patient ?POKE ?OBJ)
(instrument ?POKE ?INST))
(holdsDuring
(WhenFn ?POKE)
(connects ?INST ?AGENT ?OBJ)))
If attach is an instance of attaching and obj1 is a patient of attach and obj2 is a patient of attach, then obj1 is not connected to obj2 immediately before "the time of existence of attach" and obj1 is connected to obj2 immediately after "the time of existence of attach".
(=>
(and
(instance ?ATTACH Attaching)
(patient ?ATTACH ?OBJ1)
(patient ?ATTACH ?OBJ2))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?ATTACH))
(not
(connected ?OBJ1 ?OBJ2)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ATTACH))
(connected ?OBJ1 ?OBJ2))))
If detach is an instance of detaching and obj1 is a patient of detach and obj2 is a patient of detach, then obj1 is connected to obj2 immediately before "the time of existence of detach" and obj1 is not connected to obj2 immediately after "the time of existence of detach".
(=>
(and
(instance ?DETACH Detaching)
(patient ?DETACH ?OBJ1)
(patient ?DETACH ?OBJ2))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?DETACH))
(connected ?OBJ1 ?OBJ2))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?DETACH))
(not
(connected ?OBJ1 ?OBJ2)))))
combine is an instance of combining and obj1 is a resource for combine and obj2 is a result of combine if and only if obj1 is not a part of obj2 immediately before "the time of existence of combine" and obj1 is a part of obj2 immediately after "the time of existence of combine".
(<=>
(and
(instance ?COMBINE Combining)
(resource ?COMBINE ?OBJ1)
(result ?COMBINE ?OBJ2))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?COMBINE))
(not
(part ?OBJ1 ?OBJ2)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?COMBINE))
(part ?OBJ1 ?OBJ2))))
If , then stuff is an instance of pure substance.
(=>
(and
(instance ?PROC ChemicalProcess)
(or
(resource ?PROC ?STUFF)
(result ?PROC ?STUFF)))
(instance ?STUFF PureSubstance))
If substance1 is a resource for proc and substance2 is a result of proc and substance1 is an instance of elemental substance and substance2 is an instance of compound substance, then proc is an instance of chemical synthesis.
(=>
(and
(resource ?PROC ?SUBSTANCE1)
(result ?PROC ?SUBSTANCE2)
(instance ?SUBSTANCE1 ElementalSubstance)
(instance ?SUBSTANCE2 CompoundSubstance))
(instance ?PROC ChemicalSynthesis))
compound is an instance of compound substance if and only if there exist elemental substance element1,elemental substance element2,chemical synthesis process so that element1 is not equal to element2 and element1 is a resource for process and element2 is a resource for process and compound is a result of process.
(<=>
(instance ?COMPOUND CompoundSubstance)
(exists
(?ELEMENT1 ?ELEMENT2 ?PROCESS)
(and
(instance ?ELEMENT1 ElementalSubstance)
(instance ?ELEMENT2 ElementalSubstance)
(not
(equal ?ELEMENT1 ?ELEMENT2))
(instance ?PROCESS ChemicalSynthesis)
(resource ?PROCESS ?ELEMENT1)
(resource ?PROCESS ?ELEMENT2)
(result ?PROCESS ?COMPOUND))))
If substance1 is a resource for proc and substance2 is a result of proc and substance1 is an instance of compound substance and substance2 is an instance of elemental substance, then proc is an instance of chemical decomposition.
(=>
(and
(resource ?PROC ?SUBSTANCE1)
(result ?PROC ?SUBSTANCE2)
(instance ?SUBSTANCE1 CompoundSubstance)
(instance ?SUBSTANCE2 ElementalSubstance))
(instance ?PROC ChemicalDecomposition))
If combustion is an instance of combustion, then there exist heating heat,radiating light light so that heat is a subprocess of combustion and light is a subprocess of combustion.
(=>
(instance ?COMBUSTION Combustion)
(exists
(?HEAT ?LIGHT)
(and
(instance ?HEAT Heating)
(instance ?LIGHT RadiatingLight)
(subProcess ?HEAT ?COMBUSTION)
(subProcess ?LIGHT ?COMBUSTION))))
If change is an instance of internal change and obj is a patient of change, then there exists property so that
(=>
(and
(instance ?CHANGE InternalChange)
(patient ?CHANGE ?OBJ))
(exists
(?PROPERTY)
(or
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?CHANGE))
(attribute ?OBJ ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?CHANGE))
(not
(attribute ?OBJ ?PROPERTY))))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?CHANGE))
(not
(attribute ?OBJ ?PROPERTY)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?CHANGE))
(attribute ?OBJ ?PROPERTY))))))
If alt is an instance of surface change and obj is a patient of alt, then there exist part,property so that part is a superficial part of obj and property is an attribute of part immediately before "the time of existence of alt" and property is not an attribute of part immediately after "the time of existence of alt".
(=>
(and
(instance ?ALT SurfaceChange)
(patient ?ALT ?OBJ))
(exists
(?PART ?PROPERTY)
(and
(superficialPart ?PART ?OBJ)
(holdsDuring
(ImmediatePastFn
(WhenFn ?ALT))
(attribute ?PART ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ALT))
(not
(attribute ?PART ?PROPERTY))))))
If alt is an instance of shape change and obj is a patient of alt, then there exists shape attribute property so that
(=>
(and
(instance ?ALT ShapeChange)
(patient ?ALT ?OBJ))
(exists
(?PROPERTY)
(and
(instance ?PROPERTY ShapeAttribute)
(or
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?ALT))
(attribute ?OBJ ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ALT))
(not
(attribute ?OBJ ?PROPERTY))))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?ALT))
(not
(attribute ?OBJ ?PROPERTY)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ALT))
(attribute ?OBJ ?PROPERTY)))))))
If coloring is an instance of coloring and obj is a patient of coloring, then there exists color attribute property so that property is an attribute of obj immediately before "the time of existence of coloring" and property is not an attribute of obj immediately after "the time of existence of coloring".
(=>
(and
(instance ?COLORING Coloring)
(patient ?COLORING ?OBJ))
(exists
(?PROPERTY)
(and
(instance ?PROPERTY ColorAttribute)
(holdsDuring
(ImmediatePastFn
(WhenFn ?COLORING))
(attribute ?OBJ ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?COLORING))
(not
(attribute ?OBJ ?PROPERTY))))))
If develop is an instance of content development, then there exists content bearing object obj so that obj is a patient of develop.
(=>
(instance ?DEVELOP ContentDevelopment)
(exists
(?OBJ)
(and
(instance ?OBJ ContentBearingObject)
(patient ?DEVELOP ?OBJ))))
If read is an instance of reading, then there exist text text,prop so that text contains information prop and read expresses the content of prop.
(=>
(instance ?READ Reading)
(exists
(?TEXT ?PROP)
(and
(instance ?TEXT Text)
(containsInformation ?TEXT ?PROP)
(realization ?READ ?PROP))))
If decode is an instance of decoding and doc1 is a patient of decode, then there exist encode,doc2,time so that doc2 contains information prop and doc1 contains information prop and time is a part of "before "the time of existence of decode"" and encode is an instance of encoding and doc2 is a patient of encode during time.
(=>
(and
(instance ?DECODE Decoding)
(patient ?DECODE ?DOC1))
(exists
(?ENCODE ?DOC2 ?TIME)
(and
(containsInformation ?DOC2 ?PROP)
(containsInformation ?DOC1 ?PROP)
(temporalPart
?TIME
(PastFn
(WhenFn ?DECODE)))
(holdsDuring
?TIME
(and
(instance ?ENCODE Encoding)
(patient ?ENCODE ?DOC2))))))
If wet is an instance of wetting and obj is a patient of wet, then wet is an attribute of obj or damp is an attribute of obj immediately after "the time of existence of wet".
(=>
(and
(instance ?WET Wetting)
(patient ?WET ?OBJ))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?WET))
(or
(attribute ?OBJ Wet)
(attribute ?OBJ Damp))))
If wet is an instance of wetting, then there exists obj so that liquid is an attribute of obj and obj is a patient of wet.
(=>
(instance ?WET Wetting)
(exists
(?OBJ)
(and
(attribute ?OBJ Liquid)
(patient ?WET ?OBJ))))
If dry is an instance of drying and obj is a patient of dry, then dry is an attribute of obj immediately after "the time of existence of dry".
(=>
(and
(instance ?DRY Drying)
(patient ?DRY ?OBJ))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?DRY))
(attribute ?OBJ Dry)))
process is an instance of creation if and only if there exists patient so that patient is a patient of process and patient exists during "immediately after "the time of existence of process"" and patient doesn't exist during "immediately before "the time of existence of process"".
(<=>
(instance ?PROCESS Creation)
(exists
(?PATIENT)
(and
(patient ?PROCESS ?PATIENT)
(time
?PATIENT
(ImmediateFutureFn
(WhenFn ?PROCESS)))
(not
(time
?PATIENT
(ImmediatePastFn
(WhenFn ?PROCESS)))))))
There exists constructing build so that artifact is a result of build if and only if artifact is an instance of stationary artifact.
(<=>
(exists
(?BUILD)
(and
(instance ?BUILD Constructing)
(result ?BUILD ?ARTIFACT)))
(instance ?ARTIFACT StationaryArtifact))
If pub is an instance of publication and text is a patient of pub, then text is a subclass of text.
(=>
(and
(instance ?PUB Publication)
(patient ?PUB ?TEXT))
(subclass ?TEXT Text))
If cook is an instance of cooking, then there exists food food so that food is a result of cook.
(=>
(instance ?COOK Cooking)
(exists
(?FOOD)
(and
(instance ?FOOD Food)
(result ?COOK ?FOOD))))
If search is an instance of searching and search is an agent of agent and entity is a patient of search, then agent is interested in entity.
(=>
(and
(instance ?SEARCH Searching)
(agent ?SEARCH ?AGENT)
(patient ?SEARCH ?ENTITY))
(inScopeOfInterest ?AGENT ?ENTITY))
If pursue is an instance of pursuing and pursue is an agent of agent and obj is a patient of pursue, then agent wants obj during pursue.
(=>
(and
(instance ?PURSUE Pursuing)
(agent ?PURSUE ?AGENT)
(patient ?PURSUE ?OBJ))
(holdsDuring
?PURSUE
(wants ?AGENT ?OBJ)))
If pursue is an instance of pursuing and pursue is an agent of agent and obj is a patient of pursue, then agent doesn't posess obj during pursue.
(=>
(and
(instance ?PURSUE Pursuing)
(agent ?PURSUE ?AGENT)
(patient ?PURSUE ?OBJ))
(holdsDuring
?PURSUE
(not
(possesses ?AGENT ?OBJ))))
If investigate is an instance of investigating and prop is a patient of investigate, then prop is an instance of formula.
(=>
(and
(instance ?INVESTIGATE Investigating)
(patient ?INVESTIGATE ?PROP))
(instance ?PROP Formula))
If investigate is an instance of investigating and investigate is an agent of agent and prop is a patient of investigate, then agent doesn't know prop the time of existence of investigate.
(=>
(and
(instance ?INVESTIGATE Investigating)
(agent ?INVESTIGATE ?AGENT)
(patient ?INVESTIGATE ?PROP))
(holdsDuring
(WhenFn ?INVESTIGATE)
(not
(knows ?AGENT ?PROP))))
If proc is an instance of diagnostic process and proc is an agent of agent, then there exists cause so that proc has &n purpose "agent knows "cause causes proc"" for agent.
(=>
(and
(instance ?PROC DiagnosticProcess)
(agent ?PROC ?AGENT))
(exists
(?CAUSE)
(hasPurposeForAgent
?PROC
(knows
?AGENT
(causes ?CAUSE ?PROC))
?AGENT)))
If interaction is an instance of social interaction, then there exist agent1,agent2 so that interaction is an agent of agent1 and interaction is an agent of agent2 and agent1 is not equal to agent2.
(=>
(instance ?INTERACTION SocialInteraction)
(exists
(?AGENT1 ?AGENT2)
(and
(agent ?INTERACTION ?AGENT1)
(agent ?INTERACTION ?AGENT2)
(not
(equal ?AGENT1 ?AGENT2)))))
If pretend is an instance of pretending, then there exist person,prop so that pretend has purpose "person believes prop" and prop is true.
(=>
(instance ?PRETEND Pretending)
(exists
(?PERSON ?PROP)
(and
(hasPurpose
?PRETEND
(believes ?PERSON ?PROP))
(true ?PROP True))))
If communicate is an instance of communication, then there exist content bearing object obj,cognitive agent agent1,cognitive agent agent2 so that obj is a patient of communicate and communicate is an agent of agent1 and communicate ends at agent2.
(=>
(instance ?COMMUNICATE Communication)
(exists
(?OBJ ?AGENT1 ?AGENT2)
(and
(instance ?OBJ ContentBearingObject)
(patient ?COMMUNICATE ?OBJ)
(instance ?AGENT1 CognitiveAgent)
(agent ?COMMUNICATE ?AGENT1)
(instance ?AGENT2 CognitiveAgent)
(destination ?COMMUNICATE ?AGENT2))))
If disseminate is an instance of disseminating, then there exist cognitive agent agent1,cognitive agent agent2 so that disseminate ends at agent1 and disseminate ends at agent2 and agent1 is not equal to agent2.
(=>
(instance ?DISSEMINATE Disseminating)
(exists
(?AGENT1 ?AGENT2)
(and
(destination ?DISSEMINATE ?AGENT1)
(instance ?AGENT1 CognitiveAgent)
(destination ?DISSEMINATE ?AGENT2)
(instance ?AGENT2 CognitiveAgent)
(not
(equal ?AGENT1 ?AGENT2)))))
If advert is an instance of advertising, then there exists obj so that advert includes a reference to obj and advert has purpose "there exists selling sale so that obj is a patient of sale".
(=>
(instance ?ADVERT Advertising)
(exists
(?OBJ)
(and
(refers ?ADVERT ?OBJ)
(hasPurpose
?ADVERT
(exists
(?SALE)
(and
(instance ?SALE Selling)
(patient ?SALE ?OBJ)))))))
If communicate is an instance of linguistic communication, then there exists linguistic expression obj so that obj is a patient of communicate.
(=>
(instance ?COMMUNICATE LinguisticCommunication)
(exists
(?OBJ)
(and
(instance ?OBJ LinguisticExpression)
(patient ?COMMUNICATE ?OBJ))))
If state is an instance of stating and state is an agent of agent and formula is a patient of state and formula is an instance of formula, then agent believes formula the time of existence of state.
(=>
(and
(instance ?STATE Stating)
(agent ?STATE ?AGENT)
(patient ?STATE ?FORMULA)
(instance ?FORMULA Formula))
(holdsDuring
(WhenFn ?STATE)
(believes ?AGENT ?FORMULA)))
If order is an instance of ordering and formula is a patient of order, then the statement formula has the model force of obligation.
(=>
(and
(instance ?ORDER Ordering)
(patient ?ORDER ?FORMULA))
(modalAttribute ?FORMULA Obligation))
If request is an instance of requesting and request is an agent of agent and formula is a patient of request and formula is an instance of formula, then agent desires formula.
(=>
(and
(instance ?REQUEST Requesting)
(agent ?REQUEST ?AGENT)
(patient ?REQUEST ?FORMULA)
(instance ?FORMULA Formula))
(desires ?AGENT ?FORMULA))
If question is an instance of questioning and question is an agent of agent and formula is a patient of question and formula is an instance of formula, then agent doesn't know formula the time of existence of question.
(=>
(and
(instance ?QUESTION Questioning)
(agent ?QUESTION ?AGENT)
(patient ?QUESTION ?FORMULA)
(instance ?FORMULA Formula))
(holdsDuring
(WhenFn ?QUESTION)
(not
(knows ?AGENT ?FORMULA))))
If commit is an instance of committing and formula is a patient of commit and formula is an instance of formula, then the statement formula has the model force of promise.
(=>
(and
(instance ?COMMIT Committing)
(patient ?COMMIT ?FORMULA)
(instance ?FORMULA Formula))
(modalAttribute ?FORMULA Promise))
If express is an instance of expressing and express is an agent of agent, then there exists state of mind state so that state is an attribute of agent and express expresses state.
(=>
(and
(instance ?EXPRESS Expressing)
(agent ?EXPRESS ?AGENT))
(exists
(?STATE)
(and
(instance ?STATE StateOfMind)
(attribute ?AGENT ?STATE)
(represents ?EXPRESS ?STATE))))
If declare is an instance of declaring and declare is an agent of agent1, then there exist proc,agent2 so that declare allows agent2 to perform task of the type proc or declare obligates agent2 to perform task of the type proc.
(=>
(and
(instance ?DECLARE Declaring)
(agent ?DECLARE ?AGENT1))
(exists
(?PROC ?AGENT2)
(or
(confersRight ?PROC ?DECLARE ?AGENT2)
(confersObligation ?PROC ?DECLARE ?AGENT2))))
If meet is an instance of meeting and meet is an agent of agent1 and meet is an agent of agent2, then agent1 is near to agent2 the time of existence of meet.
(=>
(and
(instance ?MEET Meeting)
(agent ?MEET ?AGENT1)
(agent ?MEET ?AGENT2))
(holdsDuring
(WhenFn ?MEET)
(orientation ?AGENT1 ?AGENT2 Near)))
If meet is an instance of meeting, then there exist agent1,agent2 so that meet is an agent of agent1 and meet is an agent of agent2 and meet has purpose "there exists communication comm so that comm is an agent of agent1 and comm is an agent of agent2".
(=>
(instance ?MEET Meeting)
(exists
(?AGENT1 ?AGENT2)
(and
(agent ?MEET ?AGENT1)
(agent ?MEET ?AGENT2)
(hasPurpose
?MEET
(exists
(?COMM)
(and
(instance ?COMM Communication)
(agent ?COMM ?AGENT1)
(agent ?COMM ?AGENT2)))))))
If contest is an instance of contest, then there exist agent1,agent2,purp1,purp2 so that contest is an agent of agent1 and contest is an agent of agent2 and contest has &n purpose purp1 for agent1 and contest has &n purpose purp2 for agent2 and agent1 is not equal to agent2 and purp1 is not equal to purp2.
(=>
(instance ?CONTEST Contest)
(exists
(?AGENT1 ?AGENT2 ?PURP1 ?PURP2)
(and
(agent ?CONTEST ?AGENT1)
(agent ?CONTEST ?AGENT2)
(hasPurposeForAgent ?CONTEST ?PURP1 ?AGENT1)
(hasPurposeForAgent ?CONTEST ?PURP2 ?AGENT2)
(not
(equal ?AGENT1 ?AGENT2))
(not
(equal ?PURP1 ?PURP2)))))
If war is an instance of war, then there exists battle battle so that battle is a subprocess of war.
(=>
(instance ?WAR War)
(exists
(?BATTLE)
(and
(instance ?BATTLE Battle)
(subProcess ?BATTLE ?WAR))))
(=>
(and
(instance ?WAR War)
(agent ?WAR ?AGENT))
(or
(instance ?AGENT Nation)
(and
(instance ?AGENT Organization)
(forall
(?MEMBER)
(=>
(member ?MEMBER ?AGENT)
(instance ?MEMBER Nation))))))
If battle is an instance of battle, then there exists war war so that battle is a subprocess of war.
(=>
(instance ?BATTLE Battle)
(exists
(?WAR)
(and
(instance ?WAR War)
(subProcess ?BATTLE ?WAR))))
If battle is an instance of battle, then there exists violent contest attack so that attack is a subprocess of battle.
(=>
(instance ?BATTLE Battle)
(exists
(?ATTACK)
(and
(instance ?ATTACK ViolentContest)
(subProcess ?ATTACK ?BATTLE))))
If move is an instance of maneuver, then there exists contest contest so that move is a subprocess of contest.
(=>
(instance ?MOVE Maneuver)
(exists
(?CONTEST)
(and
(instance ?CONTEST Contest)
(subProcess ?MOVE ?CONTEST))))
If percept is an instance of perception and percept is an agent of agent, then agent is an instance of animal.
(=>
(and
(instance ?PERCEPT Perception)
(agent ?PERCEPT ?AGENT))
(instance ?AGENT Animal))
If percept is an instance of perception and percept is an agent of agent and object is a patient of percept, then agent notices object.
(=>
(and
(instance ?PERCEPT Perception)
(agent ?PERCEPT ?AGENT)
(patient ?PERCEPT ?OBJECT))
(notices ?AGENT ?OBJECT))
If see is an instance of seeing and see is an agent of agent and obj is a patient of see, then
(=>
(and
(instance ?SEE Seeing)
(agent ?SEE ?AGENT)
(patient ?SEE ?OBJ))
(and
(attribute ?OBJ Illuminated)
(exists
(?PROP)
(and
(instance ?PROP ColorAttribute)
(knows
?AGENT
(attribute ?OBJ ?PROP))))))
If smell is an instance of smelling and obj is a patient of smell, then there exists olfactory attribute attr so that attr is an attribute of obj.
(=>
(and
(instance ?SMELL Smelling)
(patient ?SMELL ?OBJ))
(exists
(?ATTR)
(and
(instance ?ATTR OlfactoryAttribute)
(attribute ?OBJ ?ATTR))))
If taste is an instance of tasting and obj is a patient of taste, then there exists taste attribute attr so that attr is an attribute of obj.
(=>
(and
(instance ?TASTE Tasting)
(patient ?TASTE ?OBJ))
(exists
(?ATTR)
(and
(instance ?ATTR TasteAttribute)
(attribute ?OBJ ?ATTR))))
If hear is an instance of hearing and obj is a patient of hear, then there exists sound attribute attr so that attr is an attribute of obj.
(=>
(and
(instance ?HEAR Hearing)
(patient ?HEAR ?OBJ))
(exists
(?ATTR)
(and
(instance ?ATTR SoundAttribute)
(attribute ?OBJ ?ATTR))))
If tactile is an instance of tactile perception, then there exists touching touch so that touch is a subprocess of tactile.
(=>
(instance ?TACTILE TactilePerception)
(exists
(?TOUCH)
(and
(instance ?TOUCH Touching)
(subProcess ?TOUCH ?TACTILE))))
There exists radiating light emit so that region is a patient of emit and region is an instance of region if and only if illuminated is an attribute of region.
(<=>
(exists
(?EMIT)
(and
(instance ?EMIT RadiatingLight)
(patient ?EMIT ?REGION)
(instance ?REGION Region)))
(attribute ?REGION Illuminated))
If emit is an instance of radiating sound and emit is an agent of sound, then there exists sound attribute attr so that attr is an attribute of sound.
(=>
(and
(instance ?EMIT RadiatingSound)
(agent ?EMIT ?SOUND))
(exists
(?ATTR)
(and
(instance ?ATTR SoundAttribute)
(attribute ?SOUND ?ATTR))))
If process is an instance of state change and obj is a patient of process, then there exist part,physical state state1,physical state state2 so that part is a part of obj and state1 is not equal to state2 and state1 is an attribute of part immediately before "the time of existence of process" and state2 is an attribute of part immediately after "the time of existence of freeze".
(=>
(and
(instance ?PROCESS StateChange)
(patient ?PROCESS ?OBJ))
(exists
(?PART ?STATE1 ?STATE2)
(and
(part ?PART ?OBJ)
(instance ?STATE1 PhysicalState)
(instance ?STATE2 PhysicalState)
(not
(equal ?STATE1 ?STATE2))
(holdsDuring
(ImmediatePastFn
(WhenFn ?PROCESS))
(attribute ?PART ?STATE1))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?FREEZE))
(attribute ?PART ?STATE2)))))
If melt is an instance of melting, then there exists heating heat so that heat is a subprocess of melt.
(=>
(instance ?MELT Melting)
(exists
(?HEAT)
(and
(instance ?HEAT Heating)
(subProcess ?HEAT ?MELT))))
If melt is an instance of melting and obj is a patient of melt, then there exists part so that part is a part of obj and solid is an attribute of part immediately before "the time of existence of melt" and liquid is an attribute of part immediately after "the time of existence of melt".
(=>
(and
(instance ?MELT Melting)
(patient ?MELT ?OBJ))
(exists
(?PART)
(and
(part ?PART ?OBJ)
(holdsDuring
(ImmediatePastFn
(WhenFn ?MELT))
(attribute ?PART Solid))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?MELT))
(attribute ?PART Liquid)))))
If boil is an instance of boiling, then there exists heating heat so that heat is a subprocess of boil.
(=>
(instance ?BOIL Boiling)
(exists
(?HEAT)
(and
(instance ?HEAT Heating)
(subProcess ?HEAT ?BOIL))))
If boil is an instance of boiling and obj is a patient of boil, then there exists part so that part is a part of obj and liquid is an attribute of part immediately before "the time of existence of boil" and gas is an attribute of part immediately after "the time of existence of boil".
(=>
(and
(instance ?BOIL Boiling)
(patient ?BOIL ?OBJ))
(exists
(?PART)
(and
(part ?PART ?OBJ)
(holdsDuring
(ImmediatePastFn
(WhenFn ?BOIL))
(attribute ?PART Liquid))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?BOIL))
(attribute ?PART Gas)))))
If cond is an instance of condensing, then there exists cooling cool so that cool is a subprocess of cond.
(=>
(instance ?COND Condensing)
(exists
(?COOL)
(and
(instance ?COOL Cooling)
(subProcess ?COOL ?COND))))
If cond is an instance of condensing and obj is a patient of cond, then there exists part so that part is a part of obj and gas is an attribute of part immediately before "the time of existence of cond" and liquid is an attribute of part immediately after "the time of existence of cond".
(=>
(and
(instance ?COND Condensing)
(patient ?COND ?OBJ))
(exists
(?PART)
(and
(part ?PART ?OBJ)
(holdsDuring
(ImmediatePastFn
(WhenFn ?COND))
(attribute ?PART Gas))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?COND))
(attribute ?PART Liquid)))))
If freeze is an instance of freezing, then there exists cooling cool so that cool is a subprocess of freeze.
(=>
(instance ?FREEZE Freezing)
(exists
(?COOL)
(and
(instance ?COOL Cooling)
(subProcess ?COOL ?FREEZE))))
If freeze is an instance of freezing and obj is a patient of freeze, then there exists part so that part is a part of obj and liquid is an attribute of part immediately before "the time of existence of freeze" and solid is an attribute of part immediately after "the time of existence of freeze".
(=>
(and
(instance ?FREEZE Freezing)
(patient ?FREEZE ?OBJ))
(exists
(?PART)
(and
(part ?PART ?OBJ)
(holdsDuring
(ImmediatePastFn
(WhenFn ?FREEZE))
(attribute ?PART Liquid))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?FREEZE))
(attribute ?PART Solid)))))
If area is an instance of water area, then there exist bed,hole,water water so that "the host of the hole hole" is equal to bed and water properly fills hole and "the union of the parts of bed and water" is equal to area.
(=>
(instance ?AREA WaterArea)
(exists
(?BED ?HOLE ?WATER)
(and
(equal
(PrincipalHostFn ?HOLE)
?BED)
(instance ?WATER Water)
(properlyFills ?WATER ?HOLE)
(equal
(MereologicalSumFn ?BED ?WATER)
?AREA))))
If land1 is an instance of land area, then there exists land2 so that land1 is a part of land2 and land2 is an instance of continent or land2 is an instance of island.
(=>
(instance ?LAND1 LandArea)
(exists
(?LAND2)
(and
(part ?LAND1 ?LAND2)
(or
(instance ?LAND2 Continent)
(instance ?LAND2 Island)))))
If island is an instance of island, then there don't exist land area area,part1,part2 so that part1 is a part of island and part2 is a part of area and island is not a part of area and area is not a part of island and part1 is connected to part2.
(=>
(instance ?ISLAND Island)
(not
(exists
(?AREA ?PART1 ?PART2)
(and
(instance ?AREA LandArea)
(part ?PART1 ?ISLAND)
(part ?PART2 ?AREA)
(not
(part ?ISLAND ?AREA))
(not
(part ?AREA ?ISLAND))
(connected ?PART1 ?PART2)))))
If state is an instance of state or province, then there exists nation land so that state is a properPart of land.
(=>
(instance ?STATE StateOrProvince)
(exists
(?LAND)
(and
(instance ?LAND Nation)
(properPart ?STATE ?LAND))))
If the developmental form of obj is attr1 during time1 and attr2 is a successor attribute of attr1, then there exists time2 so that time2 happens earlier than time1 and the developmental form of obj is attr2 during time2.
(=>
(and
(holdsDuring
?TIME1
(developmentalForm ?OBJ ?ATTR1))
(successorAttributeClosure ?ATTR2 ?ATTR1))
(exists
(?TIME2)
(and
(earlier ?TIME2 ?TIME1)
(holdsDuring
?TIME2
(developmentalForm ?OBJ ?ATTR2)))))
If organism is an instance of organism, then there exists birth birth so that organism experiences birth.
(=>
(instance ?ORGANISM Organism)
(exists
(?BIRTH)
(and
(instance ?BIRTH Birth)
(experiencer ?BIRTH ?ORGANISM))))
If parent is a parent of child and class is a subclass of organism and parent is an instance of class, then child is an instance of class.
(=>
(and
(parent ?CHILD ?PARENT)
(subclass ?CLASS Organism)
(instance ?PARENT ?CLASS))
(instance ?CHILD ?CLASS))
animal1 is a sibling of animal2 if and only if there exist father,mother so that father is a father of animal1 and father is a father of animal2 and mother is a mother of animal1 and mother is a mother of animal2.
(<=>
(sibling ?ANIMAL1 ?ANIMAL2)
(exists
(?FATHER ?MOTHER)
(and
(father ?ANIMAL1 ?FATHER)
(father ?ANIMAL2 ?FATHER)
(mother ?ANIMAL1 ?MOTHER)
(mother ?ANIMAL2 ?MOTHER))))
If alga is an instance of alga, then there exists water water so that alga lives in water.
(=>
(instance ?ALGA Alga)
(exists
(?WATER)
(and
(inhabits ?ALGA ?WATER)
(instance ?WATER Water))))
If fungus is an instance of fungus and fungus lives in obj, then obj is an instance of organism.
(=>
(and
(instance ?FUNGUS Fungus)
(inhabits ?FUNGUS ?OBJ))
(instance ?OBJ Organism))
(=>
(instance ?BACTERIUM Bacterium)
(exists
(?CELL1)
(and
(component ?CELL1 ?BACTERIUM)
(instance ?CELL1 Cell)
(forall
(?CELL2)
(=>
(and
(component ?CELL2 ?BACTERIUM)
(instance ?CELL2 Cell))
(equal ?CELL1 ?CELL2))))))
If bacterium is an instance of bacterium and bacterium lives in obj, then obj is an instance of organism.
(=>
(and
(instance ?BACTERIUM Bacterium)
(inhabits ?BACTERIUM ?OBJ))
(instance ?OBJ Organism))
(=>
(instance ?VIRUS Virus)
(exists
(?MOL1)
(and
(component ?MOL1 ?VIRUS)
(instance ?MOL1 Molecule)
(forall
(?MOL2)
(=>
(and
(component ?MOL2 ?VIRUS)
(instance ?MOL2 Molecule))
(equal ?MOL1 ?MOL2))))))
If virus is an instance of virus and virus lives in obj, then obj is an instance of organism.
(=>
(and
(instance ?VIRUS Virus)
(inhabits ?VIRUS ?OBJ))
(instance ?OBJ Organism))
If virus is an instance of virus and proc is an instance of replication and proc is an agent of virus, then there exists cell cell so that proc is located at cell.
(=>
(and
(instance ?VIRUS Virus)
(instance ?PROC Replication)
(agent ?PROC ?VIRUS))
(exists
(?CELL)
(and
(located ?PROC ?CELL)
(instance ?CELL Cell))))
If fish is an instance of fish, then there exists water water so that fish lives in water.
(=>
(instance ?FISH Fish)
(exists
(?WATER)
(and
(inhabits ?FISH ?WATER)
(instance ?WATER Water))))
If organism is an instance of toxic organism, then there exists biologically active substance substance so that substance is a part of organism.
(=>
(instance ?ORGANISM ToxicOrganism)
(exists
(?SUBSTANCE)
(and
(instance ?SUBSTANCE BiologicallyActiveSubstance)
(part ?SUBSTANCE ?ORGANISM))))
If food is an instance of food, then there exists nutrient nutrient so that nutrient is a part of food.
(=>
(instance ?FOOD Food)
(exists
(?NUTRIENT)
(and
(instance ?NUTRIENT Nutrient)
(part ?NUTRIENT ?FOOD))))
- if food is an instance of food,
- then for all part1 holds: if part1 is a part of food, then there exist part2,animal animal so that part1 is a part of part2 and part2 is a part of animal
.
(=>
(instance ?FOOD Food)
(forall
(?PART1)
(=>
(part ?PART1 ?FOOD)
(exists
(?PART2 ?ANIMAL)
(and
(part ?PART1 ?PART2)
(part ?PART2 ?ANIMAL)
(instance ?ANIMAL Animal))))))
- if meat is an instance of meat,
- then for all part holds: if part is a part of meat, then there exist subpart,time,animal so that subpart is a part of part and animal is an instance of animal and subpart is a part of animal during time
.
(=>
(instance ?MEAT Meat)
(forall
(?PART)
(=>
(part ?PART ?MEAT)
(exists
(?SUBPART ?TIME ?ANIMAL)
(and
(part ?SUBPART ?PART)
(holdsDuring
?TIME
(and
(instance ?ANIMAL Animal)
(part ?SUBPART ?ANIMAL))))))))
(=>
(instance ?VEG FruitOrVegetable)
(forall
(?PART)
(=>
(part ?PART ?VEG)
(exists
(?SUBPART ?TIME ?PLANT)
(and
(part ?SUBPART ?PART)
(holdsDuring
?TIME
(and
(instance ?PLANT Plant)
(part ?SUBPART ?PLANT))))))))
If drink is an instance of drinking and bev is a patient of drink, then bev is an instance of beverage.
(=>
(and
(instance ?DRINK Drinking)
(patient ?DRINK ?BEV))
(instance ?BEV Beverage))
If anat is an instance of anatomical structure, then there exists organism organism so that anat is a part of organism.
(=>
(instance ?ANAT AnatomicalStructure)
(exists
(?ORGANISM)
(and
(instance ?ORGANISM Organism)
(part ?ANAT ?ORGANISM))))
If part is an instance of anatomical structure, then there exists cell cell so that cell is a part of part.
(=>
(instance ?PART AnatomicalStructure)
(exists
(?CELL)
(and
(instance ?CELL Cell)
(part ?CELL ?PART))))
If part is an instance of body part, then there doesn't exist pathologic process proc so that part is a result of proc.
(=>
(instance ?PART BodyPart)
(not
(exists
(?PROC)
(and
(instance ?PROC PathologicProcess)
(result ?PROC ?PART)))))
If cover is an instance of body covering, then there exists body so that cover is a superficial part of body and body is an instance of organism or body is an instance of body part.
(=>
(instance ?COVER BodyCovering)
(exists
(?BODY)
(and
(superficialPart ?COVER ?BODY)
(or
(instance ?BODY Organism)
(instance ?BODY BodyPart)))))
If junct is an instance of body junction, then there exists body part struct so that junct is a component of struct.
(=>
(instance ?JUNCT BodyJunction)
(exists
(?STRUCT)
(and
(instance ?STRUCT BodyPart)
(component ?JUNCT ?STRUCT))))
If junct is an instance of body junction, then there exist body part struct1,body part struct2 so that junct is connected to struct1 and junct is connected to struct2 and struct1 is not equal to struct2.
(=>
(instance ?JUNCT BodyJunction)
(exists
(?STRUCT1 ?STRUCT2)
(and
(connected ?JUNCT ?STRUCT1)
(connected ?JUNCT ?STRUCT2)
(instance ?STRUCT1 BodyPart)
(instance ?STRUCT2 BodyPart)
(not
(equal ?STRUCT1 ?STRUCT2)))))
If stuff is an instance of tissue, then there exists cell part so that part is a part of stuff.
(=>
(instance ?STUFF Tissue)
(exists
(?PART)
(and
(instance ?PART Cell)
(part ?PART ?STUFF))))
If stuff is an instance of tissue, then there exists organism organism so that stuff is a part of organism.
(=>
(instance ?STUFF Tissue)
(exists
(?ORGANISM)
(and
(instance ?ORGANISM Organism)
(part ?STUFF ?ORGANISM))))
If bone is an instance of bone, then there exists vertebrate vert so that bone is a part of vert.
(=>
(instance ?BONE Bone)
(exists
(?VERT)
(and
(instance ?VERT Vertebrate)
(part ?BONE ?VERT))))
If morph is an instance of morpheme, then there doesn't exist morpheme othermorph so that othermorph is a part of morph and othermorph is not equal to morph.
(=>
(instance ?MORPH Morpheme)
(not
(exists
(?OTHERMORPH)
(and
(instance ?OTHERMORPH Morpheme)
(part ?OTHERMORPH ?MORPH)
(not
(equal ?OTHERMORPH ?MORPH))))))
If morph is an instance of morpheme, then there exists word word so that morph is a part of word.
(=>
(instance ?MORPH Morpheme)
(exists
(?WORD)
(and
(instance ?WORD Word)
(part ?MORPH ?WORD))))
If word is an instance of word, then there exists morpheme part so that part is a part of word.
(=>
(instance ?WORD Word)
(exists
(?PART)
(and
(part ?PART ?WORD)
(instance ?PART Morpheme))))
If phrase is an instance of phrase, then there exist word part1,word part2 so that part1 is a part of phrase and part2 is a part of phrase and part1 is not equal to part2.
(=>
(instance ?PHRASE Phrase)
(exists
(?PART1 ?PART2)
(and
(part ?PART1 ?PHRASE)
(part ?PART2 ?PHRASE)
(instance ?PART1 Word)
(instance ?PART2 Word)
(not
(equal ?PART1 ?PART2)))))
If sentence is an instance of sentence, then there exist noun phrase phrase1,verb phrase phrase2 so that phrase1 is a part of sentence and phrase2 is a part of sentence.
(=>
(instance ?SENTENCE Sentence)
(exists
(?PHRASE1 ?PHRASE2)
(and
(instance ?PHRASE1 NounPhrase)
(instance ?PHRASE2 VerbPhrase)
(part ?PHRASE1 ?SENTENCE)
(part ?PHRASE2 ?SENTENCE))))
If text is an instance of text, then there exists proposition prop so that text contains information prop.
(=>
(instance ?TEXT Text)
(exists
(?PROP)
(and
(instance ?PROP Proposition)
(containsInformation ?TEXT ?PROP))))
If text is an instance of text, then there exists sentence part so that part is a part of text.
(=>
(instance ?TEXT Text)
(exists
(?PART)
(and
(part ?PART ?TEXT)
(instance ?PART Sentence))))
If text is an instance of text, then there exists writing write so that text is a result of write.
(=>
(instance ?TEXT Text)
(exists
(?WRITE)
(and
(instance ?WRITE Writing)
(result ?WRITE ?TEXT))))
If sent is an instance of sentence, then there exist noun phrase noun,verb phrase verb so that noun is a part of sent and verb is a part of sent.
(=>
(instance ?SENT Sentence)
(exists
(?NOUN ?VERB)
(and
(instance ?NOUN NounPhrase)
(instance ?VERB VerbPhrase)
(part ?NOUN ?SENT)
(part ?VERB ?SENT))))
If agent is the author of text, then there exist process,text instance so that process is an agent of agent and text is a result of process.
(=>
(authors ?AGENT ?TEXT)
(exists
(?PROCESS ?INSTANCE)
(and
(agent ?PROCESS ?AGENT)
(instance ?INSTANCE ?TEXT)
(result ?PROCESS ?TEXT))))
org publishes text if and only if there exists publication pub so that pub is an agent of org and text is a patient of pub.
(<=>
(publishes ?ORG ?TEXT)
(exists
(?PUB)
(and
(instance ?PUB Publication)
(agent ?PUB ?ORG)
(patient ?PUB ?TEXT))))
If "edition int1 of text" is equal to edition1 and "edition int2 of text" is equal to edition2 and int2 is greater than int1 and pub1 is an instance of publication and pub2 is an instance of publication and edition1 is a patient of pub1 and edition2 is a patient of pub2 and date of pub1 is date1 and date of pub2 is date2, then "the end of date1" happen?{s} before "the end of date2".
(=>
(and
(equal
(EditionFn ?TEXT ?INT1)
?EDITION1)
(equal
(EditionFn ?TEXT ?INT2)
?EDITION2)
(greaterThan ?INT2 ?INT1)
(instance ?PUB1 Publication)
(instance ?PUB2 Publication)
(patient ?PUB1 ?EDITION1)
(patient ?PUB2 ?EDITION2)
(date ?PUB1 ?DATE1)
(date ?PUB2 ?DATE2))
(before
(EndFn ?DATE1)
(EndFn ?DATE2)))
If text is a subclass of periodical and "volume int1 in the series text" is equal to volume1 and "volume int2 in the series text" is equal to volume2 and int2 is greater than int1 and pub1 is an instance of publication and pub2 is an instance of publication and volume1 is a patient of pub1 and volume2 is a patient of pub2 and date of pub1 is date1 and date of pub2 is date2, then "the end of date1" happen?{s} before "the end of date2".
(=>
(and
(subclass ?TEXT Periodical)
(equal
(SeriesVolumeFn ?TEXT ?INT1)
?VOLUME1)
(equal
(SeriesVolumeFn ?TEXT ?INT2)
?VOLUME2)
(greaterThan ?INT2 ?INT1)
(instance ?PUB1 Publication)
(instance ?PUB2 Publication)
(patient ?PUB1 ?VOLUME1)
(patient ?PUB2 ?VOLUME2)
(date ?PUB1 ?DATE1)
(date ?PUB2 ?DATE2))
(before
(EndFn ?DATE1)
(EndFn ?DATE2)))
If text is an instance of summary, then there exists text text2 so that text2 subsumes the content of text.
(=>
(instance ?TEXT Summary)
(exists
(?TEXT2)
(and
(instance ?TEXT2 Text)
(subsumesContentInstance ?TEXT2 ?TEXT))))
If series is an instance of series, then there exist book book1,book book2 so that series subsumes the content of book1 and series subsumes the content of book2 and book1 is not equal to book2.
(=>
(instance ?SERIES Series)
(exists
(?BOOK1 ?BOOK2)
(and
(instance ?BOOK1 Book)
(instance ?BOOK2 Book)
(subsumesContentInstance ?SERIES ?BOOK1)
(subsumesContentInstance ?SERIES ?BOOK2)
(not
(equal ?BOOK1 ?BOOK2)))))
If article is an instance of article, then there exists book book so that book subsumes the content of article.
(=>
(instance ?ARTICLE Article)
(exists
(?BOOK)
(and
(instance ?BOOK Book)
(subsumesContentInstance ?BOOK ?ARTICLE))))
If doc is an instance of certificate and agent posesses doc, then there exists proc so that doc allows agent to perform task of the type proc or doc obligates agent to perform task of the type proc.
(=>
(and
(instance ?DOC Certificate)
(possesses ?AGENT ?DOC))
(exists
(?PROC)
(or
(confersRight ?PROC ?DOC ?AGENT)
(confersObligation ?PROC ?DOC ?AGENT))))
If mole is an instance of molecule, then there exist atom atom1,atom atom2 so that atom1 is a part of mole and atom2 is a part of mole and atom1 is not equal to atom2.
(=>
(instance ?MOLE Molecule)
(exists
(?ATOM1 ?ATOM2)
(and
(instance ?ATOM1 Atom)
(instance ?ATOM2 Atom)
(part ?ATOM1 ?MOLE)
(part ?ATOM2 ?MOLE)
(not
(equal ?ATOM1 ?ATOM2)))))
artifact is an instance of artifact if and only if there exists making making so that artifact is a result of making.
(<=>
(instance ?ARTIFACT Artifact)
(exists
(?MAKING)
(and
(instance ?MAKING Making)
(result ?MAKING ?ARTIFACT))))
If product is an instance of product, then there exists manufacture manufacture so that product is a result of manufacture.
(=>
(instance ?PRODUCT Product)
(exists
(?MANUFACTURE)
(and
(instance ?MANUFACTURE Manufacture)
(result ?MANUFACTURE ?PRODUCT))))
(=>
(instance ?ARTIFACT StationaryArtifact)
(exists
(?PLACE)
(forall
(?TIME)
(=>
(and
(beforeOrEqual
?TIME
(EndFn
(WhenFn ?ARTIFACT)))
(beforeOrEqual
(BeginFn
(WhenFn ?ARTIFACT))
?TIME))
(equal
(WhereFn ?ARTIFACT ?TIME)
?PLACE)))))
If building is an instance of building, then there exists human human so that - human lives in building
or - there exists act so that act is an agent of human and act is located at building
.
(=>
(instance ?BUILDING Building)
(exists
(?HUMAN)
(and
(instance ?HUMAN Human)
(or
(inhabits ?HUMAN ?BUILDING)
(exists
(?ACT)
(and
(agent ?ACT ?HUMAN)
(located ?ACT ?BUILDING)))))))
If room is an instance of room, then there exists building build so that room is a properPart of build.
(=>
(instance ?ROOM Room)
(exists
(?BUILD)
(and
(instance ?BUILD Building)
(properPart ?ROOM ?BUILD))))
If clothing is an instance of clothing, then there exists fabric fabric so that fabric is a part of clothing.
(=>
(instance ?CLOTHING Clothing)
(exists
(?FABRIC)
(and
(instance ?FABRIC Fabric)
(part ?FABRIC ?CLOTHING))))
If device is an instance of device, then there exists process proc so that device is capable to do proc in role instrument.
(=>
(instance ?DEVICE Device)
(exists
(?PROC)
(and
(subclass ?PROC Process)
(capability ?PROC instrument ?DEVICE))))
If device is an instance of device, then there exists process proc so that device has purpose "device is capable to do proc in role instrument".
(=>
(instance ?DEVICE Device)
(exists
(?PROC)
(and
(subclass ?PROC Process)
(hasPurpose
?DEVICE
(capability ?PROC instrument ?DEVICE)))))
If weapon is an instance of weapon, then weapon has purpose "there exist damaging dest,patient so that patient is a patient of dest and ".
(=>
(instance ?WEAPON Weapon)
(hasPurpose
?WEAPON
(exists
(?DEST ?PATIENT)
(and
(instance ?DEST Damaging)
(patient ?DEST ?PATIENT)
(or
(instance ?PATIENT StationaryArtifact)
(instance ?PATIENT Animal)
(exists
(?ANIMAL)
(and
(instance ?ANIMAL Animal)
(inhabits ?ANIMAL ?PATIENT))))))))
- if machine is an instance of machine,
- then for all proc holds: if machine is an instrument for proc, then there exist resource,result so that resource is a resource for proc and result is a result of proc
.
(=>
(instance ?MACHINE Machine)
(forall
(?PROC)
(=>
(instrument ?PROC ?MACHINE)
(exists
(?RESOURCE ?RESULT)
(and
(resource ?PROC ?RESOURCE)
(result ?PROC ?RESULT))))))
If comp is an instance of engineering component, then there exists device device so that comp is a component of device.
(=>
(instance ?COMP EngineeringComponent)
(exists
(?DEVICE)
(and
(instance ?DEVICE Device)
(component ?COMP ?DEVICE))))
If comp1 is connected to comp2, then comp1 is a component of comp2 and comp2 is a component of comp1.
(=>
(connectedEngineeringComponents ?COMP1 ?COMP2)
(and
(not
(engineeringSubcomponent ?COMP1 ?COMP2))
(not
(engineeringSubcomponent ?COMP2 ?COMP1))))
If group is an instance of group and memb is a member of group, then memb is an instance of agent.
(=>
(and
(instance ?GROUP Group)
(member ?MEMB ?GROUP))
(instance ?MEMB Agent))
- if group is an instance of age group,
- then for all memb1,memb2,age1,age2 holds: if memb1 is a member of group and memb2 is a member of group and the age of memb1 is age1 and the age of memb2 is age2, then age1 is equal to age2
.
(=>
(instance ?GROUP AgeGroup)
(forall
(?MEMB1 ?MEMB2 ?AGE1 ?AGE2)
(=>
(and
(member ?MEMB1 ?GROUP)
(member ?MEMB2 ?GROUP)
(age ?MEMB1 ?AGE1)
(age ?MEMB2 ?AGE2))
(equal ?AGE1 ?AGE2))))
(=>
(instance ?GROUP FamilyGroup)
(forall
(?MEMB1 ?MEMB2)
(=>
(and
(member ?MEMB1 ?GROUP)
(member ?MEMB2 ?GROUP))
(familyRelation ?MEMB1 ?MEMB2))))
If organism1 and organism2 are related, then there exists organism3 so that organism3 and organism1 are related and organism3 and organism2 are related.
(=>
(familyRelation ?ORGANISM1 ?ORGANISM2)
(exists
(?ORGANISM3)
(and
(familyRelation ?ORGANISM3 ?ORGANISM1)
(familyRelation ?ORGANISM3 ?ORGANISM2))))
If "the legal organizational entity of unit" is equal to org and attr is an instance of normative attribute, then attr is an attribute of unit if and only if attr is an attribute of org.
(=>
(and
(equal
(OrganizationFn ?UNIT)
?ORG)
(instance ?ATTR NormativeAttribute))
(<=>
(attribute ?UNIT ?ATTR)
(attribute ?ORG ?ATTR)))
If pol is an instance of political organization, then there exists political process proc so that proc is an agent of pol.
(=>
(instance ?POL PoliticalOrganization)
(exists
(?PROC)
(and
(instance ?PROC PoliticalProcess)
(agent ?PROC ?POL))))
If plan is an instance of plan and obj is an instance of content bearing object and obj contains information plan, then there exists planning planning so that obj is a result of planning.
(=>
(and
(instance ?PLAN Plan)
(instance ?OBJ ContentBearingObject)
(containsInformation ?OBJ ?PLAN))
(exists
(?PLANNING)
(and
(instance ?PLANNING Planning)
(result ?PLANNING ?OBJ))))
If obj1 is attr1 to obj2 and is opposed to ? and attr1 is a member of "()" and attr2 is a member of "()" and attr1 is not equal to attr2, then obj1 is not attr2 to obj2.
(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(contraryAttribute @ROW)
(inList
?ATTR1
(ListFn @ROW))
(inList
?ATTR2
(ListFn @ROW))
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))
If item has an attribute value and value is an instance of truth value, then item is an instance of sentence or item is an instance of proposition.
(=>
(and
(property ?ITEM ?VALUE)
(instance ?VALUE TruthValue))
(or
(instance ?ITEM Sentence)
(instance ?ITEM Proposition)))
If obj1 is attr1 to obj2 and attr1 is an instance of directional attribute and attr2 is an instance of directional attribute and attr1 is not equal to attr2, then obj1 is not attr2 to obj2.
(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(instance ?ATTR1 DirectionalAttribute)
(instance ?ATTR2 DirectionalAttribute)
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))
If direct is an instance of directional attribute and obj1 is direct to obj2 and obj2 is direct to obj3, then obj2 is between obj1 and obj33.
(=>
(and
(instance ?DIRECT DirectionalAttribute)
(orientation ?OBJ1 ?OBJ2 ?DIRECT)
(orientation ?OBJ2 ?OBJ3 ?DIRECT))
(between ?OBJ1 ?OBJ2 ?OBJ33))
If attribute is an attribute of person and attribute is an instance of social role, then person is an instance of human.
(=>
(and
(attribute ?PERSON ?ATTRIBUTE)
(instance ?ATTRIBUTE SocialRole))
(instance ?PERSON Human))
For all org holds: org doesn't employ person and person is an instance of human if and only if unemployed is an attribute of person.
(<=>
(forall
(?ORG)
(and
(not
(employs ?ORG ?PERSON))
(instance ?PERSON Human)))
(attribute ?PERSON Unemployed))
If the statement formula1 has the model force of prop and formula1 entails formula2, then the statement formula2 has the model force of prop.
(=>
(and
(modalAttribute ?FORMULA1 ?PROP)
(entails ?FORMULA1 ?FORMULA2))
(modalAttribute ?FORMULA2 ?PROP))
If agent is obliged to perform tasks of type process, then the statement "there exists process instance so that instance is an agent of agent" has the model force of obligation.
(=>
(holdsObligation ?PROCESS ?AGENT)
(modalAttribute
(exists
(?INSTANCE)
(and
(instance ?INSTANCE ?PROCESS)
(agent ?INSTANCE ?AGENT)))
Obligation))
If agent has the right to perform process, then the statement "there exists process instance so that instance is an agent of agent" has the model force of permission.
(=>
(holdsRight ?PROCESS ?AGENT)
(modalAttribute
(exists
(?INSTANCE)
(and
(instance ?INSTANCE ?PROCESS)
(agent ?INSTANCE ?AGENT)))
Permission))
If attr is an attribute of obj and attr is an instance of contest attribute, then there exists contest contest so that contest is an agent of obj or obj is a patient of contest.
(=>
(and
(attribute ?OBJ ?ATTR)
(instance ?ATTR ContestAttribute))
(exists
(?CONTEST)
(and
(instance ?CONTEST Contest)
(or
(agent ?CONTEST ?OBJ)
(patient ?CONTEST ?OBJ)))))
obj is an instance of substance if and only if there exists physical state attr so that attr is an attribute of obj.
(<=>
(instance ?OBJ Substance)
(exists
(?ATTR)
(and
(instance ?ATTR PhysicalState)
(attribute ?OBJ ?ATTR))))
If perception is an instance of perception and obj is a patient of perception, then there exists perceptual attribute prop so that prop is an attribute of obj.
(=>
(and
(instance ?PERCEPTION Perception)
(patient ?PERCEPTION ?OBJ))
(exists
(?PROP)
(and
(instance ?PROP PerceptualAttribute)
(attribute ?OBJ ?PROP))))
If obj is an instance of food, then there exists taste attribute attr so that attr is an attribute of obj.
(=>
(instance ?OBJ Food)
(exists
(?ATTR)
(and
(instance ?ATTR TasteAttribute)
(attribute ?OBJ ?ATTR))))
(=>
(and
(attribute ?OBJ Monochromatic)
(superficialPart ?PART ?OBJ)
(attribute ?PART ?COLOR)
(instance ?COLOR PrimaryColor))
(forall
(?ELEMENT)
(=>
(superficialPart ?ELEMENT ?OBJ)
(attribute ?ELEMENT ?COLOR))))
If polychromatic is an attribute of obj, then there exist part1,part2,color attribute color1,color attribute color2 so that part1 is a superficial part of obj and part2 is a superficial part of obj and color1 is an attribute of part1 and color2 is an attribute of part2 and color1 is not equal to color2.
(=>
(attribute ?OBJ Polychromatic)
(exists
(?PART1 ?PART2 ?COLOR1 ?COLOR2)
(and
(superficialPart ?PART1 ?OBJ)
(superficialPart ?PART2 ?OBJ)
(attribute ?PART1 ?COLOR1)
(attribute ?PART2 ?COLOR2)
(instance ?COLOR1 ColorAttribute)
(instance ?COLOR2 ColorAttribute)
(not
(equal ?COLOR1 ?COLOR2)))))
If there exists shape change change so that obj is a patient of change, then pliable is an attribute of obj.
(=>
(exists
(?CHANGE)
(and
(instance ?CHANGE ShapeChange)
(patient ?CHANGE ?OBJ)))
(attribute ?OBJ Pliable))
If attribute is an instance of texture attribute and attribute is an attribute of obj and surface is a surface of obj, then attribute is an attribute of surface.
(=>
(and
(instance ?ATTRIBUTE TextureAttribute)
(attribute ?OBJ ?ATTRIBUTE)
(surface ?SURFACE ?OBJ))
(attribute ?SURFACE ?ATTRIBUTE))
If dry is an attribute of obj, then there doesn't exist subobj so that subobj is a part of obj and liquid is an attribute of subobj.
(=>
(attribute ?OBJ Dry)
(not
(exists
(?SUBOBJ)
(and
(part ?SUBOBJ ?OBJ)
(attribute ?SUBOBJ Liquid)))))
- if wet is an attribute of obj,
- then for all part holds: if part is a part of obj, then there exists subpart so that subpart is a part of part and liquid is an attribute of subpart
.
(=>
(attribute ?OBJ Wet)
(forall
(?PART)
(=>
(part ?PART ?OBJ)
(exists
(?SUBPART)
(and
(part ?SUBPART ?PART)
(attribute ?SUBPART Liquid))))))
If unbreakable is an attribute of obj, then there doesn't exist damaging damage so that obj is a patient of damage.
(=>
(attribute ?OBJ Unbreakable)
(not
(exists
(?DAMAGE)
(and
(instance ?DAMAGE Damaging)
(patient ?DAMAGE ?OBJ)))))
If att is an attribute of org and att is an instance of biological attribute, then org is an instance of organism.
(=>
(and
(attribute ?ORG ?ATT)
(instance ?ATT BiologicalAttribute))
(instance ?ORG Organism))
If organism is an instance of organism and process is an agent of organism, then living is an attribute of organism the time of existence of process.
(=>
(and
(instance ?ORGANISM Organism)
(agent ?PROCESS ?ORGANISM))
(holdsDuring
(WhenFn ?PROCESS)
(attribute ?ORGANISM Living)))
If org is an instance of organism, then there exists animacy attribute attr so that attr is an attribute of org.
(=>
(instance ?ORG Organism)
(exists
(?ATTR)
(and
(instance ?ATTR AnimacyAttribute)
(attribute ?ORG ?ATTR))))
If body is an instance of reproductive body and body is a part of org and org is an instance of organism, then female is an attribute of org.
(=>
(and
(instance ?BODY ReproductiveBody)
(part ?BODY ?ORG)
(instance ?ORG Organism))
(attribute ?ORG Female))
If animal is an instance of animal, then there exists sex attribute attr so that attr is an attribute of animal.
(=>
(instance ?ANIMAL Animal)
(exists
(?ATTR)
(and
(instance ?ATTR SexAttribute)
(attribute ?ANIMAL ?ATTR))))
If fully formed is an attribute of obj, then there exists growth growth so that obj experiences growth and non fully formed is an attribute of obj the beginning of "the time of existence of obj".
(=>
(attribute ?OBJ FullyFormed)
(exists
(?GROWTH)
(and
(instance ?GROWTH Growth)
(experiencer ?GROWTH ?OBJ)
(holdsDuring
(BeginFn
(WhenFn ?OBJ))
(attribute ?OBJ NonFullyFormed)))))
If org is an instance of organism, then there exists developmental attribute attr so that attr is an attribute of org.
(=>
(instance ?ORG Organism)
(exists
(?ATTR)
(and
(instance ?ATTR DevelopmentalAttribute)
(attribute ?ORG ?ATTR))))
If larval is an attribute of org during time, then there exists birth birth so that org experiences birth before time.
(=>
(holdsDuring
?TIME
(attribute ?ORG Larval))
(holdsDuring
(PastFn ?TIME)
(exists
(?BIRTH)
(and
(instance ?BIRTH Birth)
(experiencer ?BIRTH ?ORG)))))
If embryonic is an attribute of org, then there exists reproductive body body so that org is located at body.
(=>
(attribute ?ORG Embryonic)
(exists
(?BODY)
(and
(instance ?BODY ReproductiveBody)
(located ?ORG ?BODY))))
If embryonic is an attribute of org during time, then there doesn't exist birth birth so that org experiences birth during time.
(=>
(holdsDuring
?TIME
(attribute ?ORG Embryonic))
(holdsDuring
?TIME
(not
(exists
(?BIRTH)
(and
(instance ?BIRTH Birth)
(experiencer ?BIRTH ?ORG))))))
If attr is an instance of psychological attribute and attr is an attribute of agent, then agent is an instance of sentient agent.
(=>
(and
(instance ?ATTR PsychologicalAttribute)
(attribute ?AGENT ?ATTR))
(instance ?AGENT SentientAgent))
agent is an instance of sentient agent and living is an attribute of agent if and only if there exists consciousness attribute attr so that attr is an attribute of agent.
(<=>
(and
(instance ?AGENT SentientAgent)
(attribute ?AGENT Living))
(exists
(?ATTR)
(and
(instance ?ATTR ConsciousnessAttribute)
(attribute ?AGENT ?ATTR))))
entity is an instance of "the union of class1 and class2" if and only if entity is an instance of class1 and entity is an instance of class2.
(<=>
(instance
?ENTITY
(IntersectionFn ?CLASS1 ?CLASS2))
(and
(instance ?ENTITY ?CLASS1)
(instance ?ENTITY ?CLASS2)))
If class1 is an instance of set or class and class2 is an instance of set or class, then "the difference between class1 and class2" is equal to "the union of class1 and "the complement of class2"".
(=>
(and
(instance ?CLASS1 SetOrClass)
(instance ?CLASS2 SetOrClass))
(equal
(RelativeComplementFn ?CLASS1 ?CLASS2)
(IntersectionFn
?CLASS1
(ComplementFn ?CLASS2))))
entity is an instance of "the union of all the elements of superclass" if and only if there exists superclass class so that entity is an instance of class.
(<=>
(instance
?ENTITY
(GeneralizedUnionFn ?SUPERCLASS))
(exists
(?CLASS)
(and
(instance ?CLASS ?SUPERCLASS)
(instance ?ENTITY ?CLASS))))
