equal (equal)
(equal entity1 entity2) is true just in case
entity1 is identical with entity2.
Ontologie
SUMO / STRUCTURAL-ONTOLOGYClass(es)
Související termín(y)
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
Typy argumentů
equal(entita, entita)
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.
Axiomy (245)
Jestliže immediate subclass(class1,class2) platí, potom neexistuje class2 class3 tak, že class1 je podtřídou class3 a class2 se nerovná class3 a class1 se nerovná class3.
(=>
(immediateSubclass ?CLASS1 ?CLASS2)
(not
(exists
(?CLASS3)
(and
(subclass ?CLASS3 ?CLASS2)
(subclass ?CLASS1 ?CLASS3)
(not
(equal ?CLASS2 ?CLASS3))
(not
(equal ?CLASS1 ?CLASS3))))))
Jestliže thing1 se rovná thing2, potom pro všechny attr platí: thing1 má atribut attr tehdy a jen tehdy pokud thing2 má atribut attr.
(=>
(equal ?THING1 ?THING2)
(forall
(?ATTR)
(<=>
(property ?THING1 ?ATTR)
(property ?THING2 ?ATTR))))
Jestliže attr1 se rovná attr2, potom pro všechny thing platí: thing má atribut attr1 tehdy a jen tehdy pokud thing má atribut attr2.
(=>
(equal ?ATTR1 ?ATTR2)
(forall
(?THING)
(<=>
(property ?THING ?ATTR1)
(property ?THING ?ATTR2))))
Jestliže thing1 se rovná thing2, potom pro všechny class platí: thing1 je instancí třídy class tehdy a jen tehdy pokud thing2 je instancí třídy class.
(=>
(equal ?THING1 ?THING2)
(forall
(?CLASS)
(<=>
(instance ?THING1 ?CLASS)
(instance ?THING2 ?CLASS))))
Jestliže class1 se rovná class2, potom pro všechny thing platí: thing je instancí třídy class1 tehdy a jen tehdy pokud thing je instancí třídy class2.
(=>
(equal ?CLASS1 ?CLASS2)
(forall
(?THING)
(<=>
(instance ?THING ?CLASS1)
(instance ?THING ?CLASS2))))
Jestliže rel1 se rovná rel2, potom pro všechny platí: rel1() holds tehdy a jen tehdy pokud 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))))
- jestliže list1 se rovná list2,
- potom jestliže list1 se rovná "()" a list2 se rovná "()", potom pro všechny number platí: "numberth element of "()"" se rovná "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)))))
Jestliže range of function je an instance of class a "function()" se rovná value, potom value je instancí třídy class.
(=>
(and
(range ?FUNCTION ?CLASS)
(equal
(AssignmentFn ?FUNCTION @ROW)
?VALUE))
(instance ?VALUE ?CLASS))
Jestliže range subclass(function,class) platí a "function()" se rovná value, potom value je podtřídou class.
(=>
(and
(rangeSubclass ?FUNCTION ?CLASS)
(equal
(AssignmentFn ?FUNCTION @ROW)
?VALUE))
(subclass ?VALUE ?CLASS))
Jestliže and ? are disjoint a rel1 je a member of "()" a rel2 je a member of "()" a rel1 se nerovná rel2 a rel1() holds, potom 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)))
(=>
(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))))))
Jestliže rel(,inst) holds a rel je instancí třídy funkce, potom "rel()" se rovná 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))))
Jestliže mixture je instancí třídy směs, potom existují čistá látka pure1,čistá látka pure2 tak, že pure1 se nerovná pure2 a pure1 je a piece of mixture a pure2 je 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))))
Jestliže obj je instancí třídy složený objekt, potom existují látka substance1,látka substance2 tak, že substance1 je z obj a substance2 je z obj a substance1 se nerovná substance2.
(=>
(instance ?OBJ CorpuscularObject)
(exists
(?SUBSTANCE1 ?SUBSTANCE2)
(and
(subclass ?SUBSTANCE1 Substance)
(subclass ?SUBSTANCE2 Substance)
(material ?SUBSTANCE1 ?OBJ)
(material ?SUBSTANCE2 ?OBJ)
(not
(equal ?SUBSTANCE1 ?SUBSTANCE2)))))
Jestliže process je instancí třídy proces nad dvěma objekty, potom existují obj1,obj2 tak, že obj1 je účastníkem process a obj2 je účastníkem process a obj1 se nerovná obj2.
(=>
(instance ?PROCESS DualObjectProcess)
(exists
(?OBJ1 ?OBJ2)
(and
(patient ?PROCESS ?OBJ1)
(patient ?PROCESS ?OBJ2)
(not
(equal ?OBJ1 ?OBJ2)))))
"abstraction fn(class)" se rovná attr tehdy a jen tehdy pokud pro všechny inst platí: inst je instancí třídy class tehdy a jen tehdy pokud inst má atribut attr.
(<=>
(equal
(AbstractionFn ?CLASS)
?ATTR)
(forall
(?INST)
(<=>
(instance ?INST ?CLASS)
(property ?INST ?ATTR))))
"extension fn(attribute)" se rovná class tehdy a jen tehdy pokud "abstraction fn(class)" se rovná attribute.
(<=>
(equal
(ExtensionFn ?ATTRIBUTE)
?CLASS)
(equal
(AbstractionFn ?CLASS)
?ATTRIBUTE))
number1 je menší než nebo roven number2 tehdy a jen tehdy pokud number1 se rovná number2 nebo number1 je menší než number2.
(<=>
(lessThanOrEqualTo ?NUMBER1 ?NUMBER2)
(or
(equal ?NUMBER1 ?NUMBER2)
(lessThan ?NUMBER1 ?NUMBER2)))
number1 je větší než nebo roven number2 tehdy a jen tehdy pokud number1 se rovná number2 nebo number1 je větší než number2.
(<=>
(greaterThanOrEqualTo ?NUMBER1 ?NUMBER2)
(or
(equal ?NUMBER1 ?NUMBER2)
(greaterThan ?NUMBER1 ?NUMBER2)))
Jestliže number je instancí třídy imaginární číslo, potom existuje reálné číslo real tak, že number se rovná "real*"square root fn()"".
(=>
(instance ?NUMBER ImaginaryNumber)
(exists
(?REAL)
(and
(instance ?REAL RealNumber)
(equal
?NUMBER
(MultiplicationFn
?REAL
(SquareRootFn -1))))))
Jestliže number je instancí třídy komplexní číslo, potom existují reálné číslo real1,reálné číslo real2 tak, že number se rovná "(real1+"real2*"square root fn()"")".
(=>
(instance ?NUMBER ComplexNumber)
(exists
(?REAL1 ?REAL2)
(and
(instance ?REAL1 RealNumber)
(instance ?REAL2 RealNumber)
(equal
?NUMBER
(AdditionFn
?REAL1
(MultiplicationFn
?REAL2
(SquareRootFn -1)))))))
rel je instancí třídy relace s jedinou hodnotou tehdy a jen tehdy pokud pro všechny ,item1,item2 platí: jestliže rel(,item1) holds a rel(,item2) holds, potom item1 se rovná item2.
(<=>
(instance ?REL SingleValuedRelation)
(forall
(@ROW ?ITEM1 ?ITEM2)
(=>
(and
(holds ?REL @ROW ?ITEM1)
(holds ?REL @ROW ?ITEM2))
(equal ?ITEM1 ?ITEM2))))
rel je instancí třídy úplná relace tehdy a jen tehdy pokud existuje valence tak, že rel je instancí třídy relace a rel has valence argument(s) a - jestliže pro všechny number,element,class platí: jestliže number je menší než valence a numberth argument of rel je an instance of class a element se rovná "numberth element of "()"", potom element je instancí třídy class,
- potom existuje item tak, že 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))))
Jestliže rel je instancí třídy trichotomická relace, potom pro všechny inst1,inst2 platí: rel(inst1,inst2) holds nebo inst1 se rovná inst2 nebo rel(inst2,inst1) holds.
(=>
(instance ?REL TrichotomizingRelation)
(forall
(?INST1 ?INST2)
(or
(holds ?REL ?INST1 ?INST2)
(equal ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST1))))
Jestliže formula1 increases likelihood of formula2 a "probability fn(formula2)" se rovná number1 a probability of formula1 provided that formula2 holds je formula2, potom number2 je větší než number1.
(=>
(and
(increasesLikelihood ?FORMULA1 ?FORMULA2)
(equal
(ProbabilityFn ?FORMULA2)
?NUMBER1)
(conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
(greaterThan ?NUMBER2 ?NUMBER1))
Jestliže formula1 decreases likelihood of formula2 a "probability fn(formula2)" se rovná number1 a probability of formula1 provided that formula2 holds je formula2, potom number2 je menší než number1.
(=>
(and
(decreasesLikelihood ?FORMULA1 ?FORMULA2)
(equal
(ProbabilityFn ?FORMULA2)
?NUMBER1)
(conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
(lessThan ?NUMBER2 ?NUMBER1))
Jestliže probability of formula1 and formula2 je independent a "probability fn(formula2)" se rovná number1 a probability of formula1 provided that formula2 holds je formula2, potom number2 se rovná number1.
(=>
(and
(independentProbability ?FORMULA1 ?FORMULA2)
(equal
(ProbabilityFn ?FORMULA2)
?NUMBER1)
(conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
(equal ?NUMBER2 ?NUMBER1))
(=>
(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 je instancí třídy seznam bez duplicit tehdy a jen tehdy pokud pro všechny number1,number2 platí: jestliže "number1th element of list" se rovná "number2th element of list", potom number1 se rovná number2.
(<=>
(instance ?LIST UniqueList)
(forall
(?NUMBER1 ?NUMBER2)
(=>
(equal
(ListOrderFn ?LIST ?NUMBER1)
(ListOrderFn ?LIST ?NUMBER2))
(equal ?NUMBER1 ?NUMBER2))))
list se rovná null list tehdy a jen tehdy pokud neexistuje item tak, že item je a member of list.
(<=>
(equal ?LIST NullList)
(not
(exists
(?ITEM)
(inList ?ITEM ?LIST))))
- jestliže class je disjointly decomposed into ,
- potom pro všechny item1,item2 platí: jestliže item1 je a member of "()" a item2 je a member of "()" a item1 se nerovná item2, potom item1 je 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))))
Jestliže list1 je instancí třídy seznam a list2 je instancí třídy seznam a pro všechny number platí: "numberth element of list1" se rovná "numberth element of list2", potom list1 se rovná list2.
(=>
(and
(instance ?LIST1 List)
(instance ?LIST2 List)
(forall
(?NUMBER)
(equal
(ListOrderFn ?LIST1 ?NUMBER)
(ListOrderFn ?LIST2 ?NUMBER))))
(equal ?LIST1 ?LIST2))
Jestliže "length of list" se rovná number1, potom pro všechny number2 platí: existuje item tak, že "number2th element of list" se rovná item tehdy a jen tehdy pokud number2 je menší než nebo roven number1.
(=>
(equal
(ListLengthFn ?LIST)
?NUMBER1)
(forall
(?NUMBER2)
(<=>
(exists
(?ITEM)
(equal
(ListOrderFn ?LIST ?NUMBER2)
?ITEM))
(lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))
"length of "(,item)"" se rovná "("length of "()""+1)".
(equal
(ListLengthFn
(ListFn @ROW ?ITEM))
(SuccessorFn
(ListLengthFn
(ListFn @ROW))))
""length of "(,item)""th element of "(,item)"" se rovná item.
(equal
(ListOrderFn
(ListFn @ROW ?ITEM)
(ListLengthFn
(ListFn @ROW ?ITEM)))
?ITEM)
(=>
(valence ?REL ?NUMBER)
(forall
(@ROW)
(=>
(holds ?REL @ROW)
(equal
(ListLengthFn
(ListFn @ROW))
?NUMBER))))
Jestliže "length of list1" se rovná number, potom existuje list2 tak, že list1 starts list2 a "(number+1)" se rovná "length of list2" a ""(number+1)"th element of list2" se rovná item.
(=>
(equal
(ListLengthFn ?LIST1)
?NUMBER)
(exists
(?LIST2)
(and
(initialList ?LIST1 ?LIST2)
(equal
(SuccessorFn ?NUMBER)
(ListLengthFn ?LIST2))
(equal
(ListOrderFn
?LIST2
(SuccessorFn ?NUMBER))
?ITEM))))
list3 se rovná "list concatenate fn(list1,list2)" tehdy a jen tehdy pokud pro všechny number1,number2 platí: jestliže number1 je menší než nebo roven "length of list1" a number2 je menší než nebo roven "length of list2" a number1 je instancí třídy kladné celé číslo a number2 je instancí třídy kladné celé číslo, potom "number1th element of list3" se rovná "number1th element of list1" a ""("length of list1"+number2)"th element of list3" se rovná "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 je a member of list tehdy a jen tehdy pokud existuje number tak, že "numberth element of list" se rovná item.
(<=>
(inList ?ITEM ?LIST)
(exists
(?NUMBER)
(equal
(ListOrderFn ?LIST ?NUMBER)
?ITEM)))
- jestliže list1 je a sublist of list2,
- potom existuje number3 tak, že pro všechny item platí: jestliže item je a member of list1, potom existují number1,number2 tak, že "number1th element of list1" se rovná item a "number2th element of list2" se rovná item a number2 se rovná "(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))))))))
- jestliže list1 starts list2,
- potom pro všechny number1,number2 platí: jestliže "length of list1" se rovná number1 a number2 je menší než nebo roven number1, potom "number2th element of list1" se rovná "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))))))
- jestliže function je instancí třídy asociativní funkce,
- potom pro všechny inst1,inst2,inst3 platí: jestliže th argument of function je an instance of class a inst1 je instancí třídy class a inst2 je instancí třídy class a inst3 je instancí třídy class, potom "function(inst1,"function(inst2,inst3)")" se rovná "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)))))
- jestliže function je instancí třídy komutativní funkce,
- potom pro všechny inst1,inst2 platí: jestliže th argument of function je an instance of class a inst1 je instancí třídy class a inst2 je instancí třídy class, potom "function(inst1,inst2)" se rovná "function(inst2,inst1)"
.
(=>
(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)))))
- jestliže relation je trichotomizing on class,
- potom pro všechny inst1,inst2 platí: jestliže inst1 je instancí třídy class a inst2 je instancí třídy class, potom relation(inst1,inst2) holds nebo relation(inst2,inst1) holds nebo inst1 se rovná 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)))))
- jestliže function1 je distributive over function2,
- potom pro všechny inst1,inst2,inst3 platí: jestliže th argument of function1 je an instance of class1 a inst1 je instancí třídy class1 a inst2 je instancí třídy class1 a inst3 je instancí třídy class1 a th argument of function2 je an instance of class2 a inst1 je instancí třídy class2 a inst2 je instancí třídy class2 a inst3 je instancí třídy class2, potom "function1(inst1,"function2(inst2,inst3)")" se rovná "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))))))
Jestliže obj je přesně umístěn v region, potom neexistuje otherobj tak, že otherobj je přesně umístěn v region a otherobj se nerovná obj.
(=>
(exactlyLocated ?OBJ ?REGION)
(not
(exists
(?OTHEROBJ)
(and
(exactlyLocated ?OTHEROBJ ?REGION)
(not
(equal ?OTHEROBJ ?OBJ))))))
"místo kde thing byl v čase time" se rovná region tehdy a jen tehdy pokud thing je přesně umístěn v region během time.
(<=>
(equal
(WhereFn ?THING ?TIME)
?REGION)
(holdsDuring
?TIME
(exactlyLocated ?THING ?REGION)))
Jestliže time je instancí třídy časová pozice a agent1 posesses obj během time a agent2 posesses obj během time, potom agent1 se rovná agent2.
(=>
(and
(instance ?TIME TimePosition)
(holdsDuring
?TIME
(possesses ?AGENT1 ?OBJ))
(holdsDuring
?TIME
(possesses ?AGENT2 ?OBJ)))
(equal ?AGENT1 ?AGENT2))
"(number+1)" se rovná "(number+)".
(equal
(SuccessorFn ?NUMBER)
(AdditionFn ?NUMBER 1))
"(number+2)" se rovná "(number-)".
(equal
(PredecessorFn ?NUMBER)
(SubtractionFn ?NUMBER 1))
Jestliže number je instancí třídy racionální číslo, potom existují celé číslo int1,celé číslo int2 tak, že number se rovná "int1/int2".
(=>
(instance ?NUMBER RationalNumber)
(exists
(?INT1 ?INT2)
(and
(instance ?INT1 Integer)
(instance ?INT2 Integer)
(equal
?NUMBER
(DivisionFn ?INT1 ?INT2)))))
"absolute value fn(number1)" se rovná number2 a number1 je instancí třídy reálné číslo a number2 je instancí třídy reálné číslo tehdy a jen tehdy pokud
(<=>
(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)))))
Jestliže "ceiling fn(number)" se rovná int, potom neexistuje celé číslo otherint tak, že otherint je větší než nebo roven number a otherint je menší než int.
(=>
(equal
(CeilingFn ?NUMBER)
?INT)
(not
(exists
(?OTHERINT)
(and
(instance ?OTHERINT Integer)
(greaterThanOrEqualTo ?OTHERINT ?NUMBER)
(lessThan ?OTHERINT ?INT)))))
Jestliže "floor fn(number)" se rovná int, potom neexistuje celé číslo otherint tak, že otherint je menší než nebo roven number a otherint je větší než int.
(=>
(equal
(FloorFn ?NUMBER)
?INT)
(not
(exists
(?OTHERINT)
(and
(instance ?OTHERINT Integer)
(lessThanOrEqualTo ?OTHERINT ?NUMBER)
(greaterThan ?OTHERINT ?INT)))))
(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?NUMBER)
0))))
(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(not
(exists
(?GREATER)
(and
(greaterThan ?GREATER ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?GREATER)
0)))))))
Jestliže number je instancí třídy komplexní číslo, potom existují part1,part2 tak, že part1 se rovná "real number fn(number)" a part2 se rovná "imaginary part fn(number)".
(=>
(instance ?NUMBER ComplexNumber)
(exists
(?PART1 ?PART2)
(and
(equal
?PART1
(RealNumberFn ?NUMBER))
(equal
?PART2
(ImaginaryPartFn ?NUMBER)))))
(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?NUMBER ?ELEMENT)
0))))
(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(not
(exists
(?LESS)
(and
(lessThan ?LESS ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?LESS ?ELEMENT)
0)))))))
Jestliže "max fn(number1,number2)" se rovná number, potom - number se rovná number1 a number1 je větší než number2
nebo - number se rovná number2 a number2 je větší než number1
nebo - number se rovná number1 a number se rovná 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))))
Jestliže "min fn(number1,number2)" se rovná number, potom - number se rovná number1 a number1 je menší než number2
nebo - number se rovná number2 a number2 je menší než number1
nebo - number se rovná number1 a number se rovná 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))))
Jestliže number je instancí třídy veličina, potom "reciprocal fn(number)" se rovná "exponentiation fn(number,)".
(=>
(instance ?NUMBER Quantity)
(equal
(ReciprocalFn ?NUMBER)
(ExponentiationFn ?NUMBER -1)))
Jestliže number je instancí třídy veličina, potom se rovná "number*"reciprocal fn(number)"".
(=>
(instance ?NUMBER Quantity)
(equal
1
(MultiplicationFn
?NUMBER
(ReciprocalFn ?NUMBER))))
"number1 mod number2" se rovná number tehdy a jen tehdy pokud "(""floor fn(number1/number2)"*number2"+number)" se rovná number1.
(<=>
(equal
(RemainderFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(equal
(AdditionFn
(MultiplicationFn
(FloorFn
(DivisionFn ?NUMBER1 ?NUMBER2))
?NUMBER2)
?NUMBER)
?NUMBER1))
Jestliže "number1 mod number2" se rovná number, potom "signum fn(number2)" se rovná "signum fn(number)".
(=>
(equal
(RemainderFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(equal
(SignumFn ?NUMBER2)
(SignumFn ?NUMBER)))
Jestliže number je instancí třídy sudé celé číslo, potom "number mod " se rovná .
(=>
(instance ?NUMBER EvenInteger)
(equal
(RemainderFn ?NUMBER 2)
0))
Jestliže number je instancí třídy liché celé číslo, potom "number mod " se rovná .
(=>
(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)))))
(=>
(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)))))
Jestliže number je instancí třídy nezáporné reálné číslo, potom "signum fn(number)" se rovná nebo "signum fn(number)" se rovná .
(=>
(instance ?NUMBER NonnegativeRealNumber)
(or
(equal
(SignumFn ?NUMBER)
1)
(equal
(SignumFn ?NUMBER)
0)))
Jestliže number je instancí třídy kladné reálné číslo, potom "signum fn(number)" se rovná .
(=>
(instance ?NUMBER PositiveRealNumber)
(equal
(SignumFn ?NUMBER)
1))
Jestliže number je instancí třídy záporné reálné číslo, potom "signum fn(number)" se rovná .
(=>
(instance ?NUMBER NegativeRealNumber)
(equal
(SignumFn ?NUMBER)
-1))
Jestliže "square root fn(number1)" se rovná number2, potom "number2*number2" se rovná number1.
(=>
(equal
(SquareRootFn ?NUMBER1)
?NUMBER2)
(equal
(MultiplicationFn ?NUMBER2 ?NUMBER2)
?NUMBER1))
Jestliže degree je instancí třídy jednotka plošného úhlu, potom "tangent fn(degree)" se rovná ""sine fn(degree)"/"cosine fn(degree)"".
(=>
(instance ?DEGREE PlaneAngleMeasure)
(equal
(TangentFn ?DEGREE)
(DivisionFn
(SineFn ?DEGREE)
(CosineFn ?DEGREE))))
- jestliže id je an identity element of function,
- potom pro všechny inst platí: jestliže th argument of function je an instance of class a inst je instancí třídy class, potom "function(id,inst)" se rovná inst
.
(=>
(identityElement ?FUNCTION ?ID)
(forall
(?INST)
(=>
(and
(domain ?FUNCTION 1 ?CLASS)
(instance ?INST ?CLASS))
(equal
(AssignmentFn ?FUNCTION ?ID ?INST)
?INST))))
Jestliže "(int1+1)" se rovná "(int2+1)", potom int1 se rovná int2.
(=>
(equal
(SuccessorFn ?INT1)
(SuccessorFn ?INT2))
(equal ?INT1 ?INT2))
Jestliže int je instancí třídy celé číslo, potom int se rovná "("(int+2)"+1)".
(=>
(instance ?INT Integer)
(equal
?INT
(SuccessorFn
(PredecessorFn ?INT))))
Jestliže int je instancí třídy celé číslo, potom int se rovná "("(int+1)"+2)".
(=>
(instance ?INT Integer)
(equal
?INT
(PredecessorFn
(SuccessorFn ?INT))))
Jestliže "(int1+2)" se rovná "(int2+2)", potom int1 se rovná int2.
(=>
(equal
(PredecessorFn ?INT1)
(PredecessorFn ?INT2))
(equal ?INT1 ?INT2))
Jestliže pro všechny element platí: element je an element of set1 tehdy a jen tehdy pokud element je an element of set2, potom set1 se rovná set2.
(=>
(forall
(?ELEMENT)
(<=>
(element ?ELEMENT ?SET1)
(element ?ELEMENT ?SET2)))
(equal ?SET1 ?SET2))
Jestliže set je instancí třídy konečná množina, potom existuje nezáporné celé číslo number tak, že number se rovná "cardinality fn(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)))))
Jestliže graph je instancí třídy graf a node1 je instancí třídy uzel grafu a node2 je instancí třídy uzel grafu a node1 je částí graph a node2 je částí graph a node1 se nerovná node2, potom existují arc,path tak, že
(=>
(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)))))))
Jestliže graph je instancí třídy graf, potom existují node1,node2,node3,arc1,arc2 tak, že node1 je částí graph a node2 je částí graph a node3 je částí graph a arc1 je částí graph a arc2 je částí graph a node2 spojuje arc1 a node1 a node3 spojuje arc2 a node2 a node1 se nerovná node2 a node2 se nerovná node3 a node1 se nerovná node3 a arc1 se nerovná 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)))))
Jestliže graph je instancí třídy orientovaný graf a arc je instancí třídy hrana grafu a arc je částí graph, potom existují node1,node2 tak, že "initial node fn(arc)" se rovná node1 a "terminal node fn(arc)" se rovná 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 je instancí třídy cyklus tehdy a jen tehdy pokud existuje node tak, že "the beginning of graph" se rovná node a "the end of graph" se rovná node.
(<=>
(instance ?GRAPH GraphCircuit)
(exists
(?NODE)
(and
(equal
(BeginNodeFn ?GRAPH)
?NODE)
(equal
(EndNodeFn ?GRAPH)
?NODE))))
graph je instancí třídy multigraf tehdy a jen tehdy pokud existují arc1,arc2,node1,node2 tak, že arc1 je částí graph a arc2 je částí graph a node1 je částí graph a node2 je částí graph a arc1 spojuje node1 a node2 a arc2 spojuje node1 a node2 a arc1 se nerovná 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)))))
Jestliže "initial node fn(arc)" se rovná node a "terminal node fn(arc)" se rovná node, potom arc je instancí třídy smyčka grafu.
(=>
(and
(equal
(InitialNodeFn ?ARC)
?NODE)
(equal
(TerminalNodeFn ?ARC)
?NODE))
(instance ?ARC GraphLoop))
(=>
(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)))
(=>
(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)))
Jestliže "minimal weighted path fn(node1,node2)" se rovná path, potom path je instancí třídy "graph path fn(node1,node2)".
(=>
(equal
(MinimalWeightedPathFn ?NODE1 ?NODE2)
?PATH)
(instance
?PATH
(GraphPathFn ?NODE1 ?NODE2)))
(=>
(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))))
Jestliže "maximal weighted path fn(node1,node2)" se rovná path, potom path je instancí třídy "graph path fn(node1,node2)".
(=>
(equal
(MaximalWeightedPathFn ?NODE1 ?NODE2)
?PATH)
(instance
?PATH
(GraphPathFn ?NODE1 ?NODE2)))
(=>
(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))))
Jestliže path je částí graph a graph není instancí třídy orientovaný graf, potom "graph path fn(node1,node2)" se rovná path tehdy a jen tehdy pokud "graph path fn(node2,node1)" se rovná path.
(=>
(and
(graphPart ?PATH ?GRAPH)
(not
(instance ?GRAPH DirectedGraph)))
(<=>
(equal
(GraphPathFn ?NODE1 ?NODE2)
?PATH)
(equal
(GraphPathFn ?NODE2 ?NODE1)
?PATH)))
- jestliže "minimal cut set fn(graph)" se rovná pathclass,
- potom existuje number tak, že pro všechny path platí: jestliže path je instancí třídy pathclass, potom délka path je number
.
(=>
(equal
(MinimalCutSetFn ?GRAPH)
?PATHCLASS)
(exists
(?NUMBER)
(forall
(?PATH)
(=>
(instance ?PATH ?PATHCLASS)
(pathLength ?PATH ?NUMBER)))))
Jestliže "number unit(s)" se rovná quant a unit je podtřídou quanttype, potom quant je instancí třídy quanttype.
(=>
(and
(equal
(MeasureFn ?NUMBER ?UNIT)
?QUANT)
(subclass ?UNIT ?QUANTTYPE))
(instance ?QUANT ?QUANTTYPE))
Jestliže unit je instancí třídy měrná jednotka, potom "kilo fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(KiloFn ?UNIT)
(MeasureFn 1000 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "mega fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MegaFn ?UNIT)
(MeasureFn 1000000 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "giga fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(GigaFn ?UNIT)
(MeasureFn 1000000000 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "tera fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(TeraFn ?UNIT)
(MeasureFn 1000000000000 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "milli fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MilliFn ?UNIT)
(MeasureFn 0.001 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "micro fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MicroFn ?UNIT)
(MeasureFn 0.000001 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "nano fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(NanoFn ?UNIT)
(MeasureFn 0.000000001 ?UNIT)))
Jestliže unit je instancí třídy měrná jednotka, potom "pico fn(unit)" se rovná " unit(s)".
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(PicoFn ?UNIT)
(MeasureFn 0.000000000001 ?UNIT)))
Jestliže number je instancí třídy reálné číslo a unit je instancí třídy měrná jednotka, potom "magnitude fn(number unit(s))" se rovná number.
(=>
(and
(instance ?NUMBER RealNumber)
(instance ?UNIT UnitOfMeasure))
(equal
(MagnitudeFn
(MeasureFn ?NUMBER ?UNIT))
?NUMBER))
Jestliže number je instancí třídy reálné číslo, potom "number centimeter(s)" se rovná ""number*" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Centimeter)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
Meter)))
Jestliže number je instancí třídy reálné číslo, potom "number celsius degree(s)" se rovná ""(number-)" kelvin degree(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER CelsiusDegree)
(MeasureFn
(SubtractionFn ?NUMBER 273.15)
KelvinDegree)))
Jestliže number je instancí třídy reálné číslo, potom "number celsius degree(s)" se rovná """(number-)"/" fahrenheit degree(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER CelsiusDegree)
(MeasureFn
(DivisionFn
(SubtractionFn ?NUMBER 32)
1.8)
FahrenheitDegree)))
Jestliže number je instancí třídy reálné číslo, potom "number day duration(s)" se rovná ""number*" hour duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER DayDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 24)
HourDuration)))
Jestliže number je instancí třídy reálné číslo, potom "number hour duration(s)" se rovná ""number*" minute duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER HourDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 60)
MinuteDuration)))
Jestliže number je instancí třídy reálné číslo, potom "number minute duration(s)" se rovná ""number*" second duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER MinuteDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 60)
SecondDuration)))
Jestliže number je instancí třídy reálné číslo, potom "number week duration(s)" se rovná ""number*" day duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER WeekDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 7)
DayDuration)))
Jestliže number je instancí třídy reálné číslo, potom "number year duration(s)" se rovná ""number*" day duration(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER YearDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 365)
DayDuration)))
Jestliže number je instancí třídy reálné číslo, potom "number amu(s)" se rovná ""number**" gram(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Amu)
(MeasureFn
(MultiplicationFn ?NUMBER 1.6605402 E-24)
Gram)))
Jestliže number je instancí třídy reálné číslo, potom "number electron volt(s)" se rovná ""number**" joule(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER ElectronVolt)
(MeasureFn
(MultiplicationFn ?NUMBER 1.60217733 E-19)
Joule)))
Jestliže number je instancí třídy reálné číslo, potom "number angstrom(s)" se rovná ""number**" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Angstrom)
(MeasureFn
(MultiplicationFn ?NUMBER 1.0 E-10)
Meter)))
Jestliže number je instancí třídy reálné číslo, potom "number foot(s)" se rovná ""number*" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Foot)
(MeasureFn
(MultiplicationFn ?NUMBER 0.3048)
Meter)))
Jestliže number je instancí třídy reálné číslo, potom "number inch(s)" se rovná ""number*" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Inch)
(MeasureFn
(MultiplicationFn ?NUMBER 0.0254)
Meter)))
Jestliže number je instancí třídy reálné číslo, potom "number mile(s)" se rovná ""number*" meter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Mile)
(MeasureFn
(MultiplicationFn ?NUMBER 1609.344)
Meter)))
Jestliže number je instancí třídy reálné číslo, potom "number united states gallon(s)" se rovná ""number*" liter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedStatesGallon)
(MeasureFn
(MultiplicationFn ?NUMBER 3.785411784)
Liter)))
Jestliže number je instancí třídy reálné číslo, potom "number quart(s)" se rovná ""number/" united states gallon(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Quart)
(MeasureFn
(DivisionFn ?NUMBER 4)
UnitedStatesGallon)))
Jestliže number je instancí třídy reálné číslo, potom "number pint(s)" se rovná ""number/" quart(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Pint)
(MeasureFn
(DivisionFn ?NUMBER 2)
Quart)))
Jestliže number je instancí třídy reálné číslo, potom "number cup(s)" se rovná ""number/" pint(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Cup)
(MeasureFn
(DivisionFn ?NUMBER 2)
Pint)))
Jestliže number je instancí třídy reálné číslo, potom "number ounce(s)" se rovná ""number/" cup(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Ounce)
(MeasureFn
(DivisionFn ?NUMBER 8)
Cup)))
Jestliže number je instancí třídy reálné číslo, potom "number united kingdom gallon(s)" se rovná ""number*" liter(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedKingdomGallon)
(MeasureFn
(MultiplicationFn ?NUMBER 4.54609)
Liter)))
Jestliže number je instancí třídy reálné číslo, potom "number pound mass(s)" se rovná ""number*" gram(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER PoundMass)
(MeasureFn
(MultiplicationFn ?NUMBER 453.59237)
Gram)))
Jestliže number je instancí třídy reálné číslo, potom "number slug(s)" se rovná ""number*" gram(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Slug)
(MeasureFn
(MultiplicationFn ?NUMBER 14593.90)
Gram)))
Jestliže number je instancí třídy reálné číslo, potom "number rankine degree(s)" se rovná ""number*" kelvin degree(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER RankineDegree)
(MeasureFn
(MultiplicationFn ?NUMBER 1.8)
KelvinDegree)))
Jestliže number je instancí třídy reálné číslo, potom "number pound force(s)" se rovná ""number*" newton(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER PoundForce)
(MeasureFn
(MultiplicationFn ?NUMBER 4.448222)
Newton)))
Jestliže number je instancí třídy reálné číslo, potom "number calorie(s)" se rovná ""number*" joule(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Calorie)
(MeasureFn
(MultiplicationFn ?NUMBER 4.1868)
Joule)))
Jestliže number je instancí třídy reálné číslo, potom "number british thermal unit(s)" se rovná ""number*" joule(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER BritishThermalUnit)
(MeasureFn
(MultiplicationFn ?NUMBER 1055.05585262)
Joule)))
Jestliže number je instancí třídy reálné číslo, potom "number angular degree(s)" se rovná ""number*"pi/"" radian(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER AngularDegree)
(MeasureFn
(MultiplicationFn
?NUMBER
(DivisionFn Pi 180))
Radian)))
Jestliže number je instancí třídy reálné číslo, potom "number united states cent(s)" se rovná ""number*" united states dollar(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedStatesCent)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
UnitedStatesDollar)))
Jestliže number je instancí třídy reálné číslo, potom "number euro cent(s)" se rovná ""number*" euro dollar(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER EuroCent)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
EuroDollar)))
Jestliže number je instancí třídy reálné číslo, potom "number byte(s)" se rovná ""number*" bit(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Byte)
(MeasureFn
(MultiplicationFn ?NUMBER 8)
Bit)))
Jestliže number je instancí třídy reálné číslo, potom "number kilo byte(s)" se rovná ""number*" byte(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER KiloByte)
(MeasureFn
(MultiplicationFn ?NUMBER 1024)
Byte)))
Jestliže number je instancí třídy reálné číslo, potom "number mega byte(s)" se rovná ""number*" kilo byte(s)".
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER MegaByte)
(MeasureFn
(MultiplicationFn ?NUMBER 1024)
KiloByte)))
"value of belongings of person" se rovná amount tehdy a jen tehdy pokud value of "belongings of person" je amount.
(<=>
(equal
(WealthFn ?PERSON)
?AMOUNT)
(monetaryValue
(PropertyFn ?PERSON)
?AMOUNT))
Jestliže point je instancí třídy okamžik a point se nerovná positive infinity, potom point happens before positive infinity.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT PositiveInfinity)))
(before ?POINT PositiveInfinity))
Jestliže point je instancí třídy okamžik a point se nerovná positive infinity, potom existuje otherpoint tak, že otherpoint je between point and positive infinity.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT PositiveInfinity)))
(exists
(?OTHERPOINT)
(temporallyBetween ?POINT ?OTHERPOINT PositiveInfinity)))
Jestliže point je instancí třídy okamžik a point se nerovná negative infinity, potom negative infinity happens before point.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT NegativeInfinity)))
(before NegativeInfinity ?POINT))
Jestliže point je instancí třídy okamžik a point se nerovná negative infinity, potom existuje otherpoint tak, že otherpoint je between negative infinity and point.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT NegativeInfinity)))
(exists
(?OTHERPOINT)
(temporallyBetween NegativeInfinity ?OTHERPOINT ?POINT)))
- jestliže "the beginning of interval" se rovná point,
- potom pro všechny otherpoint platí: jestliže otherpoint je a part of interval a otherpoint se nerovná point, potom point happens before otherpoint
.
(=>
(equal
(BeginFn ?INTERVAL)
?POINT)
(forall
(?OTHERPOINT)
(=>
(and
(temporalPart ?OTHERPOINT ?INTERVAL)
(not
(equal ?OTHERPOINT ?POINT)))
(before ?POINT ?OTHERPOINT))))
- jestliže "the end of interval" se rovná point,
- potom pro všechny otherpoint platí: jestliže otherpoint je a part of interval a otherpoint se nerovná point, potom otherpoint happens before point
.
(=>
(equal
(EndFn ?INTERVAL)
?POINT)
(forall
(?OTHERPOINT)
(=>
(and
(temporalPart ?OTHERPOINT ?INTERVAL)
(not
(equal ?OTHERPOINT ?POINT)))
(before ?OTHERPOINT ?POINT))))
interval1 starts interval2 tehdy a jen tehdy pokud "the beginning of interval1" se rovná "the beginning of interval2" a "the end of interval1" happens before the end of interval2.
(<=>
(starts ?INTERVAL1 ?INTERVAL2)
(and
(equal
(BeginFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(before
(EndFn ?INTERVAL1)
(EndFn ?INTERVAL2))))
interval1 finishes interval2 tehdy a jen tehdy pokud "the beginning of interval2" happens before the beginning of interval1 a "the end of interval2" se rovná "the end of interval1".
(<=>
(finishes ?INTERVAL1 ?INTERVAL2)
(and
(before
(BeginFn ?INTERVAL2)
(BeginFn ?INTERVAL1))
(equal
(EndFn ?INTERVAL2)
(EndFn ?INTERVAL1))))
Jestliže point1 happen?{s} before or at point2, potom point1 happens before point2 nebo point1 se rovná point2.
(=>
(beforeOrEqual ?POINT1 ?POINT2)
(or
(before ?POINT1 ?POINT2)
(equal ?POINT1 ?POINT2)))
interval1 meets interval2 tehdy a jen tehdy pokud "the end of interval1" se rovná "the beginning of interval2".
(<=>
(meetsTemporally ?INTERVAL1 ?INTERVAL2)
(equal
(EndFn ?INTERVAL1)
(BeginFn ?INTERVAL2)))
Jestliže "the beginning of interval1" se rovná "the beginning of interval2" a "the end of interval1" se rovná "the end of interval2", potom interval1 se rovná interval2.
(=>
(and
(equal
(BeginFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(equal
(EndFn ?INTERVAL1)
(EndFn ?INTERVAL2)))
(equal ?INTERVAL1 ?INTERVAL2))
phys1 occurs at the same time as phys2 tehdy a jen tehdy pokud "doba existence phys1" se rovná "doba existence phys2".
(<=>
(cooccur ?PHYS1 ?PHYS2)
(equal
(WhenFn ?PHYS1)
(WhenFn ?PHYS2)))
Jestliže "interval between point1 and point2" se rovná interval, potom "the beginning of interval" se rovná point1 a "the end of interval" se rovná point2.
(=>
(equal
(TimeIntervalFn ?POINT1 ?POINT2)
?INTERVAL)
(and
(equal
(BeginFn ?INTERVAL)
?POINT1)
(equal
(EndFn ?INTERVAL)
?POINT2)))
Jestliže "interval between point1 and point2" se rovná interval, potom pro všechny point platí: point je between or at point1 and point2 tehdy a jen tehdy pokud point je a part of interval.
(=>
(equal
(TimeIntervalFn ?POINT1 ?POINT2)
?INTERVAL)
(forall
(?POINT)
(<=>
(temporallyBetweenOrEqual ?POINT1 ?POINT ?POINT2)
(temporalPart ?POINT ?INTERVAL))))
Jestliže process je instancí třídy fyzický objekt, potom "před doba existence process" se rovná "interval between negative infinity and "the beginning of doba existence process"".
(=>
(instance ?PROCESS Physical)
(equal
(PastFn
(WhenFn ?PROCESS))
(TimeIntervalFn
NegativeInfinity
(BeginFn
(WhenFn ?PROCESS)))))
Jestliže process je instancí třídy fyzický objekt, potom "po doba existence process" se rovná "interval between "the end of doba existence process" and positive infinity".
(=>
(instance ?PROCESS Physical)
(equal
(FutureFn
(WhenFn ?PROCESS))
(TimeIntervalFn
(EndFn
(WhenFn ?PROCESS))
PositiveInfinity)))
Jestliže day1 je instancí třídy "number1 of month" a day2 je instancí třídy "number2 of month" a "(number2-number1)" se rovná , potom day1 meets day2.
(=>
(and
(instance
?DAY1
(DayFn ?NUMBER1 ?MONTH))
(instance
?DAY2
(DayFn ?NUMBER2 ?MONTH))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?DAY1 ?DAY2))
Jestliže hour1 je instancí třídy "number1 of day" a hour2 je instancí třídy "number2 of day" a "(number2-number1)" se rovná , potom hour1 meets hour2.
(=>
(and
(instance
?HOUR1
(HourFn ?NUMBER1 ?DAY))
(instance
?HOUR2
(HourFn ?NUMBER2 ?DAY))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?HOUR1 ?HOUR2))
Jestliže minute1 je instancí třídy "number1 of hour" a minute2 je instancí třídy "number2 of hour" a "(number2-number1)" se rovná , potom minute1 meets minute2.
(=>
(and
(instance
?MINUTE1
(MinuteFn ?NUMBER1 ?HOUR))
(instance
?MINUTE2
(MinuteFn ?NUMBER2 ?HOUR))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?MINUTE1 ?MINUTE2))
Jestliže second1 je instancí třídy "number1 of minute" a second2 je instancí třídy "number2 of minute" a "(number2-number1)" se rovná , potom second1 meets second2.
(=>
(and
(instance
?SECOND1
(SecondFn ?NUMBER1 ?MINUTE))
(instance
?SECOND2
(SecondFn ?NUMBER2 ?MINUTE))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?SECOND1 ?SECOND2))
Jestliže year1 je instancí třídy rok a year2 je instancí třídy rok a "(year2-year1)" se rovná , potom year1 meets year2.
(=>
(and
(instance ?YEAR1 Year)
(instance ?YEAR2 Year)
(equal
(SubtractionFn ?YEAR2 ?YEAR1)
1))
(meetsTemporally ?YEAR1 ?YEAR2))
Jestliže leap je instancí třídy přestupný rok a leap se rovná "number rok(s)", potom
(=>
(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)))
Jestliže month1 se rovná "leden of year" a month2 se rovná "únor of year", potom month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn January ?YEAR))
(equal
?MONTH2
(MonthFn February ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Jestliže "únor of year" se rovná month a year není instancí třídy přestupný rok, potom duration of month je " day duration(s)".
(=>
(and
(equal
(MonthFn February ?YEAR)
?MONTH)
(not
(instance ?YEAR LeapYear)))
(duration
?MONTH
(MeasureFn 28 DayDuration)))
Jestliže "únor of year" se rovná month a year je instancí třídy přestupný rok, potom duration of month je " day duration(s)".
(=>
(and
(equal
(MonthFn February ?YEAR)
?MONTH)
(instance ?YEAR LeapYear))
(duration
?MONTH
(MeasureFn 29 DayDuration)))
Jestliže month1 se rovná "únor of year" a month2 se rovná "březen of year", potom month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn February ?YEAR))
(equal
?MONTH2
(MonthFn March ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Jestliže month1 se rovná "březen of year" a month2 se rovná "duben of year", potom month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn March ?YEAR))
(equal
?MONTH2
(MonthFn April ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Jestliže month1 se rovná "duben of year" a month2 se rovná "květen of year", potom month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn April ?YEAR))
(equal
?MONTH2
(MonthFn May ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Jestliže month1 se rovná "květen of year" a month2 se rovná "červen of year", potom month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn May ?YEAR))
(equal
?MONTH2
(MonthFn June ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Jestliže month1 se rovná "červen of year" a month2 se rovná "červenec of year", potom month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn June ?YEAR))
(equal
?MONTH2
(MonthFn July ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Jestliže month1 se rovná "červenec of year" a month2 se rovná "srpen of year", potom month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn July ?YEAR))
(equal
?MONTH2
(MonthFn August ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Jestliže month1 se rovná "srpen of year" a month2 se rovná "září of year", potom month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn August ?YEAR))
(equal
?MONTH2
(MonthFn September ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Jestliže month1 se rovná "září of year" a month2 se rovná "říjen of year", potom month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn September ?YEAR))
(equal
?MONTH2
(MonthFn October ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Jestliže month1 se rovná "říjen of year" a month2 se rovná "listopad of year", potom month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn October ?YEAR))
(equal
?MONTH2
(MonthFn November ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Jestliže month1 se rovná "listopad of year" a month2 se rovná "prosinec of year", potom month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn November ?YEAR))
(equal
?MONTH2
(MonthFn December ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Jestliže month1 se rovná "prosinec of year1" a month2 se rovná "leden of year2" a year1 meets year2, potom month1 meets month2.
(=>
(and
(equal
?MONTH1
(MonthFn December ?YEAR1))
(equal
?MONTH2
(MonthFn January ?YEAR2))
(meetsTemporally ?YEAR1 ?YEAR2))
(meetsTemporally ?MONTH1 ?MONTH2))
- jestliže "decomposition of interval into ? interval-types" se rovná class,
- potom pro všechny time1,time2 platí: jestliže time1 je instancí třídy interval-type a time2 je instancí třídy class, potom existuje duration tak, že duration of time1 je duration a duration of time2 je 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))))))
- jestliže "decomposition of interval into ? interval-types" se rovná class,
- potom pro všechny time1,time2 platí: jestliže time1 je instancí třídy class a time2 je instancí třídy class a time1 se nerovná time2, potom time1 meets time2 nebo time2 meets time1 nebo time1 happens earlier than time2 nebo 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)))))
Jestliže "decomposition of interval into ? interval-types" se rovná class, potom existuje class time tak, že time starts interval.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(exists
(?TIME)
(and
(instance ?TIME ?CLASS)
(starts ?TIME ?INTERVAL))))
Jestliže "decomposition of interval into ? interval-types" se rovná class, potom existuje class time tak, že time finishes interval.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(exists
(?TIME)
(and
(instance ?TIME ?CLASS)
(finishes ?TIME ?INTERVAL))))
- jestliže "decomposition of interval into ? interval-types" se rovná class,
- potom pro všechny time1 platí: jestliže time1 je instancí třídy class a time1 doesn't finish interval, potom existuje class time2 tak, že 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))))))
- jestliže "decomposition of interval into ? interval-types" se rovná class,
- potom pro všechny time1 platí: jestliže time1 je instancí třídy class a time1 doesn't start interval, potom existuje class time2 tak, že 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))))))
- jestliže "decomposition of interval into ? interval-types" se rovná class,
- potom pro všechny time platí: jestliže time je instancí třídy okamžik a time je a part of interval, potom existuje class instance tak, že time je 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))))))
Jestliže year je instancí třídy rok, potom "cardinality fn(decomposition of year into ? měsícs)" se rovná .
(=>
(instance ?YEAR Year)
(equal
(CardinalityFn
(TemporalCompositionFn ?YEAR Month))
12))
Jestliže month je instancí třídy měsíc a duration of month je "number day duration(s)", potom "cardinality fn(decomposition of month into ? dens)" se rovná number.
(=>
(and
(instance ?MONTH Month)
(duration
?MONTH
(MeasureFn ?NUMBER DayDuration)))
(equal
(CardinalityFn
(TemporalCompositionFn ?MONTH Day))
?NUMBER))
Jestliže week je instancí třídy týren, potom "cardinality fn(decomposition of week into ? dens)" se rovná .
(=>
(instance ?WEEK Week)
(equal
(CardinalityFn
(TemporalCompositionFn ?WEEK Day))
7))
Jestliže day je instancí třídy den, potom "cardinality fn(decomposition of day into ? hodinas)" se rovná .
(=>
(instance ?DAY Day)
(equal
(CardinalityFn
(TemporalCompositionFn ?DAY Hour))
24))
Jestliže hour je instancí třídy hodina, potom "cardinality fn(decomposition of hour into ? minutas)" se rovná .
(=>
(instance ?HOUR Hour)
(equal
(CardinalityFn
(TemporalCompositionFn ?HOUR Minute))
60))
Jestliže minute je instancí třídy minuta, potom "cardinality fn(decomposition of minute into ? vteřinas)" se rovná .
(=>
(instance ?MINUTE Minute)
(equal
(CardinalityFn
(TemporalCompositionFn ?MINUTE Second))
60))
obj je instancí třídy spojitý objekt tehdy a jen tehdy pokud pro všechny part1,part2 platí: jestliže obj se rovná "mereological sum fn(part1,part2)", potom part1 je spojen s part2.
(<=>
(instance ?OBJ SelfConnectedObject)
(forall
(?PART1 ?PART2)
(=>
(equal
?OBJ
(MereologicalSumFn ?PART1 ?PART2))
(connected ?PART1 ?PART2))))
Jestliže obj1 je a členem coll a obj2 je a členem coll a obj1 se nerovná obj2, potom obj1 se nepřekrývá s obj2.
(=>
(and
(member ?OBJ1 ?COLL)
(member ?OBJ2 ?COLL)
(not
(equal ?OBJ1 ?OBJ2)))
(not
(overlapsSpatially ?OBJ1 ?OBJ2)))
Jestliže obj3 se rovná "mereological sum fn(obj1,obj2)", potom pro všechny part platí: part je částí obj3 tehdy a jen tehdy pokud part je částí obj1 nebo part je částí obj2.
(=>
(equal
?OBJ3
(MereologicalSumFn ?OBJ1 ?OBJ2))
(forall
(?PART)
(<=>
(part ?PART ?OBJ3)
(or
(part ?PART ?OBJ1)
(part ?PART ?OBJ2)))))
Jestliže obj3 se rovná "mereological product fn(obj1,obj2)", potom pro všechny part platí: part je částí obj3 tehdy a jen tehdy pokud part je částí obj1 a part je částí obj2.
(=>
(equal
?OBJ3
(MereologicalProductFn ?OBJ1 ?OBJ2))
(forall
(?PART)
(<=>
(part ?PART ?OBJ3)
(and
(part ?PART ?OBJ1)
(part ?PART ?OBJ2)))))
Jestliže obj3 se rovná "mereological difference fn(obj1,obj2)", potom pro všechny part platí: part je částí obj3 tehdy a jen tehdy pokud part je částí obj1 a part není částí obj2.
(=>
(equal
?OBJ3
(MereologicalDifferenceFn ?OBJ1 ?OBJ2))
(forall
(?PART)
(<=>
(part ?PART ?OBJ3)
(and
(part ?PART ?OBJ1)
(not
(part ?PART ?OBJ2))))))
Jestliže obj1 se rovná "principal host fn(hole)", potom pro všechny obj2 platí: obj2 se překrývá s obj1 tehdy a jen tehdy pokud existuje obj3 tak, že hole je díra v obj3 a obj2 se překrývá s obj3.
(=>
(equal
?OBJ1
(PrincipalHostFn ?HOLE))
(forall
(?OBJ2)
(<=>
(overlapsSpatially ?OBJ2 ?OBJ1)
(exists
(?OBJ3)
(and
(hole ?HOLE ?OBJ3)
(overlapsSpatially ?OBJ2 ?OBJ3))))))
Jestliže obj1 se rovná "skin fn(hole)", potom pro všechny obj2 platí: obj2 se překrývá s obj1 tehdy a jen tehdy pokud existuje obj3 tak, že obj3 je a minimální částí "principal host fn(hole)" a hole se dotýká obj3 a obj2 se překrývá s obj3.
(=>
(equal
?OBJ1
(SkinFn ?HOLE))
(forall
(?OBJ2)
(<=>
(overlapsSpatially ?OBJ2 ?OBJ1)
(exists
(?OBJ3)
(and
(superficialPart
?OBJ3
(PrincipalHostFn ?HOLE))
(meetsSpatially ?HOLE ?OBJ3)
(overlapsSpatially ?OBJ2 ?OBJ3))))))
Jestliže subproc je a subprocess of proc, potom "doba existence subproc" se rovná "doba existence proc" nebo "doba existence subproc" takes place during "doba existence proc".
(=>
(subProcess ?SUBPROC ?PROC)
(or
(equal
(WhenFn ?SUBPROC)
(WhenFn ?PROC))
(during
(WhenFn ?SUBPROC)
(WhenFn ?PROC))))
Jestliže rep je instancí třídy asexuální reprodukce a organism je výsledkem rep, potom neexistují parent1,parent2 tak, že parent1 je a parent of organism a parent2 je a parent of organism a parent1 se nerovná parent2.
(=>
(and
(instance ?REP AsexualReproduction)
(result ?REP ?ORGANISM))
(not
(exists
(?PARENT1 ?PARENT2)
(and
(parent ?ORGANISM ?PARENT1)
(parent ?ORGANISM ?PARENT2)
(not
(equal ?PARENT1 ?PARENT2))))))
Jestliže increase je instancí třídy zvyšování parametru a obj je účastníkem increase, potom existují unit,quant1,quant2 tak, že "obj unit(s)" se rovná quant1 právě před doba existence increase a "obj unit(s)" se rovná quant2 právě po doba existence increase a quant2 je větší než 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))))
Jestliže heat je instancí třídy zahřívání a obj je účastníkem heat, potom existují jednotka teploty unit,quant1,quant2 tak, že "obj unit(s)" se rovná quant1 právě před doba existence heat a "obj unit(s)" se rovná quant2 právě po doba existence heat a quant2 je větší než 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))))
Jestliže decrease je instancí třídy snižování parametru a obj je účastníkem decrease, potom existují unit,quant1,quant2 tak, že "obj unit(s)" se rovná quant1 právě před doba existence decrease a "obj unit(s)" se rovná quant2 právě po doba existence decrease a quant2 je menší než 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))))
Jestliže cool je instancí třídy ochlazování a obj je účastníkem cool, potom existují jednotka teploty unit,quant1,quant2 tak, že "obj unit(s)" se rovná quant1 právě před doba existence cool a "obj unit(s)" se rovná quant2 právě po doba existence cool a quant2 je menší než 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))))
Jestliže transfer je instancí třídy přeprava a agent je původcem transfer a patient je účastníkem transfer, potom agent se nerovná patient.
(=>
(and
(instance ?TRANSFER Transfer)
(agent ?TRANSFER ?AGENT)
(patient ?TRANSFER ?PATIENT))
(not
(equal ?AGENT ?PATIENT)))
Jestliže sub je instancí třídy záměna, potom existují uložení put,odstranění remove,obj1,obj2,place tak, že put je a subprocess of sub a remove je a subprocess of sub a obj1 je účastníkem remove a remove začíná v place a obj2 je účastníkem put a put končí v place a obj1 se nerovná 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)))))
Jestliže change je instancí třídy změna vlastnictví a obj je účastníkem change a agent1 posesses obj právě před doba existence change a agent2 posesses obj právě po doba existence change, potom agent1 se nerovná 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)))
Jestliže trans je instancí třídy transakce, potom existují agent1,agent2,dávání give1,dávání give2,obj1,obj2 tak, že give1 je a subprocess of trans a give2 je a subprocess of trans a agent1 je původcem give1 a agent2 je původcem give2 a obj1 je účastníkem give1 a obj2 je účastníkem give2 a give1 končí v agent2 a give2 končí v agent1 a agent1 se nerovná agent2 a obj1 se nerovná 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)))))
Jestliže count je instancí třídy sčítání a agent je původcem count a entity je účastníkem count, potom existuje number tak, že agent knows ""cardinality fn(entity)" se rovná number".
(=>
(and
(instance ?COUNT Counting)
(agent ?COUNT ?AGENT)
(patient ?COUNT ?ENTITY))
(exists
(?NUMBER)
(knows
?AGENT
(equal
(CardinalityFn ?ENTITY)
?NUMBER))))
compound je instancí třídy sloučenina tehdy a jen tehdy pokud existují elementární látka element1,elementární látka element2,chemická syntéza process tak, že element1 se nerovná element2 a element1 je nástrojem pro process a element2 je nástrojem pro process a compound je výsledkem 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))))
Jestliže interaction je instancí třídy sociální interakce, potom existují agent1,agent2 tak, že agent1 je původcem interaction a agent2 je původcem interaction a agent1 se nerovná agent2.
(=>
(instance ?INTERACTION SocialInteraction)
(exists
(?AGENT1 ?AGENT2)
(and
(agent ?INTERACTION ?AGENT1)
(agent ?INTERACTION ?AGENT2)
(not
(equal ?AGENT1 ?AGENT2)))))
Jestliže disseminate je instancí třídy šíření, potom existují myslící agent agent1,myslící agent agent2 tak, že disseminate končí v agent1 a disseminate končí v agent2 a agent1 se nerovná agent2.
(=>
(instance ?DISSEMINATE Disseminating)
(exists
(?AGENT1 ?AGENT2)
(and
(destination ?DISSEMINATE ?AGENT1)
(instance ?AGENT1 CognitiveAgent)
(destination ?DISSEMINATE ?AGENT2)
(instance ?AGENT2 CognitiveAgent)
(not
(equal ?AGENT1 ?AGENT2)))))
Jestliže contest je instancí třídy soutěž, potom existují agent1,agent2,purp1,purp2 tak, že agent1 je původcem contest a agent2 je původcem contest a contest has purpose purp1 for agent1 a contest has purpose purp2 for agent2 a agent1 se nerovná agent2 a purp1 se nerovná 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)))))
Jestliže process je instancí třídy změna skupenství a obj je účastníkem process, potom existují part,skupenství state1,skupenství state2 tak, že part je částí obj a state1 se nerovná state2 a state1 je atributem part právě před doba existence process a state2 je atributem part právě po doba existence 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)))))
Jestliže area je instancí třídy vodní plocha, potom existují bed,hole,voda water tak, že "principal host fn(hole)" se rovná bed a water přesně zaplňuje hole a "mereological sum fn(bed,water)" se rovná area.
(=>
(instance ?AREA WaterArea)
(exists
(?BED ?HOLE ?WATER)
(and
(equal
(PrincipalHostFn ?HOLE)
?BED)
(instance ?WATER Water)
(properlyFills ?WATER ?HOLE)
(equal
(MereologicalSumFn ?BED ?WATER)
?AREA))))
"cardinality fn(kontinent)" se rovná .
(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))))))
Jestliže junct je instancí třídy tělní kloub, potom existují část těla struct1,část těla struct2 tak, že junct je spojen s struct1 a junct je spojen s struct2 a struct1 se nerovná struct2.
(=>
(instance ?JUNCT BodyJunction)
(exists
(?STRUCT1 ?STRUCT2)
(and
(connected ?JUNCT ?STRUCT1)
(connected ?JUNCT ?STRUCT2)
(instance ?STRUCT1 BodyPart)
(instance ?STRUCT2 BodyPart)
(not
(equal ?STRUCT1 ?STRUCT2)))))
Jestliže morph je instancí třídy morfém, potom neexistuje morfém othermorph tak, že othermorph je částí morph a othermorph se nerovná morph.
(=>
(instance ?MORPH Morpheme)
(not
(exists
(?OTHERMORPH)
(and
(instance ?OTHERMORPH Morpheme)
(part ?OTHERMORPH ?MORPH)
(not
(equal ?OTHERMORPH ?MORPH))))))
Jestliže phrase je instancí třídy fráze, potom existují slovo part1,slovo part2 tak, že part1 je částí phrase a part2 je částí phrase a part1 se nerovná part2.
(=>
(instance ?PHRASE Phrase)
(exists
(?PART1 ?PART2)
(and
(part ?PART1 ?PHRASE)
(part ?PART2 ?PHRASE)
(instance ?PART1 Word)
(instance ?PART2 Word)
(not
(equal ?PART1 ?PART2)))))
Jestliže "edition fn(text,int1)" se rovná edition1 a "edition fn(text,int2)" se rovná edition2 a int2 je větší než int1 a pub1 je instancí třídy publikování a pub2 je instancí třídy publikování a edition1 je účastníkem pub1 a edition2 je účastníkem pub2 a date of pub1 je date1 a date of pub2 je date2, potom "the end of date1" happens 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)))
Jestliže "edition fn(text1,number)" se rovná text2, potom subsumes content class(text1,text2) platí.
(=>
(equal
(EditionFn ?TEXT1 ?NUMBER)
?TEXT2)
(subsumesContentClass ?TEXT1 ?TEXT2))
Jestliže text je podtřídou periodikum a "series volume fn(text,int1)" se rovná volume1 a "series volume fn(text,int2)" se rovná volume2 a int2 je větší než int1 a pub1 je instancí třídy publikování a pub2 je instancí třídy publikování a volume1 je účastníkem pub1 a volume2 je účastníkem pub2 a date of pub1 je date1 a date of pub2 je date2, potom "the end of date1" happens 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)))
Jestliže "series volume fn(series,number)" se rovná volume, potom subsumes content class(series,volume) platí.
(=>
(equal
(SeriesVolumeFn ?SERIES ?NUMBER)
?VOLUME)
(subsumesContentClass ?SERIES ?VOLUME))
Jestliže "periodical issue fn(periodical,number)" se rovná issue, potom subsumes content class(periodical,issue) platí.
(=>
(equal
(PeriodicalIssueFn ?PERIODICAL ?NUMBER)
?ISSUE)
(subsumesContentClass ?PERIODICAL ?ISSUE))
Jestliže series je instancí třídy řada, potom existují kniha book1,kniha book2 tak, že subsumes content instance(series,book1) platí a subsumes content instance(series,book2) platí a book1 se nerovná book2.
(=>
(instance ?SERIES Series)
(exists
(?BOOK1 ?BOOK2)
(and
(instance ?BOOK1 Book)
(instance ?BOOK2 Book)
(subsumesContentInstance ?SERIES ?BOOK1)
(subsumesContentInstance ?SERIES ?BOOK2)
(not
(equal ?BOOK1 ?BOOK2)))))
Jestliže mole je instancí třídy molekula, potom existují atom atom1,atom atom2 tak, že atom1 je částí mole a atom2 je částí mole a atom1 se nerovná atom2.
(=>
(instance ?MOLE Molecule)
(exists
(?ATOM1 ?ATOM2)
(and
(instance ?ATOM1 Atom)
(instance ?ATOM2 Atom)
(part ?ATOM1 ?MOLE)
(part ?ATOM2 ?MOLE)
(not
(equal ?ATOM1 ?ATOM2)))))
- jestliže artifact je instancí třídy nemovitost,
- potom existuje place tak, že pro všechny time platí: jestliže time happen?{s} before or at "the end of doba existence artifact" a "the beginning of doba existence artifact" happen?{s} before or at time, potom "místo kde artifact byl v čase time" se rovná place
.
(=>
(instance ?ARTIFACT StationaryArtifact)
(exists
(?PLACE)
(forall
(?TIME)
(=>
(and
(beforeOrEqual
?TIME
(EndFn
(WhenFn ?ARTIFACT)))
(beforeOrEqual
(BeginFn
(WhenFn ?ARTIFACT))
?TIME))
(equal
(WhereFn ?ARTIFACT ?TIME)
?PLACE)))))
- jestliže group je instancí třídy věková skupina,
- potom pro všechny memb1,memb2,age1,age2 platí: jestliže memb1 je a členem group a memb2 je a členem group a age(memb1,age1) platí a age(memb2,age2) platí, potom age1 se rovná 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))))
Jestliže "organization fn(unit)" se rovná org a attr je instancí třídy objektivní atribut, potom attr je atributem unit tehdy a jen tehdy pokud attr je atributem org.
(=>
(and
(equal
(OrganizationFn ?UNIT)
?ORG)
(instance ?ATTR NormativeAttribute))
(<=>
(attribute ?UNIT ?ATTR)
(attribute ?ORG ?ATTR)))
Jestliže obj1 je attr1 vzhledem k obj2 a contrary attribute() platí a attr1 je a member of "()" a attr2 je a member of "()" a attr1 se nerovná attr2, potom obj1 není attr2 vzhledem k 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)))
(=>
(holdsDuring
?TIME
(direction ?PROC ?ATTR1))
(forall
(?ATTR2)
(=>
(holdsDuring
?TIME
(direction ?PROC ?ATTR2))
(equal ?ATTR2 ?ATTR1))))
- jestliže faces(proc,attr1) platí během time,
- potom pro všechny attr2 platí: jestliže faces(proc,attr2) platí během time, potom attr2 se rovná attr1
.
(=>
(holdsDuring
?TIME
(faces ?PROC ?ATTR1))
(forall
(?ATTR2)
(=>
(holdsDuring
?TIME
(faces ?PROC ?ATTR2))
(equal ?ATTR2 ?ATTR1))))
Jestliže obj1 je attr1 vzhledem k obj2 a attr1 je instancí třídy směrový atribut a attr2 je instancí třídy směrový atribut a attr1 se nerovná attr2, potom obj1 není attr2 vzhledem k obj2.
(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(instance ?ATTR1 DirectionalAttribute)
(instance ?ATTR2 DirectionalAttribute)
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))
Jestliže "relative time fn(time1,pacific time zone)" se rovná time2, potom time2 se rovná "(time1+)".
(=>
(equal
(RelativeTimeFn ?TIME1 PacificTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 8)))
Jestliže "relative time fn(time1,mountain time zone)" se rovná time2, potom time2 se rovná "(time1+)".
(=>
(equal
(RelativeTimeFn ?TIME1 MountainTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 7)))
Jestliže "relative time fn(time1,central time zone)" se rovná time2, potom time2 se rovná "(time1+)".
(=>
(equal
(RelativeTimeFn ?TIME1 CentralTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 6)))
Jestliže "relative time fn(time1,eastern time zone)" se rovná time2, potom time2 se rovná "(time1+)".
(=>
(equal
(RelativeTimeFn ?TIME1 EasternTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 5)))
Jestliže polychromatic je atributem obj, potom existují part1,part2,atribut barvy color1,atribut barvy color2 tak, že part1 je a minimální částí obj a part2 je a minimální částí obj a color1 je atributem part1 a color2 je atributem part2 a color1 se nerovná 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)))))
Jestliže class1 je instancí třídy množina nebo třída a class2 je instancí třídy množina nebo třída, potom "relative complement fn(class1,class2)" se rovná "intersection fn(class1,complement fn(class2))".
(=>
(and
(instance ?CLASS1 SetOrClass)
(instance ?CLASS2 SetOrClass))
(equal
(RelativeComplementFn ?CLASS1 ?CLASS2)
(IntersectionFn
?CLASS1
(ComplementFn ?CLASS2))))
