%1 ist gleich %2 %n{nicht} (equal)
(equal entity1 entity2) is true just in case
entity1 is identical with entity2.
Ontology
SUMO / STRUCTURAL-ONTOLOGYClass(es)
Coordinate term(s)
AdditionFn
DivisionFn
ExponentiationFn
MaximumFn
MinumumFn
MultiplikationFn
ReziprokerWert
RestFn
RundFn
SubtraktionFn
arctusGewicht
schreibt
vorOderGleichzeitig
verursacht
causes subclass
bürger
aufgeschlossen
angeschlossen
enthältInformationen
zusammenGeschiecht
kopie
datum
verringertWahrscheinlichkeit
entwicklungsForm
disjunkt
istDistributiv
dokumentation
&%dauer von %1 ist %2 %n{nicht}
früh
herausgeber
element
beschäftigt
äquivalenzrelationMit
gleichwertigeInhaltskategorie
gleichwertigeInhaltsfall
nutztAus
inSpracheAusgedrückt
stelltGegenüber
verwandt
beendet
frequenz
graphenTeil
grösserAls
grösserAlsOderGleich
hatZweck
hatFähigkeit
hältWährend
hatVerpflichtung
hatRecht
loch
identitätsElement
inListe
imBereichInteresses
vergrössertWahrscheinlichkeit
Unabhänigkeitswahrscheinlichkeit
wohnt
hemmt
ausgangsList
fall
umkehrFunktion
irreflexivAur
grösser
kleinerAls
kleinerAlsOderGleich
material
mass
schliesstZeitlichAn
modalesAttribute
decktSichZeitlich
elternteil
teilweiseEinrichtung
befindetSichTeils
pfadLänge
besitzt
vorbedingung
verhindert
eigenschaft
veröffentlicht
&%bildbereich von %1 ist ein fall von %2 {nicht}
bildbereichTeilkategorie
beziehtSichAuf
reflexivAuf
verwandtesInnenkonzept
geschwister
kleiner
beginnt
teilAttribut
teilsammlung
teilGraph
teilliste
subProzess
%1 ist eine &%teilangelegenheit von %2 %n{nicht}
teilkategorie
teilrelation
fasstInhaltsKategorieZusammen
fasstInhaltsFallZusammen
nachfolgerAttribut
nachfolgerAttributSchliessung
zeitlichesTeil
zeit
gesamteinrichtung
trichotomizierungAuf
verwendet
valenz
version
Type restrictions
equal(Wesen, Wesen)
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)
Wenn class1 ist eine direkte teilkategorie von class2, dann es gibt kein class2 class3 der class1 ist eine teilkategorie von class3 und class2 ist gleich class3 nicht und class1 ist gleich class3 nicht.
(=>
(immediateSubclass ?CLASS1 ?CLASS2)
(not
(exists
(?CLASS3)
(and
(subclass ?CLASS3 ?CLASS2)
(subclass ?CLASS1 ?CLASS3)
(not
(equal ?CLASS2 ?CLASS3))
(not
(equal ?CLASS1 ?CLASS3))))))
Wenn thing1 ist gleich thing2 , dann für jeden attr gilt: thing1 hat ein attribut attr nur wenn thing2 hat ein attribut attr .
(=>
(equal ?THING1 ?THING2)
(forall
(?ATTR)
(<=>
(property ?THING1 ?ATTR)
(property ?THING2 ?ATTR))))
Wenn attr1 ist gleich attr2 , dann für jeden thing gilt: thing hat ein attribut attr1 nur wenn thing hat ein attribut attr2 .
(=>
(equal ?ATTR1 ?ATTR2)
(forall
(?THING)
(<=>
(property ?THING ?ATTR1)
(property ?THING ?ATTR2))))
Wenn thing1 ist gleich thing2 , dann für jeden class gilt: thing1 ist ein fall von class nur wenn thing2 ist ein fall von class .
(=>
(equal ?THING1 ?THING2)
(forall
(?CLASS)
(<=>
(instance ?THING1 ?CLASS)
(instance ?THING2 ?CLASS))))
Wenn class1 ist gleich class2 , dann für jeden thing gilt: thing ist ein fall von class1 nur wenn thing ist ein fall von class2 .
(=>
(equal ?CLASS1 ?CLASS2)
(forall
(?THING)
(<=>
(instance ?THING ?CLASS1)
(instance ?THING ?CLASS2))))
Wenn rel1 ist gleich rel2 , dann für jeden gilt: rel1() gilt nur wenn rel2() gilt .
(=>
(equal ?REL1 ?REL2)
(forall
(@ROW)
(<=>
(holds ?REL1 @ROW)
(holds ?REL2 @ROW))))
- wenn obj1 ist gleich obj2 ,
- dann wenn obj1 ist gleich "numberte mitglied von "()"" und obj2 ist gleich "numberte mitglied von "()"" und "()" ist gleich "()" , dann () gilt nur wenn () gilt
.
(=>
(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))))
- wenn list1 ist gleich list2 ,
- dann wenn list1 ist gleich "()" und list2 ist gleich "()" , dann für jeden number gilt: "numberte mitglied von "()"" ist gleich "numberte mitglied von "()""
.
(=>
(equal ?LIST1 ?LIST2)
(=>
(and
(equal
?LIST1
(ListFn @ROW1))
(equal
?LIST2
(ListFn @ROW2)))
(forall
(?NUMBER)
(equal
(ListOrderFn
(ListFn @ROW1)
?NUMBER)
(ListOrderFn
(ListFn @ROW2)
?NUMBER)))))
Wenn bildbereich von function ist ein fall von class {nicht} und "function()" ist gleich value , dann value ist ein fall von class .
(=>
(and
(range ?FUNCTION ?CLASS)
(equal
(AssignmentFn ?FUNCTION @ROW)
?VALUE))
(instance ?VALUE ?CLASS))
Wenn die werte die function zurückgibt sind teilkategorien von class und "function()" ist gleich value , dann value ist eine teilkategorie von class.
(=>
(and
(rangeSubclass ?FUNCTION ?CLASS)
(equal
(AssignmentFn ?FUNCTION @ROW)
?VALUE))
(subclass ?VALUE ?CLASS))
Wenn und ? werden disjunkt und rel1 ist ein Mitglied von "()" und rel2 ist ein Mitglied von "()" und rel1 ist gleich rel2 nicht und rel1() gilt , dann rel2() gilt nicht.
(=>
(and
(disjointRelation @ROW1)
(inList
?REL1
(ListFn @ROW1))
(inList
?REL2
(ListFn @ROW1))
(not
(equal ?REL1 ?REL2))
(holds ?REL1 @ROW2))
(not
(holds ?REL2 @ROW2)))
- wenn wird ? entgegengesetzet ,
- dann für jeden attr1,attr2 gilt:
- wenn attr1 ist gleich "number1te mitglied von "()"" und attr2 ist gleich "number2te mitglied von "()"" und number1 ist gleich number2 nicht,
- dann wenn obj hat ein attribut attr1 , dann obj hat ein attribut attr2 nicht
.
(=>
(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))))))
- wenn exhaustive attribute(class,) gilt,
- dann für jeden obj gilt: wenn attr1 ist ein fall von class , dann es gibt ein attr2 der attr2 ist ein Mitglied von "()" und attr1 ist gleich attr2
.
(=>
(exhaustiveAttribute ?CLASS @ROW)
(forall
(?OBJ)
(=>
(instance ?ATTR1 ?CLASS)
(exists
(?ATTR2)
(and
(inList
?ATTR2
(ListFn @ROW))
(equal ?ATTR1 ?ATTR2))))))
Wenn rel(,inst) gilt und rel ist ein fall von Funktion , dann "rel()" ist gleich inst .
(=>
(and
(holds ?REL @ROW ?INST)
(instance ?REL Function))
(equal
(AssignmentFn ?REL @ROW)
?INST))
- wenn atom ist ein fall von Atom ,
- dann für jeden nucleus1,nucleus2 gilt: wenn nucleus1 ist ein bestandteil von atom und nucleus2 ist ein bestandteil von atom und nucleus1 ist ein fall von Atomkern und nucleus2 ist ein fall von Atomkern , dann nucleus1 ist gleich nucleus2
.
(=>
(instance ?ATOM Atom)
(forall
(?NUCLEUS1 ?NUCLEUS2)
(=>
(and
(component ?NUCLEUS1 ?ATOM)
(component ?NUCLEUS2 ?ATOM)
(instance ?NUCLEUS1 AtomicNucleus)
(instance ?NUCLEUS2 AtomicNucleus))
(equal ?NUCLEUS1 ?NUCLEUS2))))
Wenn mixture ist ein fall von Mischung , dann es gibt ein reine Substanz pure1,reine Substanz pure2 der pure1 ist gleich pure2 nicht und pure1 ist ein stück von mixture und pure2 ist ein stück von mixture .
(=>
(instance ?MIXTURE Mixture)
(exists
(?PURE1 ?PURE2)
(and
(subclass ?PURE1 PureSubstance)
(subclass ?PURE2 PureSubstance)
(not
(equal ?PURE1 ?PURE2))
(piece ?PURE1 ?MIXTURE)
(piece ?PURE2 ?MIXTURE))))
Wenn obj ist ein fall von korpuskularer Gegenstand , dann es gibt ein Substanz substance1,Substanz substance2 der substance1 ist von obj gebildet und substance2 ist von obj gebildet und substance1 ist gleich substance2 nicht.
(=>
(instance ?OBJ CorpuscularObject)
(exists
(?SUBSTANCE1 ?SUBSTANCE2)
(and
(subclass ?SUBSTANCE1 Substance)
(subclass ?SUBSTANCE2 Substance)
(material ?SUBSTANCE1 ?OBJ)
(material ?SUBSTANCE2 ?OBJ)
(not
(equal ?SUBSTANCE1 ?SUBSTANCE2)))))
Wenn process ist ein fall von Doppelgegenstandprozess , dann es gibt ein obj1,obj2 der obj1 ist ein patient von process und obj2 ist ein patient von process und obj1 ist gleich obj2 nicht.
(=>
(instance ?PROCESS DualObjectProcess)
(exists
(?OBJ1 ?OBJ2)
(and
(patient ?PROCESS ?OBJ1)
(patient ?PROCESS ?OBJ2)
(not
(equal ?OBJ1 ?OBJ2)))))
"die beschreibung von class" ist gleich attr nur wenn für jeden inst gilt: inst ist ein fall von class nur wenn inst hat ein attribut attr .
(<=>
(equal
(AbstractionFn ?CLASS)
?ATTR)
(forall
(?INST)
(<=>
(instance ?INST ?CLASS)
(property ?INST ?ATTR))))
"die kategorie, die attribute entspricht" ist gleich class nur wenn "die beschreibung von class" ist gleich attribute .
(<=>
(equal
(ExtensionFn ?ATTRIBUTE)
?CLASS)
(equal
(AbstractionFn ?CLASS)
?ATTRIBUTE))
number1 ist kleinerAlsOderGleich number2 nur wenn number1 ist gleich number2 oder number1 ist kleinerAls number2 .
(<=>
(lessThanOrEqualTo ?NUMBER1 ?NUMBER2)
(or
(equal ?NUMBER1 ?NUMBER2)
(lessThan ?NUMBER1 ?NUMBER2)))
number1 ist grösserAlsOderGleich number2 nur wenn number1 ist gleich number2 oder number1 ist grösserAls number2 .
(<=>
(greaterThanOrEqualTo ?NUMBER1 ?NUMBER2)
(or
(equal ?NUMBER1 ?NUMBER2)
(greaterThan ?NUMBER1 ?NUMBER2)))
Wenn number ist ein fall von imaginäre Zahl , dann es gibt ein reelle Zahl real der number ist gleich "real*"die quadratwurzel von "" .
(=>
(instance ?NUMBER ImaginaryNumber)
(exists
(?REAL)
(and
(instance ?REAL RealNumber)
(equal
?NUMBER
(MultiplicationFn
?REAL
(SquareRootFn -1))))))
Wenn number ist ein fall von Komplexzahl , dann es gibt ein reelle Zahl real1,reelle Zahl real2 der number ist gleich "(real1+"real2*"die quadratwurzel von "")" .
(=>
(instance ?NUMBER ComplexNumber)
(exists
(?REAL1 ?REAL2)
(and
(instance ?REAL1 RealNumber)
(instance ?REAL2 RealNumber)
(equal
?NUMBER
(AdditionFn
?REAL1
(MultiplicationFn
?REAL2
(SquareRootFn -1)))))))
rel ist ein fall von einwertige Relation nur wenn für jeden ,item1,item2 gilt: wenn rel(,item1) gilt und rel(,item2) gilt , dann item1 ist gleich item2 .
(<=>
(instance ?REL SingleValuedRelation)
(forall
(@ROW ?ITEM1 ?ITEM2)
(=>
(and
(holds ?REL @ROW ?ITEM1)
(holds ?REL @ROW ?ITEM2))
(equal ?ITEM1 ?ITEM2))))
rel ist ein fall von totalwertige Relation nur wenn es gibt ein valence der rel ist ein fall von Relation und rel hat valence argument(e) und - wenn für jeden number,element,class gilt: wenn number ist kleinerAls valence und die Zahl number Argument von rel ist ein fall von class und element ist gleich "numberte mitglied von "()"" , dann element ist ein fall von class ,
- dann es gibt ein item der rel(,item) gilt
.
(<=>
(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))))))
- wenn rel ist ein fall von antisymmetrische Relation ,
- dann für jeden inst1,inst2 gilt: wenn rel(inst1,inst2) gilt und rel(inst2,inst1) gilt , dann inst1 ist gleich inst2
.
(=>
(instance ?REL AntisymmetricRelation)
(forall
(?INST1 ?INST2)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST1))
(equal ?INST1 ?INST2))))
Wenn rel ist ein fall von trichotomizierende Relation , dann für jeden inst1,inst2 gilt: rel(inst1,inst2) gilt oder inst1 ist gleich inst2 oder rel(inst2,inst1) gilt .
(=>
(instance ?REL TrichotomizingRelation)
(forall
(?INST1 ?INST2)
(or
(holds ?REL ?INST1 ?INST2)
(equal ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST1))))
Wenn formula1 vergrössert die Wahrscheinlichkeit von formula2 und "die wahrscheinlichkeit von formula2" ist gleich number1 und Gesetzt den Fall, dass formula2 gilt, ist die wahrscheinlichkeit von formula1 number2, dann number2 ist grösserAls number1 .
(=>
(and
(increasesLikelihood ?FORMULA1 ?FORMULA2)
(equal
(ProbabilityFn ?FORMULA2)
?NUMBER1)
(conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
(greaterThan ?NUMBER2 ?NUMBER1))
Wenn formula1 verringert die Wahrscheinlichkeit von formula2 und "die wahrscheinlichkeit von formula2" ist gleich number1 und Gesetzt den Fall, dass formula2 gilt, ist die wahrscheinlichkeit von formula1 number2, dann number2 ist kleinerAls number1 .
(=>
(and
(decreasesLikelihood ?FORMULA1 ?FORMULA2)
(equal
(ProbabilityFn ?FORMULA2)
?NUMBER1)
(conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
(lessThan ?NUMBER2 ?NUMBER1))
Wenn Die wahrscheinlichkeit von formula1 und formula2 ist unabhänig und "die wahrscheinlichkeit von formula2" ist gleich number1 und Gesetzt den Fall, dass formula2 gilt, ist die wahrscheinlichkeit von formula1 number2, dann number2 ist gleich number1 .
(=>
(and
(independentProbability ?FORMULA1 ?FORMULA2)
(equal
(ProbabilityFn ?FORMULA2)
?NUMBER1)
(conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
(equal ?NUMBER2 ?NUMBER1))
- wenn list ist ein fall von Liste ,
- dann es gibt ein number1 der es gibt ein item1 der "number1te mitglied von list" ist gleich item1 nicht und für jeden number2 gilt: wenn number2 ist ein fall von positive Ganzzahl und number2 ist kleinerAls number1 , dann es gibt ein item2 der "number2te mitglied von list" ist gleich 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 ist ein fall von einzigartige Liste nur wenn für jeden number1,number2 gilt: wenn "number1te mitglied von list" ist gleich "number2te mitglied von list" , dann number1 ist gleich number2 .
(<=>
(instance ?LIST UniqueList)
(forall
(?NUMBER1 ?NUMBER2)
(=>
(equal
(ListOrderFn ?LIST ?NUMBER1)
(ListOrderFn ?LIST ?NUMBER2))
(equal ?NUMBER1 ?NUMBER2))))
list ist gleich null list nur wenn es gibt kein item der item ist ein Mitglied von list.
(<=>
(equal ?LIST NullList)
(not
(exists
(?ITEM)
(inList ?ITEM ?LIST))))
- wenn class wird zusammenhanglos auf disjunkt,
- dann für jeden item1,item2 gilt: wenn item1 ist ein Mitglied von "()" und item2 ist ein Mitglied von "()" und item1 ist gleich item2 nicht, dann item1 ist dijunkt von item2
.
(=>
(disjointDecomposition ?CLASS @ROW)
(forall
(?ITEM1 ?ITEM2)
(=>
(and
(inList
?ITEM1
(ListFn @ROW))
(inList
?ITEM2
(ListFn @ROW))
(not
(equal ?ITEM1 ?ITEM2)))
(disjoint ?ITEM1 ?ITEM2))))
Wenn list1 ist ein fall von Liste und list2 ist ein fall von Liste und für jeden number gilt: "numberte mitglied von list1" ist gleich "numberte mitglied von list2" , dann list1 ist gleich list2 .
(=>
(and
(instance ?LIST1 List)
(instance ?LIST2 List)
(forall
(?NUMBER)
(equal
(ListOrderFn ?LIST1 ?NUMBER)
(ListOrderFn ?LIST2 ?NUMBER))))
(equal ?LIST1 ?LIST2))
Wenn "Länge von list" ist gleich number1 , dann für jeden number2 gilt: es gibt ein item der "number2te mitglied von list" ist gleich item nur wenn number2 ist kleinerAlsOderGleich number1 .
(=>
(equal
(ListLengthFn ?LIST)
?NUMBER1)
(forall
(?NUMBER2)
(<=>
(exists
(?ITEM)
(equal
(ListOrderFn ?LIST ?NUMBER2)
?ITEM))
(lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))
"Länge von "(,item)"" ist gleich "("Länge von "()""+1)" .
(equal
(ListLengthFn
(ListFn @ROW ?ITEM))
(SuccessorFn
(ListLengthFn
(ListFn @ROW))))
""Länge von "(,item)""te mitglied von "(,item)"" ist gleich item .
(equal
(ListOrderFn
(ListFn @ROW ?ITEM)
(ListLengthFn
(ListFn @ROW ?ITEM)))
?ITEM)
- wenn rel hat number argument(e),
- dann für jeden gilt: wenn rel() gilt , dann "Länge von "()"" ist gleich number
.
(=>
(valence ?REL ?NUMBER)
(forall
(@ROW)
(=>
(holds ?REL @ROW)
(equal
(ListLengthFn
(ListFn @ROW))
?NUMBER))))
Wenn "Länge von list1" ist gleich number , dann es gibt ein list2 der list1 beginnt list2 und "(number+1)" ist gleich "Länge von list2" und ""(number+1)"te mitglied von list2" ist gleich item .
(=>
(equal
(ListLengthFn ?LIST1)
?NUMBER)
(exists
(?LIST2)
(and
(initialList ?LIST1 ?LIST2)
(equal
(SuccessorFn ?NUMBER)
(ListLengthFn ?LIST2))
(equal
(ListOrderFn
?LIST2
(SuccessorFn ?NUMBER))
?ITEM))))
list3 ist gleich "die Liste bestanden aus list1 und list2" nur wenn für jeden number1,number2 gilt: wenn number1 ist kleinerAlsOderGleich "Länge von list1" und number2 ist kleinerAlsOderGleich "Länge von list2" und number1 ist ein fall von positive Ganzzahl und number2 ist ein fall von positive Ganzzahl , dann "number1te mitglied von list3" ist gleich "number1te mitglied von list1" und ""("Länge von list1"+number2)"te mitglied von list3" ist gleich "number2te mitglied von 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 ist ein Mitglied von list nur wenn es gibt ein number der "numberte mitglied von list" ist gleich item .
(<=>
(inList ?ITEM ?LIST)
(exists
(?NUMBER)
(equal
(ListOrderFn ?LIST ?NUMBER)
?ITEM)))
- wenn list1 ist eine teilliste von list2 ,
- dann es gibt ein number3 der für jeden item gilt: wenn item ist ein Mitglied von list1, dann es gibt ein number1,number2 der "number1te mitglied von list1" ist gleich item und "number2te mitglied von list2" ist gleich item und number2 ist gleich "(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))))))))
- wenn list1 beginnt list2 ,
- dann für jeden number1,number2 gilt: wenn "Länge von list1" ist gleich number1 und number2 ist kleinerAlsOderGleich number1 , dann "number2te mitglied von list1" ist gleich "number2te mitglied von list2"
.
(=>
(initialList ?LIST1 ?LIST2)
(forall
(?NUMBER1 ?NUMBER2)
(=>
(and
(equal
(ListLengthFn ?LIST1)
?NUMBER1)
(lessThanOrEqualTo ?NUMBER2 ?NUMBER1))
(equal
(ListOrderFn ?LIST1 ?NUMBER2)
(ListOrderFn ?LIST2 ?NUMBER2)))))
- wenn fun ist ein fall von eineindeutige Function ,
- dann für jeden arg1,arg2 gilt: wenn die Zahl Argument von fun ist ein fall von class und arg1 ist ein fall von class und arg2 ist ein fall von class und arg1 ist gleich arg2 nicht, dann "fun(arg1)" ist gleich "fun(arg2)" nicht
.
(=>
(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))))))
- wenn function ist ein fall von associative Funktion ,
- dann für jeden inst1,inst2,inst3 gilt: wenn die Zahl Argument von function ist ein fall von class und inst1 ist ein fall von class und inst2 ist ein fall von class und inst3 ist ein fall von class , dann "function(inst1,"function(inst2,inst3)")" ist gleich "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)))))
- wenn function ist ein fall von commutative Funktion ,
- dann für jeden inst1,inst2 gilt: wenn die Zahl Argument von function ist ein fall von class und inst1 ist ein fall von class und inst2 ist ein fall von class , dann "function(inst1,inst2)" ist gleich "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)))))
- wenn relation ist eine trichotomizierung auf class ,
- dann für jeden inst1,inst2 gilt: wenn inst1 ist ein fall von class und inst2 ist ein fall von class , dann relation(inst1,inst2) gilt oder relation(inst2,inst1) gilt oder inst1 ist gleich 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)))))
- wenn function1 ist distributiv über function2,
- dann für jeden inst1,inst2,inst3 gilt: wenn die Zahl Argument von function1 ist ein fall von class1 und inst1 ist ein fall von class1 und inst2 ist ein fall von class1 und inst3 ist ein fall von class1 und die Zahl Argument von function2 ist ein fall von class2 und inst1 ist ein fall von class2 und inst2 ist ein fall von class2 und inst3 ist ein fall von class2 , dann "function1(inst1,"function2(inst2,inst3)")" ist gleich "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))))))
Wenn obj liegtGenau in region , dann es gibt kein otherobj der otherobj liegtGenau in region und otherobj ist gleich obj nicht.
(=>
(exactlyLocated ?OBJ ?REGION)
(not
(exists
(?OTHEROBJ)
(and
(exactlyLocated ?OTHEROBJ ?REGION)
(not
(equal ?OTHEROBJ ?OBJ))))))
"die Stelle wo thing an time war" ist gleich region nur wenn "thing liegtGenau in region " hält während time .
(<=>
(equal
(WhereFn ?THING ?TIME)
?REGION)
(holdsDuring
?TIME
(exactlyLocated ?THING ?REGION)))
Wenn time ist ein fall von Zeitposition und "agent1 besitzt obj " hält während time und "agent2 besitzt obj " hält während time , dann agent1 ist gleich agent2 .
(=>
(and
(instance ?TIME TimePosition)
(holdsDuring
?TIME
(possesses ?AGENT1 ?OBJ))
(holdsDuring
?TIME
(possesses ?AGENT2 ?OBJ)))
(equal ?AGENT1 ?AGENT2))
"(number+1)" ist gleich "(number+)" .
(equal
(SuccessorFn ?NUMBER)
(AdditionFn ?NUMBER 1))
"(number+2)" ist gleich "(number-)" .
(equal
(PredecessorFn ?NUMBER)
(SubtractionFn ?NUMBER 1))
Wenn number ist ein fall von rationale Zahl , dann es gibt ein Ganzzahl int1,Ganzzahl int2 der number ist gleich "int1/int2" .
(=>
(instance ?NUMBER RationalNumber)
(exists
(?INT1 ?INT2)
(and
(instance ?INT1 Integer)
(instance ?INT2 Integer)
(equal
?NUMBER
(DivisionFn ?INT1 ?INT2)))))
"der absolutebetrag von number1" ist gleich number2 und number1 ist ein fall von reelle Zahl und number2 ist ein fall von reelle Zahl nur wenn
(<=>
(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)))))
Wenn "die oberstegrenze von number" ist gleich int , dann es gibt kein Ganzzahl otherint der otherint ist grösserAlsOderGleich number und otherint ist kleinerAls int .
(=>
(equal
(CeilingFn ?NUMBER)
?INT)
(not
(exists
(?OTHERINT)
(and
(instance ?OTHERINT Integer)
(greaterThanOrEqualTo ?OTHERINT ?NUMBER)
(lessThan ?OTHERINT ?INT)))))
Wenn "die grösste Ganzzahl kleiner als oder Gleichgestelltes zu number" ist gleich int , dann es gibt kein Ganzzahl otherint der otherint ist kleinerAlsOderGleich number und otherint ist grösserAls int .
(=>
(equal
(FloorFn ?NUMBER)
?INT)
(not
(exists
(?OTHERINT)
(and
(instance ?OTHERINT Integer)
(lessThanOrEqualTo ?OTHERINT ?NUMBER)
(greaterThan ?OTHERINT ?INT)))))
- wenn "die größte gemeinsamer teiler von " ist gleich number ,
- dann für jeden element gilt: wenn element ist ein Mitglied von "()", dann "element betrag number" ist gleich
.
(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?NUMBER)
0))))
- wenn "die größte gemeinsamer teiler von " ist gleich number ,
- dann es gibt kein greater der greater ist grösserAls number und für jeden element gilt: wenn element ist ein Mitglied von "()", dann "element betrag greater" ist gleich
.
(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(not
(exists
(?GREATER)
(and
(greaterThan ?GREATER ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?GREATER)
0)))))))
Wenn number ist ein fall von Komplexzahl , dann es gibt ein part1,part2 der part1 ist gleich "das reelle teil von number" und part2 ist gleich "das imaginäre teil von number" .
(=>
(instance ?NUMBER ComplexNumber)
(exists
(?PART1 ?PART2)
(and
(equal
?PART1
(RealNumberFn ?NUMBER))
(equal
?PART2
(ImaginaryPartFn ?NUMBER)))))
- wenn "das kleinste gemeinsames vielfach von " ist gleich number ,
- dann für jeden element gilt: wenn element ist ein Mitglied von "()", dann "number betrag element" ist gleich
.
(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?NUMBER ?ELEMENT)
0))))
- wenn "das kleinste gemeinsames vielfach von " ist gleich number ,
- dann es gibt kein less der less ist kleinerAls number und für jeden element gilt: wenn element ist ein Mitglied von "()", dann "less betrag element" ist gleich
.
(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(not
(exists
(?LESS)
(and
(lessThan ?LESS ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?LESS ?ELEMENT)
0)))))))
Wenn "das grössere von number1 und number2" ist gleich number , dann - number ist gleich number1 und number1 ist grösserAls number2
oder - number ist gleich number2 und number2 ist grösserAls number1
oder - number ist gleich number1 und number ist gleich 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))))
Wenn "das kleinere von number1 und number2" ist gleich number , dann - number ist gleich number1 und number1 ist kleinerAls number2
oder - number ist gleich number2 und number2 ist kleinerAls number1
oder - number ist gleich number1 und number ist gleich 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))))
Wenn number ist ein fall von Eigenschaft , dann "der reziprokerwert von number" ist gleich "number in der te Potenz" .
(=>
(instance ?NUMBER Quantity)
(equal
(ReciprocalFn ?NUMBER)
(ExponentiationFn ?NUMBER -1)))
Wenn number ist ein fall von Eigenschaft , dann ist gleich "number*"der reziprokerwert von number"" .
(=>
(instance ?NUMBER Quantity)
(equal
1
(MultiplicationFn
?NUMBER
(ReciprocalFn ?NUMBER))))
"number1 betrag number2" ist gleich number nur wenn "(""die grösste Ganzzahl kleiner als oder Gleichgestelltes zu "number1/number2""*number2"+number)" ist gleich number1 .
(<=>
(equal
(RemainderFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(equal
(AdditionFn
(MultiplicationFn
(FloorFn
(DivisionFn ?NUMBER1 ?NUMBER2))
?NUMBER2)
?NUMBER)
?NUMBER1))
Wenn "number1 betrag number2" ist gleich number , dann "das zeichen von number2" ist gleich "das zeichen von number" .
(=>
(equal
(RemainderFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(equal
(SignumFn ?NUMBER2)
(SignumFn ?NUMBER)))
Wenn number ist ein fall von gerade Ganzzahl , dann "number betrag " ist gleich .
(=>
(instance ?NUMBER EvenInteger)
(equal
(RemainderFn ?NUMBER 2)
0))
Wenn number ist ein fall von ungerade Ganzzahl , dann "number betrag " ist gleich .
(=>
(instance ?NUMBER OddInteger)
(equal
(RemainderFn ?NUMBER 2)
1))
- wenn prime ist ein fall von Hauptzahl ,
- dann für jeden number gilt: wenn "prime betrag number" ist gleich , dann number ist gleich oder number ist gleich prime
.
(=>
(instance ?PRIME PrimeNumber)
(forall
(?NUMBER)
(=>
(equal
(RemainderFn ?PRIME ?NUMBER)
0)
(or
(equal ?NUMBER 1)
(equal ?NUMBER ?PRIME)))))
- wenn "number1 gerundet" ist gleich number2 ,
- dann
- wenn "(number1-"die grösste Ganzzahl kleiner als oder Gleichgestelltes zu number1")" ist kleinerAls , dann number2 ist gleich "die grösste Ganzzahl kleiner als oder Gleichgestelltes zu number1"
oder - wenn "(number1-"die grösste Ganzzahl kleiner als oder Gleichgestelltes zu number1")" ist grösserAlsOderGleich , dann number2 ist gleich "die oberstegrenze von 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)))))
Wenn number ist ein fall von nichtnegative reelle Zahl , dann "das zeichen von number" ist gleich oder "das zeichen von number" ist gleich .
(=>
(instance ?NUMBER NonnegativeRealNumber)
(or
(equal
(SignumFn ?NUMBER)
1)
(equal
(SignumFn ?NUMBER)
0)))
Wenn number ist ein fall von positive reelle Zahl , dann "das zeichen von number" ist gleich .
(=>
(instance ?NUMBER PositiveRealNumber)
(equal
(SignumFn ?NUMBER)
1))
Wenn number ist ein fall von negative reelle Zahl , dann "das zeichen von number" ist gleich .
(=>
(instance ?NUMBER NegativeRealNumber)
(equal
(SignumFn ?NUMBER)
-1))
Wenn "die quadratwurzel von number1" ist gleich number2 , dann "number2*number2" ist gleich number1 .
(=>
(equal
(SquareRootFn ?NUMBER1)
?NUMBER2)
(equal
(MultiplicationFn ?NUMBER2 ?NUMBER2)
?NUMBER1))
Wenn degree ist ein fall von Ebenerwinkelmass , dann "der tangens von degree" ist gleich ""der Sinus von degree"/"der Kosinus von degree"" .
(=>
(instance ?DEGREE PlaneAngleMeasure)
(equal
(TangentFn ?DEGREE)
(DivisionFn
(SineFn ?DEGREE)
(CosineFn ?DEGREE))))
- wenn id ist ein identitätsElement von function,
- dann für jeden inst gilt: wenn die Zahl Argument von function ist ein fall von class und inst ist ein fall von class , dann "function(id,inst)" ist gleich inst
.
(=>
(identityElement ?FUNCTION ?ID)
(forall
(?INST)
(=>
(and
(domain ?FUNCTION 1 ?CLASS)
(instance ?INST ?CLASS))
(equal
(AssignmentFn ?FUNCTION ?ID ?INST)
?INST))))
Wenn "(int1+1)" ist gleich "(int2+1)" , dann int1 ist gleich int2 .
(=>
(equal
(SuccessorFn ?INT1)
(SuccessorFn ?INT2))
(equal ?INT1 ?INT2))
Wenn int ist ein fall von Ganzzahl , dann int ist gleich "("(int+2)"+1)" .
(=>
(instance ?INT Integer)
(equal
?INT
(SuccessorFn
(PredecessorFn ?INT))))
Wenn int ist ein fall von Ganzzahl , dann int ist gleich "("(int+1)"+2)" .
(=>
(instance ?INT Integer)
(equal
?INT
(PredecessorFn
(SuccessorFn ?INT))))
Wenn "(int1+2)" ist gleich "(int2+2)" , dann int1 ist gleich int2 .
(=>
(equal
(PredecessorFn ?INT1)
(PredecessorFn ?INT2))
(equal ?INT1 ?INT2))
Wenn für jeden element gilt: element ist ein element von set1 nur wenn element ist ein element von set2 , dann set1 ist gleich set2 .
(=>
(forall
(?ELEMENT)
(<=>
(element ?ELEMENT ?SET1)
(element ?ELEMENT ?SET2)))
(equal ?SET1 ?SET2))
Wenn set ist ein fall von begrenzte Menge , dann es gibt ein nichtnegative Ganzzahl number der number ist gleich "die Zahl Fällen in set" .
(=>
(instance ?SET FiniteSet)
(exists
(?NUMBER)
(and
(instance ?NUMBER NonnegativeInteger)
(equal
?NUMBER
(CardinalityFn ?SET)))))
- wenn superclass ist ein fall von paarweise disjunkte Kategorie ,
- dann für jeden class1,class2 gilt: wenn class1 ist ein fall von superclass und class2 ist ein fall von superclass , dann class1 ist gleich class2 oder class1 ist dijunkt von class2
.
(=>
(instance ?SUPERCLASS PairwiseDisjointClass)
(forall
(?CLASS1 ?CLASS2)
(=>
(and
(instance ?CLASS1 ?SUPERCLASS)
(instance ?CLASS2 ?SUPERCLASS))
(or
(equal ?CLASS1 ?CLASS2)
(disjoint ?CLASS1 ?CLASS2)))))
Wenn graph ist ein fall von Graph und node1 ist ein fall von Graphknoten und node2 ist ein fall von Graphknoten und node1 ist ein teil von graph und node2 ist ein teil von graph und node1 ist gleich node2 nicht, dann es gibt ein arc,path der - arc verbindet node1 und node2
oder - path ist ein teilgraph von graph
und - path ist ein fall von Graphweg
und - "der anfang von path" ist gleich node1 und "das ende von path" ist gleich node2
oder - "der anfang von path" ist gleich node2 und "das ende von path" ist gleich node1
(=>
(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)))))))
Wenn graph ist ein fall von Graph , dann es gibt ein node1,node2,node3,arc1,arc2 der node1 ist ein teil von graph und node2 ist ein teil von graph und node3 ist ein teil von graph und arc1 ist ein teil von graph und arc2 ist ein teil von graph und node2 verbindet arc1 und node1 und node3 verbindet arc2 und node2 und node1 ist gleich node2 nicht und node2 ist gleich node3 nicht und node1 ist gleich node3 nicht und arc1 ist gleich arc2 nicht.
(=>
(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)))))
Wenn graph ist ein fall von gerichtetes Graph und arc ist ein fall von Graphbogen und arc ist ein teil von graph , dann es gibt ein node1,node2 der "das ausgangsnullpunkt von arc" ist gleich node1 und "das terminalnullpunkt von arc" ist gleich 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 ist ein fall von Graphschaltkreis nur wenn es gibt ein node der "der anfang von graph" ist gleich node und "das ende von graph" ist gleich node .
(<=>
(instance ?GRAPH GraphCircuit)
(exists
(?NODE)
(and
(equal
(BeginNodeFn ?GRAPH)
?NODE)
(equal
(EndNodeFn ?GRAPH)
?NODE))))
graph ist ein fall von Multigraph nur wenn es gibt ein arc1,arc2,node1,node2 der arc1 ist ein teil von graph und arc2 ist ein teil von graph und node1 ist ein teil von graph und node2 ist ein teil von graph und arc1 verbindet node1 und node2 und arc2 verbindet node1 und node2 und arc1 ist gleich arc2 nicht.
(<=>
(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)))))
Wenn "das ausgangsnullpunkt von arc" ist gleich node und "das terminalnullpunkt von arc" ist gleich node , dann arc ist ein fall von Graphschleife .
(=>
(and
(equal
(InitialNodeFn ?ARC)
?NODE)
(equal
(TerminalNodeFn ?ARC)
?NODE))
(instance ?ARC GraphLoop))
- wenn
- "der wert von path" ist gleich sum
und - subpath ist ein teilgraph von path
und - arc1 ist ein teil von path
und - der wert von arc1 ist number1
und - für jeden arc2 gilt: wenn arc2 ist ein teil von path , dann arc2 ist ein teil von subpath oder arc2 ist gleich arc1
, - dann sum ist gleich "("der wert von 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)))
- wenn
- "der wert von path" ist gleich sum
und - arc1 ist ein teil von path
und - arc2 ist ein teil von path
und - der wert von arc1 ist number1
und - der wert von arc2 ist number2
und - für jeden arc3 gilt: wenn arc3 ist ein teil von path , dann arc3 ist gleich arc1 oder arc3 ist gleich arc2
, - dann "der wert von path" ist gleich "(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)))
Wenn "der Pfad der niedrigsten Kosten zwischen node1 und node2" ist gleich path , dann path ist ein fall von "die menge von Pfaden zwischen node1 und node2" .
(=>
(equal
(MinimalWeightedPathFn ?NODE1 ?NODE2)
?PATH)
(instance
?PATH
(GraphPathFn ?NODE1 ?NODE2)))
- wenn "der Pfad der niedrigsten Kosten zwischen node1 und node2" ist gleich path und "der wert von path" ist gleich number ,
- dann für jeden path2 gilt: wenn path2 ist ein fall von "die menge von Pfaden zwischen node1 und node2" und "der wert von path2" ist gleich number2 , dann number2 ist grösserAlsOderGleich 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))))
Wenn "der Pfad der höchsten Kosten zwischen node1 und node2" ist gleich path , dann path ist ein fall von "die menge von Pfaden zwischen node1 und node2" .
(=>
(equal
(MaximalWeightedPathFn ?NODE1 ?NODE2)
?PATH)
(instance
?PATH
(GraphPathFn ?NODE1 ?NODE2)))
- wenn "der Pfad der höchsten Kosten zwischen node1 und node2" ist gleich path und "der wert von path" ist gleich number ,
- dann für jeden path2 gilt: wenn path2 ist ein fall von "die menge von Pfaden zwischen node1 und node2" und "der wert von path2" ist gleich number2 , dann number2 ist kleinerAlsOderGleich 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))))
Wenn path ist ein teil von graph und graph ist ein fall von gerichtetes Graph nicht, dann "die menge von Pfaden zwischen node1 und node2" ist gleich path nur wenn "die menge von Pfaden zwischen node2 und node1" ist gleich path .
(=>
(and
(graphPart ?PATH ?GRAPH)
(not
(instance ?GRAPH DirectedGraph)))
(<=>
(equal
(GraphPathFn ?NODE1 ?NODE2)
?PATH)
(equal
(GraphPathFn ?NODE2 ?NODE1)
?PATH)))
- wenn "die menge von minimalen Pfaden die graph in zwei verschiedene Graphen schnitten" ist gleich pathclass ,
- dann es gibt ein number der für jeden path gilt: wenn path ist ein fall von pathclass , dann die länge von path ist number
.
(=>
(equal
(MinimalCutSetFn ?GRAPH)
?PATHCLASS)
(exists
(?NUMBER)
(forall
(?PATH)
(=>
(instance ?PATH ?PATHCLASS)
(pathLength ?PATH ?NUMBER)))))
Wenn "number unit(s)" ist gleich quant und unit ist eine teilkategorie von quanttype, dann quant ist ein fall von quanttype .
(=>
(and
(equal
(MeasureFn ?NUMBER ?UNIT)
?QUANT)
(subclass ?UNIT ?QUANTTYPE))
(instance ?QUANT ?QUANTTYPE))
Wenn unit ist ein fall von Masseinheit , dann "1 tausend unit" ist gleich " unit(s)" .
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(KiloFn ?UNIT)
(MeasureFn 1000 ?UNIT)))
Wenn unit ist ein fall von Masseinheit , dann "1 million unit" ist gleich " unit(s)" .
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MegaFn ?UNIT)
(MeasureFn 1000000 ?UNIT)))
Wenn unit ist ein fall von Masseinheit , dann "1 milliarde unit" ist gleich " unit(s)" .
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(GigaFn ?UNIT)
(MeasureFn 1000000000 ?UNIT)))
Wenn unit ist ein fall von Masseinheit , dann "1 trillion unit" ist gleich " unit(s)" .
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(TeraFn ?UNIT)
(MeasureFn 1000000000000 ?UNIT)))
Wenn unit ist ein fall von Masseinheit , dann "ein tausendstes einer unit" ist gleich " unit(s)" .
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MilliFn ?UNIT)
(MeasureFn 0.001 ?UNIT)))
Wenn unit ist ein fall von Masseinheit , dann "ein millionstel einer unit" ist gleich " unit(s)" .
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(MicroFn ?UNIT)
(MeasureFn 0.000001 ?UNIT)))
Wenn unit ist ein fall von Masseinheit , dann "ein milliardstel einer unit" ist gleich " unit(s)" .
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(NanoFn ?UNIT)
(MeasureFn 0.000000001 ?UNIT)))
Wenn unit ist ein fall von Masseinheit , dann "ein trillionstel einer unit" ist gleich " unit(s)" .
(=>
(instance ?UNIT UnitOfMeasure)
(equal
(PicoFn ?UNIT)
(MeasureFn 0.000000000001 ?UNIT)))
Wenn number ist ein fall von reelle Zahl und unit ist ein fall von Masseinheit , dann "die grösse von "number unit(s)"" ist gleich number .
(=>
(and
(instance ?NUMBER RealNumber)
(instance ?UNIT UnitOfMeasure))
(equal
(MagnitudeFn
(MeasureFn ?NUMBER ?UNIT))
?NUMBER))
Wenn number ist ein fall von reelle Zahl , dann "number centimeter(s)" ist gleich ""number*" meter(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Centimeter)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
Meter)))
Wenn number ist ein fall von reelle Zahl , dann "number celsius degree(s)" ist gleich ""(number-)" kelvin degree(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER CelsiusDegree)
(MeasureFn
(SubtractionFn ?NUMBER 273.15)
KelvinDegree)))
Wenn number ist ein fall von reelle Zahl , dann "number celsius degree(s)" ist gleich """(number-)"/" fahrenheit degree(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER CelsiusDegree)
(MeasureFn
(DivisionFn
(SubtractionFn ?NUMBER 32)
1.8)
FahrenheitDegree)))
Wenn number ist ein fall von reelle Zahl , dann "number day duration(s)" ist gleich ""number*" hour duration(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER DayDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 24)
HourDuration)))
Wenn number ist ein fall von reelle Zahl , dann "number hour duration(s)" ist gleich ""number*" minute duration(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER HourDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 60)
MinuteDuration)))
Wenn number ist ein fall von reelle Zahl , dann "number minute duration(s)" ist gleich ""number*" second duration(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER MinuteDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 60)
SecondDuration)))
Wenn number ist ein fall von reelle Zahl , dann "number week duration(s)" ist gleich ""number*" day duration(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER WeekDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 7)
DayDuration)))
Wenn number ist ein fall von reelle Zahl , dann "number year duration(s)" ist gleich ""number*" day duration(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER YearDuration)
(MeasureFn
(MultiplicationFn ?NUMBER 365)
DayDuration)))
Wenn number ist ein fall von reelle Zahl , dann "number amu(s)" ist gleich ""number**" gram(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Amu)
(MeasureFn
(MultiplicationFn ?NUMBER 1.6605402 E-24)
Gram)))
Wenn number ist ein fall von reelle Zahl , dann "number electron volt(s)" ist gleich ""number**" joule(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER ElectronVolt)
(MeasureFn
(MultiplicationFn ?NUMBER 1.60217733 E-19)
Joule)))
Wenn number ist ein fall von reelle Zahl , dann "number angstrom(s)" ist gleich ""number**" meter(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Angstrom)
(MeasureFn
(MultiplicationFn ?NUMBER 1.0 E-10)
Meter)))
Wenn number ist ein fall von reelle Zahl , dann "number foot(s)" ist gleich ""number*" meter(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Foot)
(MeasureFn
(MultiplicationFn ?NUMBER 0.3048)
Meter)))
Wenn number ist ein fall von reelle Zahl , dann "number inch(s)" ist gleich ""number*" meter(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Inch)
(MeasureFn
(MultiplicationFn ?NUMBER 0.0254)
Meter)))
Wenn number ist ein fall von reelle Zahl , dann "number mile(s)" ist gleich ""number*" meter(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Mile)
(MeasureFn
(MultiplicationFn ?NUMBER 1609.344)
Meter)))
Wenn number ist ein fall von reelle Zahl , dann "number united states gallon(s)" ist gleich ""number*" liter(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedStatesGallon)
(MeasureFn
(MultiplicationFn ?NUMBER 3.785411784)
Liter)))
Wenn number ist ein fall von reelle Zahl , dann "number quart(s)" ist gleich ""number/" united states gallon(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Quart)
(MeasureFn
(DivisionFn ?NUMBER 4)
UnitedStatesGallon)))
Wenn number ist ein fall von reelle Zahl , dann "number pint(s)" ist gleich ""number/" quart(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Pint)
(MeasureFn
(DivisionFn ?NUMBER 2)
Quart)))
Wenn number ist ein fall von reelle Zahl , dann "number cup(s)" ist gleich ""number/" pint(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Cup)
(MeasureFn
(DivisionFn ?NUMBER 2)
Pint)))
Wenn number ist ein fall von reelle Zahl , dann "number ounce(s)" ist gleich ""number/" cup(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Ounce)
(MeasureFn
(DivisionFn ?NUMBER 8)
Cup)))
Wenn number ist ein fall von reelle Zahl , dann "number united kingdom gallon(s)" ist gleich ""number*" liter(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedKingdomGallon)
(MeasureFn
(MultiplicationFn ?NUMBER 4.54609)
Liter)))
Wenn number ist ein fall von reelle Zahl , dann "number pound mass(s)" ist gleich ""number*" gram(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER PoundMass)
(MeasureFn
(MultiplicationFn ?NUMBER 453.59237)
Gram)))
Wenn number ist ein fall von reelle Zahl , dann "number slug(s)" ist gleich ""number*" gram(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Slug)
(MeasureFn
(MultiplicationFn ?NUMBER 14593.90)
Gram)))
Wenn number ist ein fall von reelle Zahl , dann "number rankine degree(s)" ist gleich ""number*" kelvin degree(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER RankineDegree)
(MeasureFn
(MultiplicationFn ?NUMBER 1.8)
KelvinDegree)))
Wenn number ist ein fall von reelle Zahl , dann "number pound force(s)" ist gleich ""number*" newton(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER PoundForce)
(MeasureFn
(MultiplicationFn ?NUMBER 4.448222)
Newton)))
Wenn number ist ein fall von reelle Zahl , dann "number calorie(s)" ist gleich ""number*" joule(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Calorie)
(MeasureFn
(MultiplicationFn ?NUMBER 4.1868)
Joule)))
Wenn number ist ein fall von reelle Zahl , dann "number british thermal unit(s)" ist gleich ""number*" joule(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER BritishThermalUnit)
(MeasureFn
(MultiplicationFn ?NUMBER 1055.05585262)
Joule)))
Wenn number ist ein fall von reelle Zahl , dann "number angular degree(s)" ist gleich ""number*"Pi/"" radian(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER AngularDegree)
(MeasureFn
(MultiplicationFn
?NUMBER
(DivisionFn Pi 180))
Radian)))
Wenn number ist ein fall von reelle Zahl , dann "number united states cent(s)" ist gleich ""number*" united states dollar(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER UnitedStatesCent)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
UnitedStatesDollar)))
Wenn number ist ein fall von reelle Zahl , dann "number euro cent(s)" ist gleich ""number*" euro dollar(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER EuroCent)
(MeasureFn
(MultiplicationFn ?NUMBER 0.01)
EuroDollar)))
Wenn number ist ein fall von reelle Zahl , dann "number byte(s)" ist gleich ""number*" bit(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER Byte)
(MeasureFn
(MultiplicationFn ?NUMBER 8)
Bit)))
Wenn number ist ein fall von reelle Zahl , dann "number kilo byte(s)" ist gleich ""number*" byte(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER KiloByte)
(MeasureFn
(MultiplicationFn ?NUMBER 1024)
Byte)))
Wenn number ist ein fall von reelle Zahl , dann "number mega byte(s)" ist gleich ""number*" kilo byte(s)" .
(=>
(instance ?NUMBER RealNumber)
(equal
(MeasureFn ?NUMBER MegaByte)
(MeasureFn
(MultiplicationFn ?NUMBER 1024)
KiloByte)))
"wert von dem Eigentum von person" ist gleich amount nur wenn wert von "eigentum von person" ist amount.
(<=>
(equal
(WealthFn ?PERSON)
?AMOUNT)
(monetaryValue
(PropertyFn ?PERSON)
?AMOUNT))
Wenn point ist ein fall von Zeitpunkt und point ist gleich positive infinity nicht, dann point geschieht vor positive infinity .
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT PositiveInfinity)))
(before ?POINT PositiveInfinity))
Wenn point ist ein fall von Zeitpunkt und point ist gleich positive infinity nicht, dann es gibt ein otherpoint der otherpoint ist zwischen point und positive infinity.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT PositiveInfinity)))
(exists
(?OTHERPOINT)
(temporallyBetween ?POINT ?OTHERPOINT PositiveInfinity)))
Wenn point ist ein fall von Zeitpunkt und point ist gleich negative infinity nicht, dann negative infinity geschieht vor point .
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT NegativeInfinity)))
(before NegativeInfinity ?POINT))
Wenn point ist ein fall von Zeitpunkt und point ist gleich negative infinity nicht, dann es gibt ein otherpoint der otherpoint ist zwischen negative infinity und point.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT NegativeInfinity)))
(exists
(?OTHERPOINT)
(temporallyBetween NegativeInfinity ?OTHERPOINT ?POINT)))
- wenn "der anfang von interval" ist gleich point ,
- dann für jeden otherpoint gilt: wenn otherpoint ist ein teil von interval und otherpoint ist gleich point nicht, dann point geschieht vor otherpoint
.
(=>
(equal
(BeginFn ?INTERVAL)
?POINT)
(forall
(?OTHERPOINT)
(=>
(and
(temporalPart ?OTHERPOINT ?INTERVAL)
(not
(equal ?OTHERPOINT ?POINT)))
(before ?POINT ?OTHERPOINT))))
- wenn "das ende von interval" ist gleich point ,
- dann für jeden otherpoint gilt: wenn otherpoint ist ein teil von interval und otherpoint ist gleich point nicht, dann otherpoint geschieht vor point
.
(=>
(equal
(EndFn ?INTERVAL)
?POINT)
(forall
(?OTHERPOINT)
(=>
(and
(temporalPart ?OTHERPOINT ?INTERVAL)
(not
(equal ?OTHERPOINT ?POINT)))
(before ?OTHERPOINT ?POINT))))
interval1 beginnt interval2 nur wenn "der anfang von interval1" ist gleich "der anfang von interval2" und "das ende von interval1" geschieht vor "das ende von interval2" .
(<=>
(starts ?INTERVAL1 ?INTERVAL2)
(and
(equal
(BeginFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(before
(EndFn ?INTERVAL1)
(EndFn ?INTERVAL2))))
interval1 beendet interval2 nur wenn "der anfang von interval2" geschieht vor "der anfang von interval1" und "das ende von interval2" ist gleich "das ende von interval1" .
(<=>
(finishes ?INTERVAL1 ?INTERVAL2)
(and
(before
(BeginFn ?INTERVAL2)
(BeginFn ?INTERVAL1))
(equal
(EndFn ?INTERVAL2)
(EndFn ?INTERVAL1))))
Wenn point1 geschieht vor oder gleichzeitig mit point2 , dann point1 geschieht vor point2 oder point1 ist gleich point2 .
(=>
(beforeOrEqual ?POINT1 ?POINT2)
(or
(before ?POINT1 ?POINT2)
(equal ?POINT1 ?POINT2)))
interval1 schliesst interval2 zeitlich an nur wenn "das ende von interval1" ist gleich "der anfang von interval2" .
(<=>
(meetsTemporally ?INTERVAL1 ?INTERVAL2)
(equal
(EndFn ?INTERVAL1)
(BeginFn ?INTERVAL2)))
Wenn "der anfang von interval1" ist gleich "der anfang von interval2" und "das ende von interval1" ist gleich "das ende von interval2" , dann interval1 ist gleich interval2 .
(=>
(and
(equal
(BeginFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(equal
(EndFn ?INTERVAL1)
(EndFn ?INTERVAL2)))
(equal ?INTERVAL1 ?INTERVAL2))
phys1 geschiecht gleichzeitig mit phys2 nur wenn "die zeit des Bestehens von phys1" ist gleich "die zeit des Bestehens von phys2" .
(<=>
(cooccur ?PHYS1 ?PHYS2)
(equal
(WhenFn ?PHYS1)
(WhenFn ?PHYS2)))
Wenn "abstand zwischen point1 und point2" ist gleich interval , dann "der anfang von interval" ist gleich point1 und "das ende von interval" ist gleich point2 .
(=>
(equal
(TimeIntervalFn ?POINT1 ?POINT2)
?INTERVAL)
(and
(equal
(BeginFn ?INTERVAL)
?POINT1)
(equal
(EndFn ?INTERVAL)
?POINT2)))
Wenn "abstand zwischen point1 und point2" ist gleich interval , dann für jeden point gilt: point ist zwischen oder gleichzeitig mit point1 und point2 nur wenn point ist ein teil von interval .
(=>
(equal
(TimeIntervalFn ?POINT1 ?POINT2)
?INTERVAL)
(forall
(?POINT)
(<=>
(temporallyBetweenOrEqual ?POINT1 ?POINT ?POINT2)
(temporalPart ?POINT ?INTERVAL))))
Wenn process ist ein fall von körperlicher Gegenstand , dann "vor "die zeit des Bestehens von process"" ist gleich "abstand zwischen negative infinity und "der anfang von "die zeit des Bestehens von process""" .
(=>
(instance ?PROCESS Physical)
(equal
(PastFn
(WhenFn ?PROCESS))
(TimeIntervalFn
NegativeInfinity
(BeginFn
(WhenFn ?PROCESS)))))
Wenn process ist ein fall von körperlicher Gegenstand , dann "nach "die zeit des Bestehens von process"" ist gleich "abstand zwischen "das ende von "die zeit des Bestehens von process"" und positive infinity" .
(=>
(instance ?PROCESS Physical)
(equal
(FutureFn
(WhenFn ?PROCESS))
(TimeIntervalFn
(EndFn
(WhenFn ?PROCESS))
PositiveInfinity)))
Wenn day1 ist ein fall von "der tag number1" und day2 ist ein fall von "der tag number2" und "(number2-number1)" ist gleich , dann day1 schliesst day2 zeitlich an.
(=>
(and
(instance
?DAY1
(DayFn ?NUMBER1 ?MONTH))
(instance
?DAY2
(DayFn ?NUMBER2 ?MONTH))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?DAY1 ?DAY2))
Wenn hour1 ist ein fall von "die stunde number1" und hour2 ist ein fall von "die stunde number2" und "(number2-number1)" ist gleich , dann hour1 schliesst hour2 zeitlich an.
(=>
(and
(instance
?HOUR1
(HourFn ?NUMBER1 ?DAY))
(instance
?HOUR2
(HourFn ?NUMBER2 ?DAY))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?HOUR1 ?HOUR2))
Wenn minute1 ist ein fall von "die minute number1" und minute2 ist ein fall von "die minute number2" und "(number2-number1)" ist gleich , dann minute1 schliesst minute2 zeitlich an.
(=>
(and
(instance
?MINUTE1
(MinuteFn ?NUMBER1 ?HOUR))
(instance
?MINUTE2
(MinuteFn ?NUMBER2 ?HOUR))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?MINUTE1 ?MINUTE2))
Wenn second1 ist ein fall von "die sekund number1" und second2 ist ein fall von "die sekund number2" und "(number2-number1)" ist gleich , dann second1 schliesst second2 zeitlich an.
(=>
(and
(instance
?SECOND1
(SecondFn ?NUMBER1 ?MINUTE))
(instance
?SECOND2
(SecondFn ?NUMBER2 ?MINUTE))
(equal
(SubtractionFn ?NUMBER2 ?NUMBER1)
1))
(meetsTemporally ?SECOND1 ?SECOND2))
Wenn year1 ist ein fall von Jahr und year2 ist ein fall von Jahr und "(year2-year1)" ist gleich , dann year1 schliesst year2 zeitlich an.
(=>
(and
(instance ?YEAR1 Year)
(instance ?YEAR2 Year)
(equal
(SubtractionFn ?YEAR2 ?YEAR1)
1))
(meetsTemporally ?YEAR1 ?YEAR2))
Wenn leap ist ein fall von Schaltjahr und leap ist gleich "number Jahr(s)" , dann - "number betrag " ist gleich und "number betrag " ist gleich nicht
oder - "number betrag " ist gleich
.
(=>
(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)))
Wenn month1 ist gleich "der monat Januar" und month2 ist gleich "der monat Februar" , dann month1 schliesst month2 zeitlich an.
(=>
(and
(equal
?MONTH1
(MonthFn January ?YEAR))
(equal
?MONTH2
(MonthFn February ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Wenn "der monat Februar" ist gleich month und year ist ein fall von Schaltjahr nicht, dann dauer von month ist " day duration(s)" .
(=>
(and
(equal
(MonthFn February ?YEAR)
?MONTH)
(not
(instance ?YEAR LeapYear)))
(duration
?MONTH
(MeasureFn 28 DayDuration)))
Wenn "der monat Februar" ist gleich month und year ist ein fall von Schaltjahr , dann dauer von month ist " day duration(s)" .
(=>
(and
(equal
(MonthFn February ?YEAR)
?MONTH)
(instance ?YEAR LeapYear))
(duration
?MONTH
(MeasureFn 29 DayDuration)))
Wenn month1 ist gleich "der monat Februar" und month2 ist gleich "der monat März" , dann month1 schliesst month2 zeitlich an.
(=>
(and
(equal
?MONTH1
(MonthFn February ?YEAR))
(equal
?MONTH2
(MonthFn March ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Wenn month1 ist gleich "der monat März" und month2 ist gleich "der monat April" , dann month1 schliesst month2 zeitlich an.
(=>
(and
(equal
?MONTH1
(MonthFn March ?YEAR))
(equal
?MONTH2
(MonthFn April ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Wenn month1 ist gleich "der monat April" und month2 ist gleich "der monat Mai" , dann month1 schliesst month2 zeitlich an.
(=>
(and
(equal
?MONTH1
(MonthFn April ?YEAR))
(equal
?MONTH2
(MonthFn May ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Wenn month1 ist gleich "der monat Mai" und month2 ist gleich "der monat Juni" , dann month1 schliesst month2 zeitlich an.
(=>
(and
(equal
?MONTH1
(MonthFn May ?YEAR))
(equal
?MONTH2
(MonthFn June ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Wenn month1 ist gleich "der monat Juni" und month2 ist gleich "der monat Juli" , dann month1 schliesst month2 zeitlich an.
(=>
(and
(equal
?MONTH1
(MonthFn June ?YEAR))
(equal
?MONTH2
(MonthFn July ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Wenn month1 ist gleich "der monat Juli" und month2 ist gleich "der monat August" , dann month1 schliesst month2 zeitlich an.
(=>
(and
(equal
?MONTH1
(MonthFn July ?YEAR))
(equal
?MONTH2
(MonthFn August ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Wenn month1 ist gleich "der monat August" und month2 ist gleich "der monat September" , dann month1 schliesst month2 zeitlich an.
(=>
(and
(equal
?MONTH1
(MonthFn August ?YEAR))
(equal
?MONTH2
(MonthFn September ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Wenn month1 ist gleich "der monat September" und month2 ist gleich "der monat Oktober" , dann month1 schliesst month2 zeitlich an.
(=>
(and
(equal
?MONTH1
(MonthFn September ?YEAR))
(equal
?MONTH2
(MonthFn October ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Wenn month1 ist gleich "der monat Oktober" und month2 ist gleich "der monat November" , dann month1 schliesst month2 zeitlich an.
(=>
(and
(equal
?MONTH1
(MonthFn October ?YEAR))
(equal
?MONTH2
(MonthFn November ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Wenn month1 ist gleich "der monat November" und month2 ist gleich "der monat Dezember" , dann month1 schliesst month2 zeitlich an.
(=>
(and
(equal
?MONTH1
(MonthFn November ?YEAR))
(equal
?MONTH2
(MonthFn December ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
Wenn month1 ist gleich "der monat Dezember" und month2 ist gleich "der monat Januar" und year1 schliesst year2 zeitlich an, dann month1 schliesst month2 zeitlich an.
(=>
(and
(equal
?MONTH1
(MonthFn December ?YEAR1))
(equal
?MONTH2
(MonthFn January ?YEAR2))
(meetsTemporally ?YEAR1 ?YEAR2))
(meetsTemporally ?MONTH1 ?MONTH2))
- wenn "Aufspaltung von interval auf ? interval-types" ist gleich class ,
- dann für jeden time1,time2 gilt: wenn time1 ist ein fall von interval-type und time2 ist ein fall von class , dann es gibt ein duration der dauer von time1 ist duration und dauer von time2 ist 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))))))
- wenn "Aufspaltung von interval auf ? interval-types" ist gleich class ,
- dann für jeden time1,time2 gilt: wenn time1 ist ein fall von class und time2 ist ein fall von class und time1 ist gleich time2 nicht, dann time1 schliesst time2 zeitlich an oder time2 schliesst time1 zeitlich an oder time1 geschieht früh als time2 oder time2 geschieht früh als 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)))))
Wenn "Aufspaltung von interval auf ? interval-types" ist gleich class , dann es gibt ein class time der time beginnt interval .
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(exists
(?TIME)
(and
(instance ?TIME ?CLASS)
(starts ?TIME ?INTERVAL))))
Wenn "Aufspaltung von interval auf ? interval-types" ist gleich class , dann es gibt ein class time der time beendet interval .
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(exists
(?TIME)
(and
(instance ?TIME ?CLASS)
(finishes ?TIME ?INTERVAL))))
- wenn "Aufspaltung von interval auf ? interval-types" ist gleich class ,
- dann für jeden time1 gilt: wenn time1 ist ein fall von class und time1 beendet interval nicht, dann es gibt ein class time2 der time1 schliesst time2 zeitlich an
.
(=>
(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))))))
- wenn "Aufspaltung von interval auf ? interval-types" ist gleich class ,
- dann für jeden time1 gilt: wenn time1 ist ein fall von class und time1 beginnt interval nicht, dann es gibt ein class time2 der time2 schliesst time1 zeitlich an
.
(=>
(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))))))
- wenn "Aufspaltung von interval auf ? interval-types" ist gleich class ,
- dann für jeden time gilt: wenn time ist ein fall von Zeitpunkt und time ist ein teil von interval , dann es gibt ein class instance der time ist ein teil von 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))))))
Wenn year ist ein fall von Jahr , dann "die Zahl Fällen in "Aufspaltung von year auf ? Monats"" ist gleich .
(=>
(instance ?YEAR Year)
(equal
(CardinalityFn
(TemporalCompositionFn ?YEAR Month))
12))
Wenn month ist ein fall von Monat und dauer von month ist "number day duration(s)" , dann "die Zahl Fällen in "Aufspaltung von month auf ? Tags"" ist gleich number .
(=>
(and
(instance ?MONTH Month)
(duration
?MONTH
(MeasureFn ?NUMBER DayDuration)))
(equal
(CardinalityFn
(TemporalCompositionFn ?MONTH Day))
?NUMBER))
Wenn week ist ein fall von Woche , dann "die Zahl Fällen in "Aufspaltung von week auf ? Tags"" ist gleich .
(=>
(instance ?WEEK Week)
(equal
(CardinalityFn
(TemporalCompositionFn ?WEEK Day))
7))
Wenn day ist ein fall von Tag , dann "die Zahl Fällen in "Aufspaltung von day auf ? Stundes"" ist gleich .
(=>
(instance ?DAY Day)
(equal
(CardinalityFn
(TemporalCompositionFn ?DAY Hour))
24))
Wenn hour ist ein fall von Stunde , dann "die Zahl Fällen in "Aufspaltung von hour auf ? Minutes"" ist gleich .
(=>
(instance ?HOUR Hour)
(equal
(CardinalityFn
(TemporalCompositionFn ?HOUR Minute))
60))
Wenn minute ist ein fall von Minute , dann "die Zahl Fällen in "Aufspaltung von minute auf ? Sekundes"" ist gleich .
(=>
(instance ?MINUTE Minute)
(equal
(CardinalityFn
(TemporalCompositionFn ?MINUTE Second))
60))
obj ist ein fall von selbstverbundener Gegenstand nur wenn für jeden part1,part2 gilt: wenn obj ist gleich "die vereinigung von den teilen von part1 und part2" , dann part1 wird an part2 angeschlossen.
(<=>
(instance ?OBJ SelfConnectedObject)
(forall
(?PART1 ?PART2)
(=>
(equal
?OBJ
(MereologicalSumFn ?PART1 ?PART2))
(connected ?PART1 ?PART2))))
Wenn obj1 ist ein Mitglied von coll und obj2 ist ein Mitglied von coll und obj1 ist gleich obj2 nicht, dann obj1 deckt sich mit obj2 räumlich nicht.
(=>
(and
(member ?OBJ1 ?COLL)
(member ?OBJ2 ?COLL)
(not
(equal ?OBJ1 ?OBJ2)))
(not
(overlapsSpatially ?OBJ1 ?OBJ2)))
Wenn obj3 ist gleich "die vereinigung von den teilen von obj1 und obj2" , dann für jeden part gilt: part ist ein teil von obj3 nur wenn part ist ein teil von obj1 oder part ist ein teil von obj2 .
(=>
(equal
?OBJ3
(MereologicalSumFn ?OBJ1 ?OBJ2))
(forall
(?PART)
(<=>
(part ?PART ?OBJ3)
(or
(part ?PART ?OBJ1)
(part ?PART ?OBJ2)))))
Wenn obj3 ist gleich "der durchschnitt von den teilen von obj1 und obj2" , dann für jeden part gilt: part ist ein teil von obj3 nur wenn part ist ein teil von obj1 und part ist ein teil von obj2 .
(=>
(equal
?OBJ3
(MereologicalProductFn ?OBJ1 ?OBJ2))
(forall
(?PART)
(<=>
(part ?PART ?OBJ3)
(and
(part ?PART ?OBJ1)
(part ?PART ?OBJ2)))))
Wenn obj3 ist gleich "die differenz zwischen den Teilen von obj1 und obj2" , dann für jeden part gilt: part ist ein teil von obj3 nur wenn part ist ein teil von obj1 und part ist ein teil von obj2 nicht.
(=>
(equal
?OBJ3
(MereologicalDifferenceFn ?OBJ1 ?OBJ2))
(forall
(?PART)
(<=>
(part ?PART ?OBJ3)
(and
(part ?PART ?OBJ1)
(not
(part ?PART ?OBJ2))))))
Wenn obj1 ist gleich "der wirt von dem Loch hole" , dann für jeden obj2 gilt: obj2 deckt sich mit obj1 räumlich nur wenn es gibt ein obj3 der hole ist ein loch in obj3 und obj2 deckt sich mit obj3 räumlich .
(=>
(equal
?OBJ1
(PrincipalHostFn ?HOLE))
(forall
(?OBJ2)
(<=>
(overlapsSpatially ?OBJ2 ?OBJ1)
(exists
(?OBJ3)
(and
(hole ?HOLE ?OBJ3)
(overlapsSpatially ?OBJ2 ?OBJ3))))))
Wenn obj1 ist gleich "die oberfläche von dem Loch hole" , dann für jeden obj2 gilt: obj2 deckt sich mit obj1 räumlich nur wenn es gibt ein obj3 der obj3 ist ein oberflächliches teil von "der wirt von dem Loch hole" und hole schliesst obj3 räumlich an und obj2 deckt sich mit obj3 räumlich .
(=>
(equal
?OBJ1
(SkinFn ?HOLE))
(forall
(?OBJ2)
(<=>
(overlapsSpatially ?OBJ2 ?OBJ1)
(exists
(?OBJ3)
(and
(superficialPart
?OBJ3
(PrincipalHostFn ?HOLE))
(meetsSpatially ?HOLE ?OBJ3)
(overlapsSpatially ?OBJ2 ?OBJ3))))))
Wenn subproc ist ein subProzess von proc, dann "die zeit des Bestehens von subproc" ist gleich "die zeit des Bestehens von proc" oder "die zeit des Bestehens von subproc" geschieht während "die zeit des Bestehens von proc" .
(=>
(subProcess ?SUBPROC ?PROC)
(or
(equal
(WhenFn ?SUBPROC)
(WhenFn ?PROC))
(during
(WhenFn ?SUBPROC)
(WhenFn ?PROC))))
Wenn rep ist ein fall von asexuelle Wiedergabe und organism ist ein resultat von rep , dann es gibt kein parent1,parent2 der parent1 ist das elterntiel von organism und parent2 ist das elterntiel von organism und parent1 ist gleich parent2 nicht.
(=>
(and
(instance ?REP AsexualReproduction)
(result ?REP ?ORGANISM))
(not
(exists
(?PARENT1 ?PARENT2)
(and
(parent ?ORGANISM ?PARENT1)
(parent ?ORGANISM ?PARENT2)
(not
(equal ?PARENT1 ?PARENT2))))))
Wenn increase ist ein fall von Zunehmen und obj ist ein patient von increase , dann es gibt ein unit,quant1,quant2 der ""obj unit(s)" ist gleich quant1 " hält während "direkt vor "die zeit des Bestehens von increase"" und ""obj unit(s)" ist gleich quant2 " hält während "sofort nach "die zeit des Bestehens von increase"" und quant2 ist grösserAls 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))))
Wenn heat ist ein fall von Erhitzen und obj ist ein patient von heat , dann es gibt ein Temperaturmass unit,quant1,quant2 der ""obj unit(s)" ist gleich quant1 " hält während "direkt vor "die zeit des Bestehens von heat"" und ""obj unit(s)" ist gleich quant2 " hält während "sofort nach "die zeit des Bestehens von heat"" und quant2 ist grösserAls 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))))
Wenn decrease ist ein fall von Abnehmen und obj ist ein patient von decrease , dann es gibt ein unit,quant1,quant2 der ""obj unit(s)" ist gleich quant1 " hält während "direkt vor "die zeit des Bestehens von decrease"" und ""obj unit(s)" ist gleich quant2 " hält während "sofort nach "die zeit des Bestehens von decrease"" und quant2 ist kleinerAls 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))))
Wenn cool ist ein fall von Abkühlen und obj ist ein patient von cool , dann es gibt ein Temperaturmass unit,quant1,quant2 der ""obj unit(s)" ist gleich quant1 " hält während "direkt vor "die zeit des Bestehens von cool"" und ""obj unit(s)" ist gleich quant2 " hält während "sofort nach "die zeit des Bestehens von cool"" und quant2 ist kleinerAls 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))))
Wenn transfer ist ein fall von Übertragung und transfer ist der agent von agent und patient ist ein patient von transfer , dann agent ist gleich patient nicht.
(=>
(and
(instance ?TRANSFER Transfer)
(agent ?TRANSFER ?AGENT)
(patient ?TRANSFER ?PATIENT))
(not
(equal ?AGENT ?PATIENT)))
Wenn sub ist ein fall von Ersetzen , dann es gibt ein Setzen put,Entfernen remove,obj1,obj2,place der put ist ein subProzess von sub und remove ist ein subProzess von sub und obj1 ist ein patient von remove und remove beginnet an place und obj2 ist ein patient von put und put endet an place und obj1 ist gleich obj2 nicht.
(=>
(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)))))
Wenn change ist ein fall von Änderung des Besitzes und obj ist ein patient von change und "agent1 besitzt obj " hält während "direkt vor "die zeit des Bestehens von change"" und "agent2 besitzt obj " hält während "sofort nach "die zeit des Bestehens von change"" , dann agent1 ist gleich agent2 nicht.
(=>
(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)))
Wenn trans ist ein fall von Transaktion , dann es gibt ein agent1,agent2,Geben give1,Geben give2,obj1,obj2 der give1 ist ein subProzess von trans und give2 ist ein subProzess von trans und give1 ist der agent von agent1 und give2 ist der agent von agent2 und obj1 ist ein patient von give1 und obj2 ist ein patient von give2 und give1 endet an agent2 und give2 endet an agent1 und agent1 ist gleich agent2 nicht und obj1 ist gleich obj2 nicht.
(=>
(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)))))
Wenn count ist ein fall von Zählen und count ist der agent von agent und entity ist ein patient von count , dann es gibt ein number der agent kennt ""die Zahl Fällen in entity" ist gleich number " .
(=>
(and
(instance ?COUNT Counting)
(agent ?COUNT ?AGENT)
(patient ?COUNT ?ENTITY))
(exists
(?NUMBER)
(knows
?AGENT
(equal
(CardinalityFn ?ENTITY)
?NUMBER))))
compound ist ein fall von Verbindung nur wenn es gibt ein elementare Substanz element1,elementare Substanz element2,chemische Synthese process der element1 ist gleich element2 nicht und element1 ist ein hilfmittel für process und element2 ist ein hilfmittel für process und compound ist ein resultat von 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))))
Wenn interaction ist ein fall von Sozialunterhaltung , dann es gibt ein agent1,agent2 der interaction ist der agent von agent1 und interaction ist der agent von agent2 und agent1 ist gleich agent2 nicht.
(=>
(instance ?INTERACTION SocialInteraction)
(exists
(?AGENT1 ?AGENT2)
(and
(agent ?INTERACTION ?AGENT1)
(agent ?INTERACTION ?AGENT2)
(not
(equal ?AGENT1 ?AGENT2)))))
Wenn disseminate ist ein fall von Verbreitung , dann es gibt ein kognitiver Agent agent1,kognitiver Agent agent2 der disseminate endet an agent1 und disseminate endet an agent2 und agent1 ist gleich agent2 nicht.
(=>
(instance ?DISSEMINATE Disseminating)
(exists
(?AGENT1 ?AGENT2)
(and
(destination ?DISSEMINATE ?AGENT1)
(instance ?AGENT1 CognitiveAgent)
(destination ?DISSEMINATE ?AGENT2)
(instance ?AGENT2 CognitiveAgent)
(not
(equal ?AGENT1 ?AGENT2)))))
Wenn contest ist ein fall von Kampf , dann es gibt ein agent1,agent2,purp1,purp2 der contest ist der agent von agent1 und contest ist der agent von agent2 und contest hat Zweck von purp1 für agent1 und contest hat Zweck von purp2 für agent2 und agent1 ist gleich agent2 nicht und purp1 ist gleich purp2 nicht.
(=>
(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)))))
Wenn process ist ein fall von Zustandänderung und obj ist ein patient von process , dann es gibt ein part,körperliche Zustand state1,körperliche Zustand state2 der part ist ein teil von obj und state1 ist gleich state2 nicht und "state1 ist ein attribut von part " hält während "direkt vor "die zeit des Bestehens von process"" und "state2 ist ein attribut von part " hält während "sofort nach "die zeit des Bestehens von 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)))))
Wenn area ist ein fall von Wassergebiet , dann es gibt ein bed,hole,Wasser water der "der wirt von dem Loch hole" ist gleich bed und water füllt hole richtig und "die vereinigung von den teilen von bed und water" ist gleich area .
(=>
(instance ?AREA WaterArea)
(exists
(?BED ?HOLE ?WATER)
(and
(equal
(PrincipalHostFn ?HOLE)
?BED)
(instance ?WATER Water)
(properlyFills ?WATER ?HOLE)
(equal
(MereologicalSumFn ?BED ?WATER)
?AREA))))
"die Zahl Fällen in Kontinent" ist gleich .
(equal
(CardinalityFn Continent)
7)
- wenn bacterium ist ein fall von Bakterium ,
- dann es gibt ein Zelle cell1 der cell1 ist ein bestandteil von bacterium und für jeden cell2 gilt: wenn cell2 ist ein bestandteil von bacterium und cell2 ist ein fall von Zelle , dann cell1 ist gleich cell2
.
(=>
(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))))))
Wenn junct ist ein fall von Körperverzweigung , dann es gibt ein Körperteil struct1,Körperteil struct2 der junct wird an struct1 angeschlossen und junct wird an struct2 angeschlossen und struct1 ist gleich struct2 nicht.
(=>
(instance ?JUNCT BodyJunction)
(exists
(?STRUCT1 ?STRUCT2)
(and
(connected ?JUNCT ?STRUCT1)
(connected ?JUNCT ?STRUCT2)
(instance ?STRUCT1 BodyPart)
(instance ?STRUCT2 BodyPart)
(not
(equal ?STRUCT1 ?STRUCT2)))))
Wenn morph ist ein fall von Morphem , dann es gibt kein Morphem othermorph der othermorph ist ein teil von morph und othermorph ist gleich morph nicht.
(=>
(instance ?MORPH Morpheme)
(not
(exists
(?OTHERMORPH)
(and
(instance ?OTHERMORPH Morpheme)
(part ?OTHERMORPH ?MORPH)
(not
(equal ?OTHERMORPH ?MORPH))))))
Wenn phrase ist ein fall von Phrase , dann es gibt ein Wort part1,Wort part2 der part1 ist ein teil von phrase und part2 ist ein teil von phrase und part1 ist gleich part2 nicht.
(=>
(instance ?PHRASE Phrase)
(exists
(?PART1 ?PART2)
(and
(part ?PART1 ?PHRASE)
(part ?PART2 ?PHRASE)
(instance ?PART1 Word)
(instance ?PART2 Word)
(not
(equal ?PART1 ?PART2)))))
Wenn "ausgabe int1 von text" ist gleich edition1 und "ausgabe int2 von text" ist gleich edition2 und int2 ist grösserAls int1 und pub1 ist ein fall von Publikation und pub2 ist ein fall von Publikation und edition1 ist ein patient von pub1 und edition2 ist ein patient von pub2 und datum von pub1 ist date1 und datum von pub2 ist date2 , dann "das ende von date1" geschieht vor "das ende von 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)))
Wenn "ausgabe number von text1" ist gleich text2 , dann text1 fasst das Inhalt von text2 zusammen.
(=>
(equal
(EditionFn ?TEXT1 ?NUMBER)
?TEXT2)
(subsumesContentClass ?TEXT1 ?TEXT2))
Wenn text ist eine teilkategorie von Zeitschrift und "Band int1 in der reihe text" ist gleich volume1 und "Band int2 in der reihe text" ist gleich volume2 und int2 ist grösserAls int1 und pub1 ist ein fall von Publikation und pub2 ist ein fall von Publikation und volume1 ist ein patient von pub1 und volume2 ist ein patient von pub2 und datum von pub1 ist date1 und datum von pub2 ist date2 , dann "das ende von date1" geschieht vor "das ende von 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)))
Wenn "Band number in der reihe series" ist gleich volume , dann series fasst das Inhalt von volume zusammen.
(=>
(equal
(SeriesVolumeFn ?SERIES ?NUMBER)
?VOLUME)
(subsumesContentClass ?SERIES ?VOLUME))
Wenn "die Zahl von periodikum number von periodical" ist gleich issue , dann periodical fasst das Inhalt von issue zusammen.
(=>
(equal
(PeriodicalIssueFn ?PERIODICAL ?NUMBER)
?ISSUE)
(subsumesContentClass ?PERIODICAL ?ISSUE))
Wenn series ist ein fall von Reihe , dann es gibt ein Buch book1,Buch book2 der series fasst das Inhalt von book1 zusammen und series fasst das Inhalt von book2 zusammen und book1 ist gleich book2 nicht.
(=>
(instance ?SERIES Series)
(exists
(?BOOK1 ?BOOK2)
(and
(instance ?BOOK1 Book)
(instance ?BOOK2 Book)
(subsumesContentInstance ?SERIES ?BOOK1)
(subsumesContentInstance ?SERIES ?BOOK2)
(not
(equal ?BOOK1 ?BOOK2)))))
Wenn mole ist ein fall von Molekül , dann es gibt ein Atom atom1,Atom atom2 der atom1 ist ein teil von mole und atom2 ist ein teil von mole und atom1 ist gleich atom2 nicht.
(=>
(instance ?MOLE Molecule)
(exists
(?ATOM1 ?ATOM2)
(and
(instance ?ATOM1 Atom)
(instance ?ATOM2 Atom)
(part ?ATOM1 ?MOLE)
(part ?ATOM2 ?MOLE)
(not
(equal ?ATOM1 ?ATOM2)))))
- wenn artifact ist ein fall von feststehendes Kunstprodukt ,
- dann es gibt ein place der für jeden time gilt: wenn time geschieht vor oder gleichzeitig mit "das ende von "die zeit des Bestehens von artifact"" und "der anfang von "die zeit des Bestehens von artifact"" geschieht vor oder gleichzeitig mit time , dann "die Stelle wo artifact an time war" ist gleich place
.
(=>
(instance ?ARTIFACT StationaryArtifact)
(exists
(?PLACE)
(forall
(?TIME)
(=>
(and
(beforeOrEqual
?TIME
(EndFn
(WhenFn ?ARTIFACT)))
(beforeOrEqual
(BeginFn
(WhenFn ?ARTIFACT))
?TIME))
(equal
(WhereFn ?ARTIFACT ?TIME)
?PLACE)))))
- wenn group ist ein fall von Altersklasse ,
- dann für jeden memb1,memb2,age1,age2 gilt: wenn memb1 ist ein Mitglied von group und memb2 ist ein Mitglied von group und das alter von memb1 ist age1 und das alter von memb2 ist age2 , dann age1 ist gleich 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))))
Wenn "die zugelassene organisatorishe Gruppe von unit" ist gleich org und attr ist ein fall von normatives Attribut , dann attr ist ein attribut von unit nur wenn attr ist ein attribut von org .
(=>
(and
(equal
(OrganizationFn ?UNIT)
?ORG)
(instance ?ATTR NormativeAttribute))
(<=>
(attribute ?UNIT ?ATTR)
(attribute ?ORG ?ATTR)))
Wenn obj1 ist attr1 hinsichlich obj2 und wird ? entgegengesetzet und attr1 ist ein Mitglied von "()" und attr2 ist ein Mitglied von "()" und attr1 ist gleich attr2 nicht, dann obj1 ist attr2 hinsichlich obj2 nicht.
(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(contraryAttribute @ROW)
(inList
?ATTR1
(ListFn @ROW))
(inList
?ATTR2
(ListFn @ROW))
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))
- wenn "Wesen bei proc bewegen attr1" hält während time ,
- dann für jeden attr2 gilt: wenn "Wesen bei proc bewegen attr2" hält während time , dann attr2 ist gleich attr1
.
(=>
(holdsDuring
?TIME
(direction ?PROC ?ATTR1))
(forall
(?ATTR2)
(=>
(holdsDuring
?TIME
(direction ?PROC ?ATTR2))
(equal ?ATTR2 ?ATTR1))))
- wenn "proc stellet attr1 gegenüber" hält während time ,
- dann für jeden attr2 gilt: wenn "proc stellet attr2 gegenüber" hält während time , dann attr2 ist gleich attr1
.
(=>
(holdsDuring
?TIME
(faces ?PROC ?ATTR1))
(forall
(?ATTR2)
(=>
(holdsDuring
?TIME
(faces ?PROC ?ATTR2))
(equal ?ATTR2 ?ATTR1))))
Wenn obj1 ist attr1 hinsichlich obj2 und attr1 ist ein fall von Richtungsattribut und attr2 ist ein fall von Richtungsattribut und attr1 ist gleich attr2 nicht, dann obj1 ist attr2 hinsichlich obj2 nicht.
(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(instance ?ATTR1 DirectionalAttribute)
(instance ?ATTR2 DirectionalAttribute)
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))
Wenn "" ist gleich time2 , dann time2 ist gleich "(time1+)" .
(=>
(equal
(RelativeTimeFn ?TIME1 PacificTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 8)))
Wenn "" ist gleich time2 , dann time2 ist gleich "(time1+)" .
(=>
(equal
(RelativeTimeFn ?TIME1 MountainTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 7)))
Wenn "" ist gleich time2 , dann time2 ist gleich "(time1+)" .
(=>
(equal
(RelativeTimeFn ?TIME1 CentralTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 6)))
Wenn "" ist gleich time2 , dann time2 ist gleich "(time1+)" .
(=>
(equal
(RelativeTimeFn ?TIME1 EasternTimeZone)
?TIME2)
(equal
?TIME2
(AdditionFn ?TIME1 5)))
Wenn polychromatic ist ein attribut von obj , dann es gibt ein part1,part2,Farbeattribut color1,Farbeattribut color2 der part1 ist ein oberflächliches teil von obj und part2 ist ein oberflächliches teil von obj und color1 ist ein attribut von part1 und color2 ist ein attribut von part2 und color1 ist gleich color2 nicht.
(=>
(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)))))
Wenn class1 ist ein fall von Menge oder Kategorie und class2 ist ein fall von Menge oder Kategorie , dann "der unterschied zwischen class1 und class2" ist gleich "der durchschnitt von class1 und "die ergänzung von class2"" .
(=>
(and
(instance ?CLASS1 SetOrClass)
(instance ?CLASS2 SetOrClass))
(equal
(RelativeComplementFn ?CLASS1 ?CLASS2)
(IntersectionFn
?CLASS1
(ComplementFn ?CLASS2))))
