forall (forall)
The universal quantifier of predicate logic.
Ontology
SUMO / STRUCTURAL-ONTOLOGYClass(es)
Coordinate term(s)
<=>
=>
and
hatZurFolge
exists
not
or
Type restrictions
forall(Liste, Formel)
Related WordNet synsets
See more related synsets on a separate page.
Axioms (114)
Wenn rel1 ist eine inverse von rel2 , dann für jeden inst1,inst2 gilt: rel1(inst1,inst2) gilt nur wenn rel2(inst2,inst1) gilt .
(=>
(inverse ?REL1 ?REL2)
(forall
(?INST1 ?INST2)
(<=>
(holds ?REL1 ?INST1 ?INST2)
(holds ?REL2 ?INST2 ?INST1))))
subclass ist eine teilkategorie von class nur wenn
(<=>
(subclass ?SUBCLASS ?CLASS)
(and
(instance ?SUBCLASS SetOrClass)
(instance ?CLASS SetOrClass)
(forall
(?INST)
(=>
(instance ?INST ?SUBCLASS)
(instance ?INST ?CLASS)))))
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 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)))))
class1 ist dijunkt von class2 nur wenn
(<=>
(disjoint ?CLASS1 ?CLASS2)
(and
(instance ?CLASS1 SetOrClass)
(instance ?CLASS2 SetOrClass)
(forall
(?INST)
(not
(and
(instance ?INST ?CLASS1)
(instance ?INST ?CLASS2))))))
- 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))))))
(=>
(subAttribute ?ATTR1 ?ATTR2)
(forall
(?OBJ)
(=>
(property ?OBJ ?ATTR1)
(property ?OBJ ?ATTR2))))
- wenn substance1 ist ein stück von substance2 ,
- dann für jeden class gilt: wenn substance1 ist ein fall von class , dann substance2 ist ein fall von class
.
(=>
(piece ?SUBSTANCE1 ?SUBSTANCE2)
(forall
(?CLASS)
(=>
(instance ?SUBSTANCE1 ?CLASS)
(instance ?SUBSTANCE2 ?CLASS))))
- 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))))
coll1 ist eine korrekte teilsammlung von coll2 nur wenn
(<=>
(subCollection ?COLL1 ?COLL2)
(and
(instance ?COLL1 Collection)
(instance ?COLL2 Collection)
(forall
(?MEMBER)
(=>
(member ?MEMBER ?COLL1)
(member ?MEMBER ?COLL2)))))
"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))))
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 irreflexive Relation , dann für jeden inst gilt: rel(inst,inst) gilt nicht.
(=>
(instance ?REL IrreflexiveRelation)
(forall
(?INST)
(not
(holds ?REL ?INST ?INST))))
- wenn rel ist ein fall von symmetrische Relation ,
- dann für jeden inst1,inst2 gilt: wenn rel(inst1,inst2) gilt , dann rel(inst2,inst1) gilt
.
(=>
(instance ?REL SymmetricRelation)
(forall
(?INST1 ?INST2)
(=>
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST1))))
- 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 rel ist ein fall von transitive Relation ,
- dann für jeden inst1,inst2,inst3 gilt: wenn rel(inst1,inst2) gilt und rel(inst2,inst3) gilt , dann rel(inst1,inst3) gilt
.
(=>
(instance ?REL TransitiveRelation)
(forall
(?INST1 ?INST2 ?INST3)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST3))
(holds ?REL ?INST1 ?INST3))))
- wenn rel ist ein fall von intransitive Relation ,
- dann für jeden inst1,inst2,inst3 gilt: wenn rel(inst1,inst2) gilt und rel(inst2,inst3) gilt , dann rel(inst1,inst3) gilt nicht
.
(=>
(instance ?REL IntransitiveRelation)
(forall
(?INST1 ?INST2 ?INST3)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST3))
(not
(holds ?REL ?INST1 ?INST3)))))
Wenn rel ist ein fall von Totalordnungsrelation , dann für jeden inst1,inst2 gilt: rel(inst1,inst2) gilt oder rel(inst2,inst1) gilt .
(=>
(instance ?REL TotalOrderingRelation)
(forall
(?INST1 ?INST2)
(or
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST1))))
- 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))))
- wenn class wird mit behandelt,
- dann für jeden obj gilt: wenn obj ist ein fall von class , dann es gibt ein item der item ist ein Mitglied von "()" und obj ist ein fall von item
.
(=>
(exhaustiveDecomposition ?CLASS @ROW)
(forall
(?OBJ)
(=>
(instance ?OBJ ?CLASS)
(exists
(?ITEM)
(and
(inList
?ITEM
(ListFn @ROW))
(instance ?OBJ ?ITEM))))))
- wenn class wird zusammenhanglos auf disjunkt,
- dann für jeden item gilt: wenn item ist ein Mitglied von "()", dann item ist eine teilkategorie von class
.
(=>
(disjointDecomposition ?CLASS @ROW)
(forall
(?ITEM)
(=>
(inList
?ITEM
(ListFn @ROW))
(subclass ?ITEM ?CLASS))))
- 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))))
- 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))))
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))))))
- wenn list1 ist eine teilliste von list2 ,
- dann für jeden item gilt: wenn item ist ein Mitglied von list1, dann item ist ein Mitglied von list2
.
(=>
(subList ?LIST1 ?LIST2)
(forall
(?ITEM)
(=>
(inList ?ITEM ?LIST1)
(inList ?ITEM ?LIST2))))
- 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 function ist mit class aufgeschlossen und function ist ein fall von einstellige Funktion ,
- dann für jeden inst gilt: wenn inst ist ein fall von class , dann "function(inst)" ist ein fall von class
.
(=>
(and
(closedOn ?FUNCTION ?CLASS)
(instance ?FUNCTION UnaryFunction))
(forall
(?INST)
(=>
(instance ?INST ?CLASS)
(instance
(AssignmentFn ?FUNCTION ?INST)
?CLASS))))
- wenn function ist mit class aufgeschlossen und function ist ein fall von zweistellige Funktion ,
- dann für jeden inst1,inst2 gilt: wenn inst1 ist ein fall von class und inst2 ist ein fall von class , dann "function(inst1,inst2)" ist ein fall von class
.
(=>
(and
(closedOn ?FUNCTION ?CLASS)
(instance ?FUNCTION BinaryFunction))
(forall
(?INST1 ?INST2)
(=>
(and
(instance ?INST1 ?CLASS)
(instance ?INST2 ?CLASS))
(instance
(AssignmentFn ?FUNCTION ?INST1 ?INST2)
?CLASS))))
- wenn relation ist auf class reflexiv ,
- dann für jeden inst gilt: wenn inst ist ein fall von class , dann relation(inst,inst) gilt
.
(=>
(reflexiveOn ?RELATION ?CLASS)
(forall
(?INST)
(=>
(instance ?INST ?CLASS)
(holds ?RELATION ?INST ?INST))))
- wenn relation ist irreflexiv auf class ,
- dann für jeden inst gilt: wenn inst ist ein fall von class , dann relation(inst,inst) gilt nicht
.
(=>
(irreflexiveOn ?RELATION ?CLASS)
(forall
(?INST)
(=>
(instance ?INST ?CLASS)
(not
(holds ?RELATION ?INST ?INST)))))
- 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 causes subclass(proc1,proc2) gilt,
- dann für jeden inst2 gilt: wenn inst2 ist ein fall von proc2 , dann es gibt ein proc1 inst1 der inst1 verursacht inst2
.
(=>
(causesSubclass ?PROC1 ?PROC2)
(forall
(?INST2)
(=>
(instance ?INST2 ?PROC2)
(exists
(?INST1)
(and
(instance ?INST1 ?PROC1)
(causes ?INST1 ?INST2))))))
- wenn obj1 ist eine genaue kopie von obj2,
- dann für jeden attr gilt: wenn attr ist ein attribut von obj1 , dann attr ist ein attribut von obj2
.
(=>
(copy ?OBJ1 ?OBJ2)
(forall
(?ATTR)
(=>
(attribute ?OBJ1 ?ATTR)
(attribute ?OBJ2 ?ATTR))))
- wenn obj befindet sich an ,
- dann für jeden subobj gilt: wenn subobj ist ein teil von obj , dann subobj befindet sich an
.
(=>
(located ?OBJ ?REGION)
(forall
(?SUBOBJ)
(=>
(part ?SUBOBJ ?OBJ)
(located ?SUBOBJ ?REGION))))
- wenn person besitzt obj ,
- dann es gibt ein type der type hat das Recht, person durchzuführen und für jeden process gilt: wenn process ist ein fall von type , dann obj ist ein patient von process
.
(=>
(possesses ?PERSON ?OBJ)
(exists
(?TYPE)
(and
(holdsRight ?PERSON ?TYPE)
(forall
(?PROCESS)
(=>
(instance ?PROCESS ?TYPE)
(patient ?PROCESS ?OBJ))))))
Wenn proc1 hemmt proc2, dann für jeden time,place gilt: ""es gibt ein proc1 inst1 der inst1 befindet sich an " hält während time " verringert die Wahrscheinlichkeit von ""es gibt ein proc2 inst2 der inst2 befindet sich an " hält während time " .
(=>
(inhibits ?PROC1 ?PROC2)
(forall
(?TIME ?PLACE)
(decreasesLikelihood
(holdsDuring
?TIME
(exists
(?INST1)
(and
(instance ?INST1 ?PROC1)
(located ?INST1 ?PLACE))))
(holdsDuring
?TIME
(exists
(?INST2)
(and
(instance ?INST2 ?PROC2)
(located ?INST2 ?PLACE)))))))
- wenn proc1 verhindert das Auftreten von proc2,
- dann für jeden time,place gilt: wenn "es gibt ein proc1 inst1 der inst1 befindet sich an " hält während time , dann "es gibt ein proc2 inst2 der inst2 befindet sich an " hält während time nicht
.
(=>
(prevents ?PROC1 ?PROC2)
(forall
(?TIME ?PLACE)
(=>
(holdsDuring
?TIME
(exists
(?INST1)
(and
(instance ?INST1 ?PROC1)
(located ?INST1 ?PLACE))))
(not
(holdsDuring
?TIME
(exists
(?INST2)
(and
(instance ?INST2 ?PROC2)
(located ?INST2 ?PLACE))))))))
class1 fasst das Inhalt von class2 zusammen nur wenn für jeden obj2,info gilt: wenn obj2 ist ein fall von class2 und obj2 enthält Informationen über info, dann es gibt ein class1 obj1 der obj1 enthält Informationen über info.
(<=>
(subsumesContentClass ?CLASS1 ?CLASS2)
(forall
(?OBJ2 ?INFO)
(=>
(and
(instance ?OBJ2 ?CLASS2)
(containsInformation ?OBJ2 ?INFO))
(exists
(?OBJ1)
(and
(instance ?OBJ1 ?CLASS1)
(containsInformation ?OBJ1 ?INFO))))))
obj1 fasst das Inhalt von obj2 zusammen nur wenn für jeden info gilt: wenn obj2 enthält Informationen über info, dann obj1 enthält Informationen über info.
(<=>
(subsumesContentInstance ?OBJ1 ?OBJ2)
(forall
(?INFO)
(=>
(containsInformation ?OBJ2 ?INFO)
(containsInformation ?OBJ1 ?INFO))))
- wenn prop1 ist eine teilangelegenheit von prop2 ,
- dann für jeden obj1,obj2 gilt: wenn obj1 enthält Informationen über prop1 und obj2 enthält Informationen über prop2, dann obj2 fasst das Inhalt von obj1 zusammen
.
(=>
(subProposition ?PROP1 ?PROP2)
(forall
(?OBJ1 ?OBJ2)
(=>
(and
(containsInformation ?OBJ1 ?PROP1)
(containsInformation ?OBJ2 ?PROP2))
(subsumesContentInstance ?OBJ2 ?OBJ1))))
- 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 "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 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 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 subset ist eine teilmenge von set ,
- dann für jeden element gilt: wenn element ist ein element von subset , dann element ist ein element von set
.
(=>
(subset ?SUBSET ?SET)
(forall
(?ELEMENT)
(=>
(element ?ELEMENT ?SUBSET)
(element ?ELEMENT ?SET))))
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 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)))))
(=>
(instance ?CLASS MutuallyDisjointClass)
(forall
(?INST1 ?INST2)
(=>
(and
(instance ?INST1 ?CLASS)
(instance ?INST2 ?INST1))
(exists
(?INST3)
(and
(instance ?INST3 ?CLASS)
(not
(instance ?INST2 ?INST3)))))))
- 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 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 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 "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)))))
(=>
(and
(instance ?REL RelationExtendedToQuantities)
(instance ?REL TernaryRelation)
(instance ?NUMBER1 RealNumber)
(instance ?NUMBER2 RealNumber)
(holds ?REL ?NUMBER1 ?NUMBER2 ?VALUE))
(forall
(?UNIT)
(=>
(instance ?UNIT UnitOfMeasure)
(holds
?REL
(MeasureFn ?NUMBER1 ?UNIT)
(MeasureFn ?NUMBER2 ?UNIT)
(MeasureFn ?VALUE ?UNIT)))))
(=>
(and
(instance ?REL RelationExtendedToQuantities)
(instance ?REL BinaryRelation)
(instance ?NUMBER1 RealNumber)
(instance ?NUMBER2 RealNumber)
(holds ?REL ?NUMBER1 ?NUMBER2))
(forall
(?UNIT)
(=>
(instance ?UNIT UnitOfMeasure)
(holds
?REL
(MeasureFn ?NUMBER1 ?UNIT)
(MeasureFn ?NUMBER2 ?UNIT)))))
(=>
(larger ?OBJ1 ?OBJ2)
(forall
(?QUANT1 ?QUANT2)
(=>
(and
(measure
?OBJ1
(MeasureFn ?QUANT1 LengthMeasure))
(measure
?OBJ2
(MeasureFn ?QUANT2 LengthMeasure)))
(greaterThan ?QUANT1 ?QUANT2))))
- wenn proc gescheit alle time1,
- dann für jeden time2 gilt: wenn dauer von time2 ist time1 , dann es gibt ein position der position ist ein teil von time2 und "es gibt ein inst der inst ist ein fall von proc " hält während position
.
(=>
(frequency ?PROC ?TIME1)
(forall
(?TIME2)
(=>
(duration ?TIME2 ?TIME1)
(exists
(?POSITION)
(and
(temporalPart ?POSITION ?TIME2)
(holdsDuring
?POSITION
(exists
(?INST)
(instance ?INST ?PROC))))))))
- 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))))
- wenn obj ist ein fall von Gegenstand ,
- dann es gibt ein Zeitpunkt time1,Zeitpunkt time2 der time1 geschieht vor time2 und für jeden time gilt: wenn time1 geschieht vor oder gleichzeitig mit time und time geschieht vor oder gleichzeitig mit time2 , dann obj besteht während time
.
(=>
(instance ?OBJ Object)
(exists
(?TIME1 ?TIME2)
(and
(instance ?TIME1 TimePoint)
(instance ?TIME2 TimePoint)
(before ?TIME1 ?TIME2)
(forall
(?TIME)
(=>
(and
(beforeOrEqual ?TIME1 ?TIME)
(beforeOrEqual ?TIME ?TIME2))
(time ?OBJ ?TIME))))))
- wenn obj ist ein resultat von proc ,
- dann für jeden time gilt: wenn time geschieht vor "der anfang von "die zeit des Bestehens von proc"" , dann obj besteht während time nicht
.
(=>
(result ?PROC ?OBJ)
(forall
(?TIME)
(=>
(before
?TIME
(BeginFn
(WhenFn ?PROC)))
(not
(time ?OBJ ?TIME)))))
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 "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 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))))))
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 eine fläche von obj2 ,
- dann für jeden obj3 gilt: wenn obj3 ist ein oberflächliches teil von obj2 , dann obj3 ist ein teil von obj1
.
(=>
(surface ?OBJ1 ?OBJ2)
(forall
(?OBJ3)
(=>
(superficialPart ?OBJ3 ?OBJ2)
(part ?OBJ3 ?OBJ1))))
- wenn obj1 ist ein innenteil von obj2 ,
- dann für jeden part gilt: wenn part ist ein oberflächliches teil von obj2 , dann obj1 deckt sich mit part räumlich nicht
.
(=>
(interiorPart ?OBJ1 ?OBJ2)
(forall
(?PART)
(=>
(superficialPart ?PART ?OBJ2)
(not
(overlapsSpatially ?OBJ1 ?PART)))))
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 hole1 ist ein loch in obj und hole2 ist ein loch in obj ,
- dann für jeden hole3 gilt: wenn hole3 ist ein teil von "die vereinigung von den teilen von hole1 und hole2" , dann hole3 ist ein loch in obj
.
(=>
(and
(hole ?HOLE1 ?OBJ)
(hole ?HOLE2 ?OBJ))
(forall
(?HOLE3)
(=>
(part
?HOLE3
(MereologicalSumFn ?HOLE1 ?HOLE2))
(hole ?HOLE3 ?OBJ))))
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 füllt hole vollständig,
- dann für jeden obj2 gilt: wenn obj2 wird an hole angeschlossen, dann obj2 wird an obj1 angeschlossen
.
(=>
(completelyFills ?OBJ1 ?HOLE)
(forall
(?OBJ2)
(=>
(connected ?OBJ2 ?HOLE)
(connected ?OBJ2 ?OBJ1))))
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 für jeden region gilt: wenn proc befindet sich an , dann subproc befindet sich an
.
(=>
(subProcess ?SUBPROC ?PROC)
(forall
(?REGION)
(=>
(located ?PROC ?REGION)
(located ?SUBPROC ?REGION))))
- wenn
- path1 ist der pfad entlang dem process geschieht
und - process beginnet an source
und - process endet an dest
und - die länge von path1 ist measure1
und - es gibt kein path2,measure2 der path2 ist der pfad entlang dem process geschieht und process beginnet an origin und process endet an dest und die länge von path2 ist measure2 und measure2 ist kleinerAls measure1
, - dann für jeden obj gilt: wenn obj ist ein teil von path1 , dann obj ist zwischen source und dest
.
(=>
(and
(path ?PROCESS ?PATH1)
(origin ?PROCESS ?SOURCE)
(destination ?PROCESS ?DEST)
(length ?PATH1 ?MEASURE1)
(not
(exists
(?PATH2 ?MEASURE2)
(and
(path ?PROCESS ?PATH2)
(origin ?PROCESS ?ORIGIN)
(destination ?PROCESS ?DEST)
(length ?PATH2 ?MEASURE2)
(lessThan ?MEASURE2 ?MEASURE1)))))
(forall
(?OBJ)
(=>
(part ?OBJ ?PATH1)
(between ?SOURCE ?OBJ ?DEST))))
- wenn keep ist ein fall von Halten und obj ist ein patient von keep ,
- dann es gibt ein place der für jeden time gilt: wenn time ist ein teil von "die zeit des Bestehens von keep" , dann "obj befindet sich an " hält während time
.
(=>
(and
(instance ?KEEP Keeping)
(patient ?KEEP ?OBJ))
(exists
(?PLACE)
(forall
(?TIME)
(=>
(temporalPart
?TIME
(WhenFn ?KEEP))
(holdsDuring
?TIME
(located ?OBJ ?PLACE))))))
- wenn cooperate ist ein fall von Mitarbeit ,
- dann es gibt ein purp der für jeden agent gilt: wenn cooperate ist der agent von agent , dann cooperate hat Zweck von purp für agent
.
(=>
(instance ?COOPERATE Cooperation)
(exists
(?PURP)
(forall
(?AGENT)
(=>
(agent ?COOPERATE ?AGENT)
(hasPurposeForAgent ?COOPERATE ?PURP ?AGENT)))))
- wenn war ist ein fall von Krieg und war ist der agent von agent ,
- dann
.
(=>
(and
(instance ?WAR War)
(agent ?WAR ?AGENT))
(or
(instance ?AGENT Nation)
(and
(instance ?AGENT Organization)
(forall
(?MEMBER)
(=>
(member ?MEMBER ?AGENT)
(instance ?MEMBER Nation))))))
- 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 food ist ein fall von Nahrung ,
- dann für jeden part1 gilt: wenn part1 ist ein teil von food , dann es gibt ein part2,Tier animal der part1 ist ein teil von part2 und part2 ist ein teil von animal
.
(=>
(instance ?FOOD Food)
(forall
(?PART1)
(=>
(part ?PART1 ?FOOD)
(exists
(?PART2 ?ANIMAL)
(and
(part ?PART1 ?PART2)
(part ?PART2 ?ANIMAL)
(instance ?ANIMAL Animal))))))
- wenn meat ist ein fall von Fleisch ,
- dann für jeden part gilt: wenn part ist ein teil von meat , dann es gibt ein subpart,time,animal der subpart ist ein teil von part und "animal ist ein fall von Tier und subpart ist ein teil von animal " hält während time
.
(=>
(instance ?MEAT Meat)
(forall
(?PART)
(=>
(part ?PART ?MEAT)
(exists
(?SUBPART ?TIME ?ANIMAL)
(and
(part ?SUBPART ?PART)
(holdsDuring
?TIME
(and
(instance ?ANIMAL Animal)
(part ?SUBPART ?ANIMAL))))))))
- wenn veg ist ein fall von Frucht oder Gemüse ,
- dann für jeden part gilt: wenn part ist ein teil von veg , dann es gibt ein subpart,time,plant der subpart ist ein teil von part und "plant ist ein fall von Pflanze und subpart ist ein teil von plant " hält während time
.
(=>
(instance ?VEG FruitOrVegetable)
(forall
(?PART)
(=>
(part ?PART ?VEG)
(exists
(?SUBPART ?TIME ?PLANT)
(and
(part ?SUBPART ?PART)
(holdsDuring
?TIME
(and
(instance ?PLANT Plant)
(part ?SUBPART ?PLANT))))))))
- 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 machine ist ein fall von Maschine ,
- dann für jeden proc gilt: wenn machine ist ein instrument für proc , dann es gibt ein resource,result der resource ist ein hilfmittel für proc und result ist ein resultat von proc
.
(=>
(instance ?MACHINE Machine)
(forall
(?PROC)
(=>
(instrument ?PROC ?MACHINE)
(exists
(?RESOURCE ?RESULT)
(and
(resource ?PROC ?RESOURCE)
(result ?PROC ?RESULT))))))
- 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))))
(=>
(instance ?GROUP FamilyGroup)
(forall
(?MEMB1 ?MEMB2)
(=>
(and
(member ?MEMB1 ?GROUP)
(member ?MEMB2 ?GROUP))
(familyRelation ?MEMB1 ?MEMB2))))
- 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))))
Für jeden org gilt: org beschäftigt person nicht und person ist ein fall von Mensch nur wenn unemployed ist ein attribut von person .
(<=>
(forall
(?ORG)
(and
(not
(employs ?ORG ?PERSON))
(instance ?PERSON Human)))
(attribute ?PERSON Unemployed))
(=>
(and
(attribute ?OBJ Monochromatic)
(superficialPart ?PART ?OBJ)
(attribute ?PART ?COLOR)
(instance ?COLOR PrimaryColor))
(forall
(?ELEMENT)
(=>
(superficialPart ?ELEMENT ?OBJ)
(attribute ?ELEMENT ?COLOR))))
- wenn wet ist ein attribut von obj ,
- dann für jeden part gilt: wenn part ist ein teil von obj , dann es gibt ein subpart der subpart ist ein teil von part und liquid ist ein attribut von subpart
.
(=>
(attribute ?OBJ Wet)
(forall
(?PART)
(=>
(part ?PART ?OBJ)
(exists
(?SUBPART)
(and
(part ?SUBPART ?PART)
(attribute ?SUBPART Liquid))))))
entity ist ein fall von "der durchschnitt aller Elementen von superclass" nur wenn für jeden class gilt: wenn class ist ein fall von superclass , dann entity ist ein fall von class .
(<=>
(instance
?ENTITY
(GeneralizedIntersectionFn ?SUPERCLASS))
(forall
(?CLASS)
(=>
(instance ?CLASS ?SUPERCLASS)
(instance ?ENTITY ?CLASS))))
