equal (equal)
(equal entity1 entity2) is true just in case
entity1 is identical with entity2.
Ontology
SUMO / STRUCTURAL-ONTOLOGYClass(es)
Coordinate term(s)
addition fn
division fn
exponentiation fn
max fn
min fn
multiplication fn
reciprocal fn
remainder fn
round fn
subtraction fn
arc weight
authors
before or equal
causes
causes subclass
citizen
closed on
connected
contains information
cooccur
copy
date
decreases likelihood
developmental form
disjoint
distributes
documentation
duration
earlier
editor
element
employs
equivalence relation on
equivalent content class
equivalent content instance
exploits
expressed in language
faces
family relation
finishes
frequency
graph part
greater than
greater than or equal to
has purpose
has skill
holds during
holds obligation
holds right
hole
identity element
in list
in scope of interest
increases likelihood
independent probability
inhabits
inhibits
initial list
instance
inverse
irreflexive on
larger
less than
less than or equal to
material
measure
meets temporally
modal attribute
overlaps temporally
parent
partial ordering on
partly located
path length
possesses
precondition
prevents
property
publishes
range
range subclass
refers
reflexive on
related internal concept
sibling
smaller
starts
sub attribute
sub collection
sub graph
sub list
sub process
sub proposition
subclass
subrelation
subsumes content class
subsumes content instance
successor attribute
successor attribute closure
temporal part
time
total ordering on
trichotomizing on
uses
valence
version
Type restrictions
equal(entity, entity)
Related WordNet synsets
- sameness
- the quality of being alike: "sameness of purpose kept them together"
- identity, identicalness, indistinguishability
- exact sameness; "they shared an identity of interests"
- equality
- the quality or state of being the same in quantity or measure or value or status
- equivalence
- essential equality and interchangeability
- equatability
- capability of being equated
- changelessness
- the property of remaining unchanged
- equivalent
- a person or thing equal to another in value or measure or force or effect or significance etc: "send two dollars or the equivalent in stamps"
- equate, correspond
- be equivalent or parallel, in mathematics
- equal, be
- be identical or equivalent to: "One dollar equals 1,000 rubles these days!"
- equal
- well matched; having the same quantity, value, or measure as another; "on equal terms"; "all men are equal before the law"
- like, equal, equivalent, same
- equal in amount or value; "like amounts"; "equivalent amounts"; "the same amount"; "gave one six blows and the other a like number"; "an equal number"; "the same number"
- same
- same in identity; "the same man I saw yesterday"; "never wore the same dress twice"; "this road is the same one we were on yesterday"; "on the same side of the street"
See more related synsets on a separate page.
Axioms (245)
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 thing1 is equal to thing2, then for all attr holds: thing1 has an attribute attr if and only if thing2 has an attribute attr.
(=>
(equal ?THING1 ?THING2)
(forall
(?ATTR)
(<=>
(property ?THING1 ?ATTR)
(property ?THING2 ?ATTR))))
If attr1 is equal to attr2, then for all thing holds: thing has an attribute attr1 if and only if thing has an attribute attr2.
(=>
(equal ?ATTR1 ?ATTR2)
(forall
(?THING)
(<=>
(property ?THING ?ATTR1)
(property ?THING ?ATTR2))))
If thing1 is equal to thing2, then for all class holds: thing1 is an instance of class if and only if thing2 is an instance of class.
(=>
(equal ?THING1 ?THING2)
(forall
(?CLASS)
(<=>
(instance ?THING1 ?CLASS)
(instance ?THING2 ?CLASS))))
If class1 is equal to class2, then for all thing holds: thing is an instance of class1 if and only if thing is an instance of class2.
(=>
(equal ?CLASS1 ?CLASS2)
(forall
(?THING)
(<=>
(instance ?THING ?CLASS1)
(instance ?THING ?CLASS2))))
If rel1 is equal to rel2, then for all holds: rel1() holds if and only if rel2() holds.
(=>
(equal ?REL1 ?REL2)
(forall
(@ROW)
(<=>
(holds ?REL1 @ROW)
(holds ?REL2 @ROW))))
(=>
(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 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 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))))))
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))
(=>
(instance ?ATOM Atom)
(forall
(?NUCLEUS1 ?NUCLEUS2)
(=>
(and
(component ?NUCLEUS1 ?ATOM)
(component ?NUCLEUS2 ?ATOM)
(instance ?NUCLEUS1 AtomicNucleus)
(instance ?NUCLEUS2 AtomicNucleus))
(equal ?NUCLEUS1 ?NUCLEUS2))))
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)))))
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)))))
"the description of class" is equal to attr if and only if for all inst holds: inst is an instance of class if and only if inst has an attribute attr.
(<=>
(equal
(AbstractionFn ?CLASS)
?ATTR)
(forall
(?INST)
(<=>
(instance ?INST ?CLASS)
(property ?INST ?ATTR))))
"the class corresponding to attribute" is equal to class if and only if "the description of class" is equal to attribute.
(<=>
(equal
(ExtensionFn ?ATTRIBUTE)
?CLASS)
(equal
(AbstractionFn ?CLASS)
?ATTRIBUTE))
number1 is less than or equal to number2 if and only if number1 is equal to number2 or number1 is less than number2.
(<=>
(lessThanOrEqualTo ?NUMBER1 ?NUMBER2)
(or
(equal ?NUMBER1 ?NUMBER2)
(lessThan ?NUMBER1 ?NUMBER2)))
number1 is greater than or equal to number2 if and only if number1 is equal to number2 or number1 is greater than number2.
(<=>
(greaterThanOrEqualTo ?NUMBER1 ?NUMBER2)
(or
(equal ?NUMBER1 ?NUMBER2)
(greaterThan ?NUMBER1 ?NUMBER2)))
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))))))
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)))))))
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))))))
(=>
(instance ?REL AntisymmetricRelation)
(forall
(?INST1 ?INST2)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST1))
(equal ?INST1 ?INST2))))
If rel is an instance of trichotomizing relation, then for all inst1,inst2 holds: rel(inst1,inst2) holds or inst1 is equal to inst2 or rel(inst2,inst1) holds.
(=>
(instance ?REL TrichotomizingRelation)
(forall
(?INST1 ?INST2)
(or
(holds ?REL ?INST1 ?INST2)
(equal ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST1))))
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 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))))))))
list is an instance of unique list if and only if for all number1,number2 holds: if "number1th element of list" is equal to "number2th element of list", then number1 is equal to number2.
(<=>
(instance ?LIST UniqueList)
(forall
(?NUMBER1 ?NUMBER2)
(=>
(equal
(ListOrderFn ?LIST ?NUMBER1)
(ListOrderFn ?LIST ?NUMBER2))
(equal ?NUMBER1 ?NUMBER2))))
list is equal to null list if and only if there doesn't exist item so that item is a member of list.
(<=>
(equal ?LIST NullList)
(not
(exists
(?ITEM)
(inList ?ITEM ?LIST))))
- 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 "length of list" is equal to number1, then for all number2 holds: there exists item so that "number2th element of list" is equal to item if and only if number2 is less than or equal to number1.
(=>
(equal
(ListLengthFn ?LIST)
?NUMBER1)
(forall
(?NUMBER2)
(<=>
(exists
(?ITEM)
(equal
(ListOrderFn ?LIST ?NUMBER2)
?ITEM))
(lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))
"length of "(,item)"" is equal to "("length of "()""+1)".
(equal
(ListLengthFn
(ListFn @ROW ?ITEM))
(SuccessorFn
(ListLengthFn
(ListFn @ROW))))
""length of "(,item)""th element of "(,item)"" is equal to item.
(equal
(ListOrderFn
(ListFn @ROW ?ITEM)
(ListLengthFn
(ListFn @ROW ?ITEM)))
?ITEM)
(=>
(valence ?REL ?NUMBER)
(forall
(@ROW)
(=>
(holds ?REL @ROW)
(equal
(ListLengthFn
(ListFn @ROW))
?NUMBER))))
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))))))
item is a member of list if and only if there exists number so that "numberth element of list" is equal to item.
(<=>
(inList ?ITEM ?LIST)
(exists
(?NUMBER)
(equal
(ListOrderFn ?LIST ?NUMBER)
?ITEM)))
- 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 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)))))
- 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 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 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))))))
"the place where thing was at time" is equal to region if and only if thing is exactly located in region during time.
(<=>
(equal
(WhereFn ?THING ?TIME)
?REGION)
(holdsDuring
?TIME
(exactlyLocated ?THING ?REGION)))
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))
"(number+1)" is equal to "(number+)".
(equal
(SuccessorFn ?NUMBER)
(AdditionFn ?NUMBER 1))
"(number+2)" is equal to "(number-)".
(equal
(PredecessorFn ?NUMBER)
(SubtractionFn ?NUMBER 1))
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 for all element holds: if element is a member of "()", then "element mod number" is equal to
.
(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?NUMBER)
0))))
- 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 for all element holds: if element is a member of "()", then "number mod element" is equal to
.
(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?NUMBER ?ELEMENT)
0))))
- 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 number is an instance of quantity, then "the reciprocal of number" is equal to "number raised to the power ".
(=>
(instance ?NUMBER Quantity)
(equal
(ReciprocalFn ?NUMBER)
(ExponentiationFn ?NUMBER -1)))
If number is an instance of quantity, then is equal to "number*"the reciprocal of number"".
(=>
(instance ?NUMBER Quantity)
(equal
1
(MultiplicationFn
?NUMBER
(ReciprocalFn ?NUMBER))))
"number1 mod number2" is equal to number if and only if "(""the largest integer less than or equal to "number1/number2""*number2"+number)" is equal to number1.
(<=>
(equal
(RemainderFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(equal
(AdditionFn
(MultiplicationFn
(FloorFn
(DivisionFn ?NUMBER1 ?NUMBER2))
?NUMBER2)
?NUMBER)
?NUMBER1))
If "number1 mod number2" is equal to number, then "the sign of number2" is equal to "the sign of number".
(=>
(equal
(RemainderFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(equal
(SignumFn ?NUMBER2)
(SignumFn ?NUMBER)))
If number is an instance of even integer, then "number mod " is equal to .
(=>
(instance ?NUMBER EvenInteger)
(equal
(RemainderFn ?NUMBER 2)
0))
If number is an instance of odd integer, then "number mod " is equal to .
(=>
(instance ?NUMBER OddInteger)
(equal
(RemainderFn ?NUMBER 2)
1))
(=>
(instance ?PRIME PrimeNumber)
(forall
(?NUMBER)
(=>
(equal
(RemainderFn ?PRIME ?NUMBER)
0)
(or
(equal ?NUMBER 1)
(equal ?NUMBER ?PRIME)))))
- if "number1 rounded" is equal to number2,
- then
- if "(number1-"the largest integer less than or equal to number1")" is less than , then number2 is equal to "the largest integer less than or equal to number1"
or - if "(number1-"the largest integer less than or equal to number1")" is greater than or equal to , then number2 is equal to "the ceiling of number1"
.
(=>
(equal
(RoundFn ?NUMBER1)
?NUMBER2)
(or
(=>
(lessThan
(SubtractionFn
?NUMBER1
(FloorFn ?NUMBER1))
0.5)
(equal
?NUMBER2
(FloorFn ?NUMBER1)))
(=>
(greaterThanOrEqualTo
(SubtractionFn
?NUMBER1
(FloorFn ?NUMBER1))
0.5)
(equal
?NUMBER2
(CeilingFn ?NUMBER1)))))
If number is an instance of nonnegative real number, then "the sign of number" is equal to or "the sign of number" is equal to .
(=>
(instance ?NUMBER NonnegativeRealNumber)
(or
(equal
(SignumFn ?NUMBER)
1)
(equal
(SignumFn ?NUMBER)
0)))
If number is an instance of positive real number, then "the sign of number" is equal to .
(=>
(instance ?NUMBER PositiveRealNumber)
(equal
(SignumFn ?NUMBER)
1))
If number is an instance of negative real number, then "the sign of number" is equal to .
(=>
(instance ?NUMBER NegativeRealNumber)
(equal
(SignumFn ?NUMBER)
-1))
If "the square root of number1" is equal to number2, then "number2*number2" is equal to number1.
(=>
(equal
(SquareRootFn ?NUMBER1)
?NUMBER2)
(equal
(MultiplicationFn ?NUMBER2 ?NUMBER2)
?NUMBER1))
If degree is an instance of plane angle measure, then "the tangent of degree" is equal to ""the sine of degree"/"the cosine of degree"".
(=>
(instance ?DEGREE PlaneAngleMeasure)
(equal
(TangentFn ?DEGREE)
(DivisionFn
(SineFn ?DEGREE)
(CosineFn ?DEGREE))))
- 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+1)" is equal to "(int2+1)", then int1 is equal to int2.
(=>
(equal
(SuccessorFn ?INT1)
(SuccessorFn ?INT2))
(equal ?INT1 ?INT2))
If int is an instance of integer, then int is equal to "("(int+2)"+1)".
(=>
(instance ?INT Integer)
(equal
?INT
(SuccessorFn
(PredecessorFn ?INT))))
If int is an instance of integer, then int is equal to "("(int+1)"+2)".
(=>
(instance ?INT Integer)
(equal
?INT
(PredecessorFn
(SuccessorFn ?INT))))
If "(int1+2)" is equal to "(int2+2)", then int1 is equal to int2.
(=>
(equal
(PredecessorFn ?INT1)
(PredecessorFn ?INT2))
(equal ?INT1 ?INT2))
If for all element holds: element is an element of set1 if and only if element is an element of set2, then set1 is equal to set2.
(=>
(forall
(?ELEMENT)
(<=>
(element ?ELEMENT ?SET1)
(element ?ELEMENT ?SET2)))
(equal ?SET1 ?SET2))
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)))))
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))))
(=>
(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)))))
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
- "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, then path is an instance of "the set of paths between node1 and node2".
(=>
(equal
(MinimalWeightedPathFn ?NODE1 ?NODE2)
?PATH)
(instance
?PATH
(GraphPathFn ?NODE1 ?NODE2)))
- 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, then path is an instance of "the set of paths between node1 and node2".
(=>
(equal
(MaximalWeightedPathFn ?NODE1 ?NODE2)
?PATH)
(instance
?PATH
(GraphPathFn ?NODE1 ?NODE2)))
- 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)))
- if "the set of minimal paths that partition graph into two separate graphs" is equal to pathclass,
- then there exists number so that for all path holds: if path is an instance of pathclass, then the length of path is number
.
(=>
(equal
(MinimalCutSetFn ?GRAPH)
?PATHCLASS)
(exists
(?NUMBER)
(forall
(?PATH)
(=>
(instance ?PATH ?PATHCLASS)
(pathLength ?PATH ?NUMBER)))))
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))
If unit is an instance of unit of measure, then "1 thousand units" is equal to " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(KiloFn ?UNIT)
(MeasureFn 1000 ?UNIT)))
If unit is an instance of unit of measure, then "1 million units" is equal to " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MegaFn ?UNIT)
(MeasureFn 1000000 ?UNIT)))
If unit is an instance of unit of measure, then "1 billion units " is equal to " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(GigaFn ?UNIT)
(MeasureFn 1000000000 ?UNIT)))
If unit is an instance of unit of measure, then "1 trillion units" is equal to " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(TeraFn ?UNIT)
(MeasureFn 1000000000000 ?UNIT)))
If unit is an instance of unit of measure, then "one thousandth of a unit" is equal to " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MilliFn ?UNIT)
(MeasureFn 0.001 ?UNIT)))
If unit is an instance of unit of measure, then "one millionth of a unit" is equal to " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MicroFn ?UNIT)
(MeasureFn 0.000001 ?UNIT)))
If unit is an instance of unit of measure, then "one billionth of a unit" is equal to " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(NanoFn ?UNIT)
(MeasureFn 0.000000001 ?UNIT)))
If unit is an instance of unit of measure, then "one trillionth of a unit" is equal to " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(PicoFn ?UNIT)
(MeasureFn 0.000000000001 ?UNIT)))
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 number is an instance of real number, then "number centimeter(s)" is equal to ""number*" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Centimeter)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
Meter)))
If number is an instance of real number, then "number celsius degree(s)" is equal to ""(number-)" kelvin degree(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER CelsiusDegree)
(MeasureFn
(SubtractionFn ?NUMBER 273.15)
KelvinDegree)))
If number is an instance of real number, then "number celsius degree(s)" is equal to """(number-)"/" fahrenheit degree(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER CelsiusDegree)
(MeasureFn
(DivisionFn
(SubtractionFn ?NUMBER 32)
1.8)
FahrenheitDegree)))
If number is an instance of real number, then "number day duration(s)" is equal to ""number*" hour duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER DayDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 24)
HourDuration)))
If number is an instance of real number, then "number hour duration(s)" is equal to ""number*" minute duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER HourDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 60)
MinuteDuration)))
If number is an instance of real number, then "number minute duration(s)" is equal to ""number*" second duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER MinuteDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 60)
SecondDuration)))
If number is an instance of real number, then "number week duration(s)" is equal to ""number*" day duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER WeekDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 7)
DayDuration)))
If number is an instance of real number, then "number year duration(s)" is equal to ""number*" day duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER YearDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 365)
DayDuration)))
If number is an instance of real number, then "number amu(s)" is equal to ""number**" gram(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Amu)
(MeasureFn
(MultiplicationFn ?NUMBER 1.6605402 E-24)
Gram)))
If number is an instance of real number, then "number electron volt(s)" is equal to ""number**" joule(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER ElectronVolt)
(MeasureFn
(MultiplicationFn ?NUMBER 1.60217733 E-19)
Joule)))
If number is an instance of real number, then "number angstrom(s)" is equal to ""number**" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Angstrom)
(MeasureFn
(MultiplicationFn ?NUMBER 1.0 E-10)
Meter)))
If number is an instance of real number, then "number foot(s)" is equal to ""number*" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Foot)
(MeasureFn
(MultiplicationFn ?NUMBER 0.3048)
Meter)))
If number is an instance of real number, then "number inch(s)" is equal to ""number*" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Inch)
(MeasureFn
(MultiplicationFn ?NUMBER 0.0254)
Meter)))
If number is an instance of real number, then "number mile(s)" is equal to ""number*" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Mile)
(MeasureFn
(MultiplicationFn ?NUMBER 1609.344)
Meter)))
If number is an instance of real number, then "number united states gallon(s)" is equal to ""number*" liter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedStatesGallon)
(MeasureFn
(MultiplicationFn ?NUMBER 3.785411784)
Liter)))
If number is an instance of real number, then "number quart(s)" is equal to ""number/" united states gallon(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Quart)
(MeasureFn
(DivisionFn ?NUMBER 4)
UnitedStatesGallon)))
If number is an instance of real number, then "number pint(s)" is equal to ""number/" quart(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Pint)
(MeasureFn
(DivisionFn ?NUMBER 2)
Quart)))
If number is an instance of real number, then "number cup(s)" is equal to ""number/" pint(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Cup)
(MeasureFn
(DivisionFn ?NUMBER 2)
Pint)))
If number is an instance of real number, then "number ounce(s)" is equal to ""number/" cup(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Ounce)
(MeasureFn
(DivisionFn ?NUMBER 8)
Cup)))
If number is an instance of real number, then "number united kingdom gallon(s)" is equal to ""number*" liter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedKingdomGallon)
(MeasureFn
(MultiplicationFn ?NUMBER 4.54609)
Liter)))
If number is an instance of real number, then "number pound mass(s)" is equal to ""number*" gram(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER PoundMass)
(MeasureFn
(MultiplicationFn ?NUMBER 453.59237)
Gram)))
If number is an instance of real number, then "number slug(s)" is equal to ""number*" gram(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Slug)
(MeasureFn
(MultiplicationFn ?NUMBER 14593.90)
Gram)))
If number is an instance of real number, then "number rankine degree(s)" is equal to ""number*" kelvin degree(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER RankineDegree)
(MeasureFn
(MultiplicationFn ?NUMBER 1.8)
KelvinDegree)))
If number is an instance of real number, then "number pound force(s)" is equal to ""number*" newton(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER PoundForce)
(MeasureFn
(MultiplicationFn ?NUMBER 4.448222)
Newton)))
If number is an instance of real number, then "number calorie(s)" is equal to ""number*" joule(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Calorie)
(MeasureFn
(MultiplicationFn ?NUMBER 4.1868)
Joule)))
If number is an instance of real number, then "number british thermal unit(s)" is equal to ""number*" joule(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER BritishThermalUnit)
(MeasureFn
(MultiplicationFn ?NUMBER 1055.05585262)
Joule)))
If number is an instance of real number, then "number angular degree(s)" is equal to ""number*"pi/"" radian(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER AngularDegree)
(MeasureFn
(MultiplicationFn
?NUMBER
(DivisionFn Pi 180))
Radian)))
If number is an instance of real number, then "number united states cent(s)" is equal to ""number*" united states dollar(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedStatesCent)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
UnitedStatesDollar)))
If number is an instance of real number, then "number euro cent(s)" is equal to ""number*" euro dollar(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER EuroCent)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
EuroDollar)))
If number is an instance of real number, then "number byte(s)" is equal to ""number*" bit(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Byte)
(MeasureFn
(MultiplicationFn ?NUMBER 8)
Bit)))
If number is an instance of real number, then "number kilo byte(s)" is equal to ""number*" byte(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER KiloByte)
(MeasureFn
(MultiplicationFn ?NUMBER 1024)
Byte)))
If number is an instance of real number, then "number mega byte(s)" is equal to ""number*" kilo byte(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER MegaByte)
(MeasureFn
(MultiplicationFn ?NUMBER 1024)
KiloByte)))
"value of belongings of person" is equal to amount if and only if value of "belongings of person" is amount.
(<=>
(equal
(WealthFn ?PERSON)
?AMOUNT)
(monetaryValue
(PropertyFn ?PERSON)
?AMOUNT))
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 "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))))
If point1 happen?{s} before or at point2, then point1 happen?{s} before point2 or point1 is equal to point2.
(=>
(beforeOrEqual ?POINT1 ?POINT2)
(or
(before ?POINT1 ?POINT2)
(equal ?POINT1 ?POINT2)))
interval1 meets interval2 if and only if "the end of interval1" is equal to "the beginning of interval2".
(<=>
(meetsTemporally ?INTERVAL1 ?INTERVAL2)
(equal
(EndFn ?INTERVAL1)
(BeginFn ?INTERVAL2)))
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))
phys1 occurs at the same time as phys2 if and only if "the time of existence of phys1" is equal to "the time of existence of phys2".
(<=>
(cooccur ?PHYS1 ?PHYS2)
(equal
(WhenFn ?PHYS1)
(WhenFn ?PHYS2)))
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 between point1 and point2" is equal to interval, then for all point holds: point is between or at point1 and point2 if and only if point is a part of interval.
(=>
(equal
(TimeIntervalFn ?POINT1 ?POINT2)
?INTERVAL)
(forall
(?POINT)
(<=>
(temporallyBetweenOrEqual ?POINT1 ?POINT ?POINT2)
(temporalPart ?POINT ?INTERVAL))))
If process is an instance of physical, then "before "the time of existence of process"" is equal to "interval between negative infinity and "the beginning of "the time of existence of process""".
(=>
(instance ?PROCESS Physical)
(equal
(PastFn
(WhenFn ?PROCESS))
(TimeIntervalFn
NegativeInfinity
(BeginFn
(WhenFn ?PROCESS)))))
If process is an instance of physical, then "after "the time of existence of process"" is equal to "interval between "the end of "the time of existence of process"" and positive infinity".
(=>
(instance ?PROCESS Physical)
(equal
(FutureFn
(WhenFn ?PROCESS))
(TimeIntervalFn
(EndFn
(WhenFn ?PROCESS))
PositiveInfinity)))
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 "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 year is an instance of year, then "the number of instances in "decomposition of year into ? months"" is equal to .
(=>
(instance ?YEAR Year)
(equal
(CardinalityFn
(TemporalCompositionFn ?YEAR Month))
12))
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))
If week is an instance of week, then "the number of instances in "decomposition of week into ? days"" is equal to .
(=>
(instance ?WEEK Week)
(equal
(CardinalityFn
(TemporalCompositionFn ?WEEK Day))
7))
If day is an instance of day, then "the number of instances in "decomposition of day into ? hours"" is equal to .
(=>
(instance ?DAY Day)
(equal
(CardinalityFn
(TemporalCompositionFn ?DAY Hour))
24))
If hour is an instance of hour, then "the number of instances in "decomposition of hour into ? minutes"" is equal to .
(=>
(instance ?HOUR Hour)
(equal
(CardinalityFn
(TemporalCompositionFn ?HOUR Minute))
60))
If minute is an instance of minute, then "the number of instances in "decomposition of minute into ? seconds"" is equal to .
(=>
(instance ?MINUTE Minute)
(equal
(CardinalityFn
(TemporalCompositionFn ?MINUTE Second))
60))
obj is an instance of self connected object if and only if for all part1,part2 holds: if obj is equal to "the union of the parts of part1 and part2", then part1 is connected to part2.
(<=>
(instance ?OBJ SelfConnectedObject)
(forall
(?PART1 ?PART2)
(=>
(equal
?OBJ
(MereologicalSumFn ?PART1 ?PART2))
(connected ?PART1 ?PART2))))
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 obj3 is equal to "the union 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 or part is a part of obj2.
(=>
(equal
?OBJ3
(MereologicalSumFn ?OBJ1 ?OBJ2))
(forall
(?PART)
(<=>
(part ?PART ?OBJ3)
(or
(part ?PART ?OBJ1)
(part ?PART ?OBJ2)))))
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 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 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 subproc is a subprocess of proc, then "the time of existence of subproc" is equal to "the time of existence of proc" or "the time of existence of subproc" takes place during "the time of existence of proc".
(=>
(subProcess ?SUBPROC ?PROC)
(or
(equal
(WhenFn ?SUBPROC)
(WhenFn ?PROC))
(during
(WhenFn ?SUBPROC)
(WhenFn ?PROC))))
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 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 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 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 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 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 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))))
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 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 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 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 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 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))))
"the number of instances in continent" is equal to .
(equal
(CardinalityFn Continent)
7)
(=>
(instance ?BACTERIUM Bacterium)
(exists
(?CELL1)
(and
(component ?CELL1 ?BACTERIUM)
(instance ?CELL1 Cell)
(forall
(?CELL2)
(=>
(and
(component ?CELL2 ?BACTERIUM)
(instance ?CELL2 Cell))
(equal ?CELL1 ?CELL2))))))
(=>
(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 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 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 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 "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 "edition number of text1" is equal to text2, then text1 subsumes the content of text2.
(=>
(equal
(EditionFn ?TEXT1 ?NUMBER)
?TEXT2)
(subsumesContentClass ?TEXT1 ?TEXT2))
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 "volume number in the series series" is equal to volume, then series subsumes the content of volume.
(=>
(equal
(SeriesVolumeFn ?SERIES ?NUMBER)
?VOLUME)
(subsumesContentClass ?SERIES ?VOLUME))
If "the periodical number number of periodical" is equal to issue, then periodical subsumes the content of issue.
(=>
(equal
(PeriodicalIssueFn ?PERIODICAL ?NUMBER)
?ISSUE)
(subsumesContentClass ?PERIODICAL ?ISSUE))
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 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)))))
(=>
(instance ?ARTIFACT StationaryArtifact)
(exists
(?PLACE)
(forall
(?TIME)
(=>
(and
(beforeOrEqual
?TIME
(EndFn
(WhenFn ?ARTIFACT)))
(beforeOrEqual
(BeginFn
(WhenFn ?ARTIFACT))
?TIME))
(equal
(WhereFn ?ARTIFACT ?TIME)
?PLACE)))))
- 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))))
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 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 entities in the process proc are moving attr1 during time,
- then for all attr2 holds: if entities in the process proc are moving attr2 during time, then attr2 is equal to attr1
.
(=>
(holdsDuring
?TIME
(direction ?PROC ?ATTR1))
(forall
(?ATTR2)
(=>
(holdsDuring
?TIME
(direction ?PROC ?ATTR2))
(equal ?ATTR2 ?ATTR1))))
- if proc faces attr1 during time,
- then for all attr2 holds: if proc faces attr2 during time, then attr2 is equal to attr1
.
(=>
(holdsDuring
?TIME
(faces ?PROC ?ATTR1))
(forall
(?ATTR2)
(=>
(holdsDuring
?TIME
(faces ?PROC ?ATTR2))
(equal ?ATTR2 ?ATTR1))))
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 "relative time fn(time1,pacific time zone)" is equal to time2, then time2 is equal to "(time1+)".
(=>
(equal
(RelativeTimeFn ?TIME1 PacificTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 8)))
If "relative time fn(time1,mountain time zone)" is equal to time2, then time2 is equal to "(time1+)".
(=>
(equal
(RelativeTimeFn ?TIME1 MountainTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 7)))
If "relative time fn(time1,central time zone)" is equal to time2, then time2 is equal to "(time1+)".
(=>
(equal
(RelativeTimeFn ?TIME1 CentralTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 6)))
If "relative time fn(time1,eastern time zone)" is equal to time2, then time2 is equal to "(time1+)".
(=>
(equal
(RelativeTimeFn ?TIME1 EasternTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 5)))
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 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))))
