not (not)
The truth-functional connective of negation.
Ontologie
SUMO / STRUCTURAL-ONTOLOGYClass(es)
Související termín(y)
<=>
=>
and
entails
exists
forall
or
Typy argumentů
not(formule)
Related WordNet synsets
- negation
- the negative of the opposition
- not
- negation of a word or group of words; "he does not speak French"; "she is not going"; "they are not friends"; "not many"; "not much"; "not at all"
- no
- not in any degree or manner; not at all; "he is no better today"
See more related synsets on a separate page.
Axiomy (121)
Jestliže immediate instance(entity,class) platí, potom neexistuje class subclass tak, že entity je instancí třídy subclass.
(=>
(immediateInstance ?ENTITY ?CLASS)
(not
(exists
(?SUBCLASS)
(and
(subclass ?SUBCLASS ?CLASS)
(instance ?ENTITY ?SUBCLASS)))))
Jestliže immediate subclass(class1,class2) platí, potom neexistuje class2 class3 tak, že class1 je podtřídou class3 a class2 se nerovná class3 a class1 se nerovná class3.
(=>
(immediateSubclass ?CLASS1 ?CLASS2)
(not
(exists
(?CLASS3)
(and
(subclass ?CLASS3 ?CLASS2)
(subclass ?CLASS1 ?CLASS3)
(not
(equal ?CLASS2 ?CLASS3))
(not
(equal ?CLASS1 ?CLASS3))))))
class1 je disjoint from class2 tehdy a jen tehdy pokud
(<=>
(disjoint ?CLASS1 ?CLASS2)
(and
(instance ?CLASS1 SetOrClass)
(instance ?CLASS2 SetOrClass)
(forall
(?INST)
(not
(and
(instance ?INST ?CLASS1)
(instance ?INST ?CLASS2))))))
Jestliže and ? are disjoint a rel1 je a member of "()" a rel2 je a member of "()" a rel1 se nerovná rel2 a rel1() holds, potom rel2() doesn't hold.
(=>
(and
(disjointRelation @ROW1)
(inList
?REL1
(ListFn @ROW1))
(inList
?REL2
(ListFn @ROW1))
(not
(equal ?REL1 ?REL2))
(holds ?REL1 @ROW2))
(not
(holds ?REL2 @ROW2)))
(=>
(contraryAttribute @ROW)
(forall
(?ATTR1 ?ATTR2)
(=>
(and
(equal
?ATTR1
(ListOrderFn
(ListFn @ROW)
?NUMBER1))
(equal
?ATTR2
(ListOrderFn
(ListFn @ROW)
?NUMBER2))
(not
(equal ?NUMBER1 ?NUMBER2)))
(=>
(property ?OBJ ?ATTR1)
(not
(property ?OBJ ?ATTR2))))))
obj1 je vlastní částí obj2 tehdy a jen tehdy pokud obj1 je částí obj2 a obj2 není částí obj1.
(<=>
(properPart ?OBJ1 ?OBJ2)
(and
(part ?OBJ1 ?OBJ2)
(not
(part ?OBJ2 ?OBJ1))))
Jestliže mixture je instancí třídy směs, potom existují čistá látka pure1,čistá látka pure2 tak, že pure1 se nerovná pure2 a pure1 je a piece of mixture a pure2 je a piece of mixture.
(=>
(instance ?MIXTURE Mixture)
(exists
(?PURE1 ?PURE2)
(and
(subclass ?PURE1 PureSubstance)
(subclass ?PURE2 PureSubstance)
(not
(equal ?PURE1 ?PURE2))
(piece ?PURE1 ?MIXTURE)
(piece ?PURE2 ?MIXTURE))))
Jestliže obj je instancí třídy složený objekt, potom existují látka substance1,látka substance2 tak, že substance1 je z obj a substance2 je z obj a substance1 se nerovná substance2.
(=>
(instance ?OBJ CorpuscularObject)
(exists
(?SUBSTANCE1 ?SUBSTANCE2)
(and
(subclass ?SUBSTANCE1 Substance)
(subclass ?SUBSTANCE2 Substance)
(material ?SUBSTANCE1 ?OBJ)
(material ?SUBSTANCE2 ?OBJ)
(not
(equal ?SUBSTANCE1 ?SUBSTANCE2)))))
Jestliže lang je instancí třídy zvířecí jazyk a agent je původcem proc a lang je nástrojem for proc, potom agent je instancí třídy zvíře a agent není instancí třídy člověk.
(=>
(and
(instance ?LANG AnimalLanguage)
(agent ?PROC ?AGENT)
(instrument ?PROC ?LANG))
(and
(instance ?AGENT Animal)
(not
(instance ?AGENT Human))))
Jestliže process je instancí třídy proces nad dvěma objekty, potom existují obj1,obj2 tak, že obj1 je účastníkem process a obj2 je účastníkem process a obj1 se nerovná obj2.
(=>
(instance ?PROCESS DualObjectProcess)
(exists
(?OBJ1 ?OBJ2)
(and
(patient ?PROCESS ?OBJ1)
(patient ?PROCESS ?OBJ2)
(not
(equal ?OBJ1 ?OBJ2)))))
abs je instancí třídy abstraktum tehdy a jen tehdy pokud neexistuje point tak, že abs je located at point nebo abs exists during point.
(<=>
(instance ?ABS Abstract)
(not
(exists
(?POINT)
(or
(located ?ABS ?POINT)
(time ?ABS ?POINT)))))
Jestliže rel je instancí třídy binární relace, potom neexistují item1,item2,item3, tak, že rel(item1,item2,item3,) holds.
(=>
(instance ?REL BinaryRelation)
(not
(exists
(?ITEM1 ?ITEM2 ?ITEM3 @ROW)
(holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 @ROW))))
Jestliže rel je instancí třídy ireflexivní relace, potom pro všechny inst platí: rel(inst,inst) doesn't hold.
(=>
(instance ?REL IrreflexiveRelation)
(forall
(?INST)
(not
(holds ?REL ?INST ?INST))))
(=>
(instance ?REL IntransitiveRelation)
(forall
(?INST1 ?INST2 ?INST3)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST3))
(not
(holds ?REL ?INST1 ?INST3)))))
Jestliže rel je instancí třídy terciální relace, potom neexistují item1,item2,item3,item4, tak, že rel(item1,item2,item3,item4,) holds.
(=>
(instance ?REL TernaryRelation)
(not
(exists
(?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW)
(holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW))))
Jestliže rel je instancí třídy relace se čtyřmi argumenty, potom neexistují item1,item2,item3,item4,item5, tak, že rel(item1,item2,item3,item4,item5,) holds.
(=>
(instance ?REL QuaternaryRelation)
(not
(exists
(?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW)
(holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW))))
Jestliže rel je instancí třídy relace s pěti argumenty, potom neexistují item1,item2,item3,item4,item5,item6, tak, že rel(item1,item2,item3,item4,item5,item6,) holds.
(=>
(instance ?REL QuintaryRelation)
(not
(exists
(?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW)
(holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW))))
(=>
(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 se rovná null list tehdy a jen tehdy pokud neexistuje item tak, že item je a member of list.
(<=>
(equal ?LIST NullList)
(not
(exists
(?ITEM)
(inList ?ITEM ?LIST))))
- jestliže class je disjointly decomposed into ,
- potom pro všechny item1,item2 platí: jestliže item1 je a member of "()" a item2 je a member of "()" a item1 se nerovná item2, potom item1 je disjoint from item2
.
(=>
(disjointDecomposition ?CLASS @ROW)
(forall
(?ITEM1 ?ITEM2)
(=>
(and
(inList
?ITEM1
(ListFn @ROW))
(inList
?ITEM2
(ListFn @ROW))
(not
(equal ?ITEM1 ?ITEM2)))
(disjoint ?ITEM1 ?ITEM2))))
(=>
(instance ?FUN OneToOneFunction)
(forall
(?ARG1 ?ARG2)
(=>
(and
(domain ?FUN 1 ?CLASS)
(instance ?ARG1 ?CLASS)
(instance ?ARG2 ?CLASS)
(not
(equal ?ARG1 ?ARG2)))
(not
(equal
(AssignmentFn ?FUN ?ARG1)
(AssignmentFn ?FUN ?ARG2))))))
Jestliže rel je instancí třídy relace s proměnným počtem argumentů, potom neexistuje int tak, že rel has int argument(s).
(=>
(instance ?REL VariableArityRelation)
(not
(exists
(?INT)
(valence ?REL ?INT))))
- jestliže relation je irreflexive on class,
- potom pro všechny inst platí: jestliže inst je instancí třídy class, potom relation(inst,inst) doesn't hold
.
(=>
(irreflexiveOn ?RELATION ?CLASS)
(forall
(?INST)
(=>
(instance ?INST ?CLASS)
(not
(holds ?RELATION ?INST ?INST)))))
Jestliže situation během time, potom situation platí během time.
(=>
(holdsDuring
?TIME
(not ?SITUATION))
(not
(holdsDuring ?TIME ?SITUATION)))
Jestliže obj je přesně umístěn v region, potom neexistuje otherobj tak, že otherobj je přesně umístěn v region a otherobj se nerovná obj.
(=>
(exactlyLocated ?OBJ ?REGION)
(not
(exists
(?OTHEROBJ)
(and
(exactlyLocated ?OTHEROBJ ?REGION)
(not
(equal ?OTHEROBJ ?OBJ))))))
- jestliže prevents(proc1,proc2) platí,
- potom pro všechny time,place platí: jestliže existuje proc1 inst1 tak, že inst1 je located at place během time, potom existuje proc2 inst2 tak, že inst2 je located at place během time
.
(=>
(prevents ?PROC1 ?PROC2)
(forall
(?TIME ?PLACE)
(=>
(holdsDuring
?TIME
(exists
(?INST1)
(and
(instance ?INST1 ?PROC1)
(located ?INST1 ?PLACE))))
(not
(holdsDuring
?TIME
(exists
(?INST2)
(and
(instance ?INST2 ?PROC2)
(located ?INST2 ?PLACE))))))))
Jestliže "ceiling fn(number)" se rovná int, potom neexistuje celé číslo otherint tak, že otherint je větší než nebo roven number a otherint je menší než int.
(=>
(equal
(CeilingFn ?NUMBER)
?INT)
(not
(exists
(?OTHERINT)
(and
(instance ?OTHERINT Integer)
(greaterThanOrEqualTo ?OTHERINT ?NUMBER)
(lessThan ?OTHERINT ?INT)))))
Jestliže "floor fn(number)" se rovná int, potom neexistuje celé číslo otherint tak, že otherint je menší než nebo roven number a otherint je větší než int.
(=>
(equal
(FloorFn ?NUMBER)
?INT)
(not
(exists
(?OTHERINT)
(and
(instance ?OTHERINT Integer)
(lessThanOrEqualTo ?OTHERINT ?NUMBER)
(greaterThan ?OTHERINT ?INT)))))
(=>
(equal
(GreatestCommonDivisorFn @ROW)
?NUMBER)
(not
(exists
(?GREATER)
(and
(greaterThan ?GREATER ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?ELEMENT ?GREATER)
0)))))))
(=>
(equal
(LeastCommonMultipleFn @ROW)
?NUMBER)
(not
(exists
(?LESS)
(and
(lessThan ?LESS ?NUMBER)
(forall
(?ELEMENT)
(=>
(inList
?ELEMENT
(ListFn @ROW))
(equal
(RemainderFn ?LESS ?ELEMENT)
0)))))))
Jestliže int1 je instancí třídy celé číslo a int2 je instancí třídy celé číslo, potom int1 není menší než int2 nebo int2 není menší než "(int1+1)".
(=>
(and
(instance ?INT1 Integer)
(instance ?INT2 Integer))
(not
(and
(lessThan ?INT1 ?INT2)
(lessThan
?INT2
(SuccessorFn ?INT1)))))
Jestliže int1 je instancí třídy celé číslo a int2 je instancí třídy celé číslo, potom int2 není menší než int1 nebo "(int1+2)" není menší než int2.
(=>
(and
(instance ?INT1 Integer)
(instance ?INT2 Integer))
(not
(and
(lessThan ?INT2 ?INT1)
(lessThan
(PredecessorFn ?INT1)
?INT2))))
Neexistuje element tak, že element je an element of null set.
(not
(exists
(?ELEMENT)
(element ?ELEMENT NullSet)))
(=>
(instance ?CLASS MutuallyDisjointClass)
(forall
(?INST1 ?INST2)
(=>
(and
(instance ?INST1 ?CLASS)
(instance ?INST2 ?INST1))
(exists
(?INST3)
(and
(instance ?INST3 ?CLASS)
(not
(instance ?INST2 ?INST3)))))))
Jestliže graph je instancí třídy graf a node1 je instancí třídy uzel grafu a node2 je instancí třídy uzel grafu a node1 je částí graph a node2 je částí graph a node1 se nerovná node2, potom existují arc,path tak, že
(=>
(and
(instance ?GRAPH Graph)
(instance ?NODE1 GraphNode)
(instance ?NODE2 GraphNode)
(graphPart ?NODE1 ?GRAPH)
(graphPart ?NODE2 ?GRAPH)
(not
(equal ?NODE1 ?NODE2)))
(exists
(?ARC ?PATH)
(or
(links ?NODE1 ?NODE2 ?ARC)
(and
(subGraph ?PATH ?GRAPH)
(instance ?PATH GraphPath)
(or
(and
(equal
(BeginNodeFn ?PATH)
?NODE1)
(equal
(EndNodeFn ?PATH)
?NODE2))
(and
(equal
(BeginNodeFn ?PATH)
?NODE2)
(equal
(EndNodeFn ?PATH)
?NODE1)))))))
Jestliže graph je instancí třídy graf, potom existují node1,node2,node3,arc1,arc2 tak, že node1 je částí graph a node2 je částí graph a node3 je částí graph a arc1 je částí graph a arc2 je částí graph a node2 spojuje arc1 a node1 a node3 spojuje arc2 a node2 a node1 se nerovná node2 a node2 se nerovná node3 a node1 se nerovná node3 a arc1 se nerovná arc2.
(=>
(instance ?GRAPH Graph)
(exists
(?NODE1 ?NODE2 ?NODE3 ?ARC1 ?ARC2)
(and
(graphPart ?NODE1 ?GRAPH)
(graphPart ?NODE2 ?GRAPH)
(graphPart ?NODE3 ?GRAPH)
(graphPart ?ARC1 ?GRAPH)
(graphPart ?ARC2 ?GRAPH)
(links ?ARC1 ?NODE1 ?NODE2)
(links ?ARC2 ?NODE2 ?NODE3)
(not
(equal ?NODE1 ?NODE2))
(not
(equal ?NODE2 ?NODE3))
(not
(equal ?NODE1 ?NODE3))
(not
(equal ?ARC1 ?ARC2)))))
Jestliže graph je instancí třídy strom, potom neexistuje smyčka grafu loop tak, že loop je částí graph.
(=>
(instance ?GRAPH Tree)
(not
(exists
(?LOOP)
(and
(instance ?LOOP GraphLoop)
(graphPart ?LOOP ?GRAPH)))))
(=>
(and
(instance ?GRAPH GraphPath)
(instance ?ARC GraphArc)
(graphPart ?ARC ?GRAPH))
(=>
(equal
(InitialNodeFn ?ARC)
?NODE)
(not
(exists
(?OTHER)
(and
(equal
(InitialNodeFn ?OTHER)
?NODE)
(not
(equal ?OTHER ?ARC)))))))
(=>
(and
(instance ?GRAPH GraphPath)
(instance ?ARC GraphArc)
(graphPart ?ARC ?GRAPH))
(=>
(equal
(TerminalNodeFn ?ARC)
?NODE)
(not
(exists
(?OTHER)
(and
(equal
(TerminalNodeFn ?OTHER)
?NODE)
(not
(equal ?OTHER ?ARC)))))))
graph je instancí třídy multigraf tehdy a jen tehdy pokud existují arc1,arc2,node1,node2 tak, že arc1 je částí graph a arc2 je částí graph a node1 je částí graph a node2 je částí graph a arc1 spojuje node1 a node2 a arc2 spojuje node1 a node2 a arc1 se nerovná arc2.
(<=>
(instance ?GRAPH MultiGraph)
(exists
(?ARC1 ?ARC2 ?NODE1 ?NODE2)
(and
(graphPart ?ARC1 ?GRAPH)
(graphPart ?ARC2 ?GRAPH)
(graphPart ?NODE1 ?GRAPH)
(graphPart ?NODE2 ?GRAPH)
(links ?NODE1 ?NODE2 ?ARC1)
(links ?NODE1 ?NODE2 ?ARC2)
(not
(equal ?ARC1 ?ARC2)))))
Jestliže path je částí graph a graph není instancí třídy orientovaný graf, potom "graph path fn(node1,node2)" se rovná path tehdy a jen tehdy pokud "graph path fn(node2,node1)" se rovná path.
(=>
(and
(graphPart ?PATH ?GRAPH)
(not
(instance ?GRAPH DirectedGraph)))
(<=>
(equal
(GraphPathFn ?NODE1 ?NODE2)
?PATH)
(equal
(GraphPathFn ?NODE2 ?NODE1)
?PATH)))
Neexistují cut set fn(graph) path1,minimal cut set fn(graph) path2 tak, že délka path1 je number1 a délka path2 je number2 a number1 je menší než number2.
(not
(exists
(?PATH1 ?PATH2)
(and
(instance
?PATH1
(CutSetFn ?GRAPH))
(instance
?PATH2
(MinimalCutSetFn ?GRAPH))
(pathLength ?PATH1 ?NUMBER1)
(pathLength ?PATH2 ?NUMBER2)
(lessThan ?NUMBER1 ?NUMBER2))))
Jestliže point je instancí třídy okamžik a point se nerovná positive infinity, potom point happens before positive infinity.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT PositiveInfinity)))
(before ?POINT PositiveInfinity))
Jestliže point je instancí třídy okamžik a point se nerovná positive infinity, potom existuje otherpoint tak, že otherpoint je between point and positive infinity.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT PositiveInfinity)))
(exists
(?OTHERPOINT)
(temporallyBetween ?POINT ?OTHERPOINT PositiveInfinity)))
Jestliže point je instancí třídy okamžik a point se nerovná negative infinity, potom negative infinity happens before point.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT NegativeInfinity)))
(before NegativeInfinity ?POINT))
Jestliže point je instancí třídy okamžik a point se nerovná negative infinity, potom existuje otherpoint tak, že otherpoint je between negative infinity and point.
(=>
(and
(instance ?POINT TimePoint)
(not
(equal ?POINT NegativeInfinity)))
(exists
(?OTHERPOINT)
(temporallyBetween NegativeInfinity ?OTHERPOINT ?POINT)))
- jestliže "the beginning of interval" se rovná point,
- potom pro všechny otherpoint platí: jestliže otherpoint je a part of interval a otherpoint se nerovná point, potom point happens before otherpoint
.
(=>
(equal
(BeginFn ?INTERVAL)
?POINT)
(forall
(?OTHERPOINT)
(=>
(and
(temporalPart ?OTHERPOINT ?INTERVAL)
(not
(equal ?OTHERPOINT ?POINT)))
(before ?POINT ?OTHERPOINT))))
- jestliže "the end of interval" se rovná point,
- potom pro všechny otherpoint platí: jestliže otherpoint je a part of interval a otherpoint se nerovná point, potom otherpoint happens before point
.
(=>
(equal
(EndFn ?INTERVAL)
?POINT)
(forall
(?OTHERPOINT)
(=>
(and
(temporalPart ?OTHERPOINT ?INTERVAL)
(not
(equal ?OTHERPOINT ?POINT)))
(before ?OTHERPOINT ?POINT))))
(=>
(result ?PROC ?OBJ)
(forall
(?TIME)
(=>
(before
?TIME
(BeginFn
(WhenFn ?PROC)))
(not
(time ?OBJ ?TIME)))))
Jestliže leap je instancí třídy přestupný rok a leap se rovná "number rok(s)", potom
(=>
(and
(instance ?LEAP LeapYear)
(equal
?LEAP
(MeasureFn ?NUMBER Year)))
(or
(and
(equal
(RemainderFn ?NUMBER 4)
0)
(not
(equal
(RemainderFn ?NUMBER 100)
0)))
(equal
(RemainderFn ?NUMBER 400)
0)))
Jestliže "únor of year" se rovná month a year není instancí třídy přestupný rok, potom duration of month je " day duration(s)".
(=>
(and
(equal
(MonthFn February ?YEAR)
?MONTH)
(not
(instance ?YEAR LeapYear)))
(duration
?MONTH
(MeasureFn 28 DayDuration)))
- jestliže "decomposition of interval into ? interval-types" se rovná class,
- potom pro všechny time1,time2 platí: jestliže time1 je instancí třídy class a time2 je instancí třídy class a time1 se nerovná time2, potom time1 meets time2 nebo time2 meets time1 nebo time1 happens earlier than time2 nebo time2 happens earlier than time1
.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(forall
(?TIME1 ?TIME2)
(=>
(and
(instance ?TIME1 ?CLASS)
(instance ?TIME2 ?CLASS)
(not
(equal ?TIME1 ?TIME2)))
(or
(meetsTemporally ?TIME1 ?TIME2)
(meetsTemporally ?TIME2 ?TIME1)
(earlier ?TIME1 ?TIME2)
(earlier ?TIME2 ?TIME1)))))
- jestliže "decomposition of interval into ? interval-types" se rovná class,
- potom pro všechny time1 platí: jestliže time1 je instancí třídy class a time1 doesn't finish interval, potom existuje class time2 tak, že time1 meets time2
.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(forall
(?TIME1)
(=>
(and
(instance ?TIME1 ?CLASS)
(not
(finishes ?TIME1 ?INTERVAL)))
(exists
(?TIME2)
(and
(instance ?TIME2 ?CLASS)
(meetsTemporally ?TIME1 ?TIME2))))))
- jestliže "decomposition of interval into ? interval-types" se rovná class,
- potom pro všechny time1 platí: jestliže time1 je instancí třídy class a time1 doesn't start interval, potom existuje class time2 tak, že time2 meets time1
.
(=>
(equal
(TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
?CLASS)
(forall
(?TIME1)
(=>
(and
(instance ?TIME1 ?CLASS)
(not
(starts ?TIME1 ?INTERVAL)))
(exists
(?TIME2)
(and
(instance ?TIME2 ?CLASS)
(meetsTemporally ?TIME2 ?TIME1))))))
obj1 spojuje obj2 a obj3 tehdy a jen tehdy pokud obj1 je spojen s obj2 a obj1 je spojen s obj3 a obj2 není spojen s obj3.
(<=>
(connects ?OBJ1 ?OBJ2 ?OBJ3)
(and
(connected ?OBJ1 ?OBJ2)
(connected ?OBJ1 ?OBJ3)
(not
(connected ?OBJ2 ?OBJ3))))
Jestliže obj1 je a členem coll a obj2 je a členem coll a obj1 se nerovná obj2, potom obj1 se nepřekrývá s obj2.
(=>
(and
(member ?OBJ1 ?COLL)
(member ?OBJ2 ?COLL)
(not
(equal ?OBJ1 ?OBJ2)))
(not
(overlapsSpatially ?OBJ1 ?OBJ2)))
obj1 se částečně překrývá s obj2 tehdy a jen tehdy pokud - obj1 není částí obj2
a - obj2 není částí obj1
a - existuje obj3 tak, že obj3 je částí obj1 a obj3 je částí obj2
.
(<=>
(overlapsPartially ?OBJ1 ?OBJ2)
(and
(not
(part ?OBJ1 ?OBJ2))
(not
(part ?OBJ2 ?OBJ1))
(exists
(?OBJ3)
(and
(part ?OBJ3 ?OBJ1)
(part ?OBJ3 ?OBJ2)))))
Jestliže obj1 je a minimální částí obj2, potom obj1 není a interior part of obj2 a neexistuje obj3 tak, že obj3 je a interior part of obj1.
(=>
(superficialPart ?OBJ1 ?OBJ2)
(and
(not
(interiorPart ?OBJ1 ?OBJ2))
(not
(exists
(?OBJ3)
(interiorPart ?OBJ3 ?OBJ1)))))
- jestliže obj1 je a interior part of obj2,
- potom pro všechny part platí: jestliže part je a minimální částí obj2, potom obj1 se nepřekrývá s part
.
(=>
(interiorPart ?OBJ1 ?OBJ2)
(forall
(?PART)
(=>
(superficialPart ?PART ?OBJ2)
(not
(overlapsSpatially ?OBJ1 ?PART)))))
Jestliže bottom(bottom,object) platí a part je částí object a part není spojen s bottom, potom part je above vzhledem k bottom.
(=>
(and
(bottom ?BOTTOM ?OBJECT)
(part ?PART ?OBJECT)
(not
(connected ?PART ?BOTTOM)))
(orientation ?PART ?BOTTOM Above))
Jestliže top(top,object) platí a part je částí object a part není spojen s top, potom part je below vzhledem k top.
(=>
(and
(top ?TOP ?OBJECT)
(part ?PART ?OBJECT)
(not
(connected ?PART ?TOP)))
(orientation ?PART ?TOP Below))
Jestliže side(side,object) platí a part je částí object a part není spojen s side, potom existuje direct tak, že side je direct vzhledem k part.
(=>
(and
(side ?SIDE ?OBJECT)
(part ?PART ?OBJECT)
(not
(connected ?PART ?SIDE)))
(exists
(?DIRECT)
(orientation ?SIDE ?PART ?DIRECT)))
Jestliže obj3 se rovná "mereological difference fn(obj1,obj2)", potom pro všechny part platí: part je částí obj3 tehdy a jen tehdy pokud part je částí obj1 a part není částí obj2.
(=>
(equal
?OBJ3
(MereologicalDifferenceFn ?OBJ1 ?OBJ2))
(forall
(?PART)
(<=>
(part ?PART ?OBJ3)
(and
(part ?PART ?OBJ1)
(not
(part ?PART ?OBJ2))))))
Jestliže hole je díra v obj, potom obj není instancí třídy díra.
(=>
(hole ?HOLE ?OBJ)
(not
(instance ?OBJ Hole)))
Jestliže hole je díra v obj, potom hole se nepřekrývá s obj.
(=>
(hole ?HOLE ?OBJ)
(not
(overlapsSpatially ?HOLE ?OBJ)))
Jestliže hole1 je instancí třídy díra a hole2 je vlastní částí hole1, potom existuje obj tak, že hole1 se dotýká obj a hole2 se nedotýká obj.
(=>
(and
(instance ?HOLE1 Hole)
(properPart ?HOLE2 ?HOLE1))
(exists
(?OBJ)
(and
(meetsSpatially ?HOLE1 ?OBJ)
(not
(meetsSpatially ?HOLE2 ?OBJ)))))
Jestliže obj1 zaplňuje hole a fillable je atributem obj2, potom obj1 se nepřekrývá s obj2.
(=>
(and
(fills ?OBJ1 ?HOLE)
(attribute ?OBJ2 Fillable))
(not
(overlapsSpatially ?OBJ1 ?OBJ2)))
Jestliže rep je instancí třídy sexuální reprodukce a organism je výsledkem rep, potom neexistují mother,father tak, že mother je a mother of organism a father je a father of organism.
(=>
(and
(instance ?REP SexualReproduction)
(result ?REP ?ORGANISM))
(not
(exists
(?MOTHER ?FATHER)
(and
(mother ?ORGANISM ?MOTHER)
(father ?ORGANISM ?FATHER)))))
Jestliže rep je instancí třídy asexuální reprodukce a organism je výsledkem rep, potom neexistují parent1,parent2 tak, že parent1 je a parent of organism a parent2 je a parent of organism a parent1 se nerovná parent2.
(=>
(and
(instance ?REP AsexualReproduction)
(result ?REP ?ORGANISM))
(not
(exists
(?PARENT1 ?PARENT2)
(and
(parent ?ORGANISM ?PARENT1)
(parent ?ORGANISM ?PARENT2)
(not
(equal ?PARENT1 ?PARENT2))))))
Jestliže leave je instancí třídy opuštění organizace a org je instancí třídy organizace a org je původcem leave a person je účastníkem leave, potom person není a členem org právě po doba existence leave.
(=>
(and
(instance ?LEAVE LeavingAnOrganization)
(instance ?ORG Organization)
(agent ?LEAVE ?ORG)
(patient ?LEAVE ?PERSON))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?LEAVE))
(not
(member ?PERSON ?ORG))))
Jestliže fire je instancí třídy ukončení pracovního poměru a org je instancí třídy organizace a org je původcem fire a person je účastníkem fire, potom org doesn't employ person právě po doba existence fire.
(=>
(and
(instance ?FIRE TerminatingEmployment)
(instance ?ORG Organization)
(agent ?FIRE ?ORG)
(patient ?FIRE ?PERSON))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?FIRE))
(not
(employs ?ORG ?PERSON))))
- jestliže
- path1 je cesta podél které se vyskytuje process
a - process začíná v source
a - process končí v dest
a - délka path1 je measure1
a - neexistují path2,measure2 tak, že path2 je cesta podél které se vyskytuje process a process začíná v origin a process končí v dest a délka path2 je measure2 a measure2 je menší než measure1
, - potom pro všechny obj platí: jestliže obj je částí path1, potom obj je mezi source a 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))))
Jestliže proc je instancí třídy změna směru, potom existuje směrový atribut attr tak, že
(=>
(instance ?PROC DirectionChange)
(exists
(?ATTR)
(and
(instance ?ATTR DirectionalAttribute)
(or
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?PROC))
(manner ?PROC ?ATTR))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?PROC))
(not
(manner ?PROC ?ATTR))))
(and
(holdsDuring
(ImmediateFutureFn
(WhenFn ?PROC))
(manner ?PROC ?ATTR))
(holdsDuring
(ImmediatePastFn
(WhenFn ?PROC))
(not
(manner ?PROC ?ATTR))))))))
Jestliže transfer je instancí třídy přeprava a agent je původcem transfer a patient je účastníkem transfer, potom agent se nerovná patient.
(=>
(and
(instance ?TRANSFER Transfer)
(agent ?TRANSFER ?AGENT)
(patient ?TRANSFER ?PATIENT))
(not
(equal ?AGENT ?PATIENT)))
Jestliže remove je instancí třídy odstranění a remove začíná v place a obj je účastníkem remove, potom obj je located at place právě před doba existence remove a obj není located at place právě po doba existence remove.
(=>
(and
(instance ?REMOVE Removing)
(origin ?REMOVE ?PLACE)
(patient ?REMOVE ?OBJ))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?REMOVE))
(located ?OBJ ?PLACE))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?REMOVE))
(not
(located ?OBJ ?PLACE)))))
Jestliže put je instancí třídy uložení a put končí v place a obj je účastníkem put, potom obj není located at place právě před doba existence put a obj je located at place právě po doba existence put.
(=>
(and
(instance ?PUT Putting)
(destination ?PUT ?PLACE)
(patient ?PUT ?OBJ))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?PUT))
(not
(located ?OBJ ?PLACE)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?PUT))
(located ?OBJ ?PLACE))))
Jestliže sub je instancí třídy záměna, potom existují uložení put,odstranění remove,obj1,obj2,place tak, že put je a subprocess of sub a remove je a subprocess of sub a obj1 je účastníkem remove a remove začíná v place a obj2 je účastníkem put a put končí v place a obj1 se nerovná obj2.
(=>
(instance ?SUB Substituting)
(exists
(?PUT ?REMOVE ?OBJ1 ?OBJ2 ?PLACE)
(and
(instance ?PUT Putting)
(instance ?REMOVE Removing)
(subProcess ?PUT ?SUB)
(subProcess ?REMOVE ?SUB)
(patient ?REMOVE ?OBJ1)
(origin ?REMOVE ?PLACE)
(patient ?PUT ?OBJ2)
(destination ?PUT ?PLACE)
(not
(equal ?OBJ1 ?OBJ2)))))
Jestliže change je instancí třídy změna vlastnictví a obj je účastníkem change a agent1 posesses obj právě před doba existence change a agent2 posesses obj právě po doba existence change, potom agent1 se nerovná agent2.
(=>
(and
(instance ?CHANGE ChangeOfPossession)
(patient ?CHANGE ?OBJ)
(holdsDuring
(ImmediatePastFn
(WhenFn ?CHANGE))
(possesses ?AGENT1 ?OBJ))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?CHANGE))
(possesses ?AGENT2 ?OBJ)))
(not
(equal ?AGENT1 ?AGENT2)))
Jestliže give je instancí třídy jednosměrné dávání, potom neexistuje transakce trans tak, že give je a subprocess of trans.
(=>
(instance ?GIVE UnilateralGiving)
(not
(exists
(?TRANS)
(and
(instance ?TRANS Transaction)
(subProcess ?GIVE ?TRANS)))))
Jestliže get je instancí třídy jednosměrné braní, potom neexistuje transakce trans tak, že get je a subprocess of trans.
(=>
(instance ?GET UnilateralGetting)
(not
(exists
(?TRANS)
(and
(instance ?TRANS Transaction)
(subProcess ?GET ?TRANS)))))
Jestliže trans je instancí třídy transakce, potom existují agent1,agent2,dávání give1,dávání give2,obj1,obj2 tak, že give1 je a subprocess of trans a give2 je a subprocess of trans a agent1 je původcem give1 a agent2 je původcem give2 a obj1 je účastníkem give1 a obj2 je účastníkem give2 a give1 končí v agent2 a give2 končí v agent1 a agent1 se nerovná agent2 a obj1 se nerovná obj2.
(=>
(instance ?TRANS Transaction)
(exists
(?AGENT1 ?AGENT2 ?GIVE1 ?GIVE2 ?OBJ1 ?OBJ2)
(and
(instance ?GIVE1 Giving)
(instance ?GIVE2 Giving)
(subProcess ?GIVE1 ?TRANS)
(subProcess ?GIVE2 ?TRANS)
(agent ?GIVE1 ?AGENT1)
(agent ?GIVE2 ?AGENT2)
(patient ?GIVE1 ?OBJ1)
(patient ?GIVE2 ?OBJ2)
(destination ?GIVE1 ?AGENT2)
(destination ?GIVE2 ?AGENT1)
(not
(equal ?AGENT1 ?AGENT2))
(not
(equal ?OBJ1 ?OBJ2)))))
Jestliže confine je instancí třídy věznění a person je účastníkem confine, potom person doesn't desire "person je účastníkem confine".
(=>
(and
(instance ?CONFINE Confining)
(patient ?CONFINE ?PERSON))
(not
(desires
?PERSON
(patient ?CONFINE ?PERSON))))
process je instancí třídy zničení tehdy a jen tehdy pokud existuje patient tak, že patient je účastníkem process a patient exists during "právě před doba existence process" a patient doesn't exist during "právě po doba existence process".
(<=>
(instance ?PROCESS Destruction)
(exists
(?PATIENT)
(and
(patient ?PROCESS ?PATIENT)
(time
?PATIENT
(ImmediatePastFn
(WhenFn ?PROCESS)))
(not
(time
?PATIENT
(ImmediateFutureFn
(WhenFn ?PROCESS)))))))
Jestliže attach je instancí třídy připojení a obj1 je účastníkem attach a obj2 je účastníkem attach, potom obj1 není spojen s obj2 právě před doba existence attach a obj1 je spojen s obj2 právě po doba existence attach.
(=>
(and
(instance ?ATTACH Attaching)
(patient ?ATTACH ?OBJ1)
(patient ?ATTACH ?OBJ2))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?ATTACH))
(not
(connected ?OBJ1 ?OBJ2)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ATTACH))
(connected ?OBJ1 ?OBJ2))))
Jestliže detach je instancí třídy odpojení a obj1 je účastníkem detach a obj2 je účastníkem detach, potom obj1 je spojen s obj2 právě před doba existence detach a obj1 není spojen s obj2 právě po doba existence detach.
(=>
(and
(instance ?DETACH Detaching)
(patient ?DETACH ?OBJ1)
(patient ?DETACH ?OBJ2))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?DETACH))
(connected ?OBJ1 ?OBJ2))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?DETACH))
(not
(connected ?OBJ1 ?OBJ2)))))
combine je instancí třídy spojení a obj1 je nástrojem pro combine a obj2 je výsledkem combine tehdy a jen tehdy pokud obj1 není částí obj2 právě před doba existence combine a obj1 je částí obj2 právě po doba existence combine.
(<=>
(and
(instance ?COMBINE Combining)
(resource ?COMBINE ?OBJ1)
(result ?COMBINE ?OBJ2))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?COMBINE))
(not
(part ?OBJ1 ?OBJ2)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?COMBINE))
(part ?OBJ1 ?OBJ2))))
compound je instancí třídy sloučenina tehdy a jen tehdy pokud existují elementární látka element1,elementární látka element2,chemická syntéza process tak, že element1 se nerovná element2 a element1 je nástrojem pro process a element2 je nástrojem pro process a compound je výsledkem process.
(<=>
(instance ?COMPOUND CompoundSubstance)
(exists
(?ELEMENT1 ?ELEMENT2 ?PROCESS)
(and
(instance ?ELEMENT1 ElementalSubstance)
(instance ?ELEMENT2 ElementalSubstance)
(not
(equal ?ELEMENT1 ?ELEMENT2))
(instance ?PROCESS ChemicalSynthesis)
(resource ?PROCESS ?ELEMENT1)
(resource ?PROCESS ?ELEMENT2)
(result ?PROCESS ?COMPOUND))))
Jestliže change je instancí třídy interní změna a obj je účastníkem change, potom existuje property tak, že
(=>
(and
(instance ?CHANGE InternalChange)
(patient ?CHANGE ?OBJ))
(exists
(?PROPERTY)
(or
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?CHANGE))
(attribute ?OBJ ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?CHANGE))
(not
(attribute ?OBJ ?PROPERTY))))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?CHANGE))
(not
(attribute ?OBJ ?PROPERTY)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?CHANGE))
(attribute ?OBJ ?PROPERTY))))))
Jestliže alt je instancí třídy změna povrchu a obj je účastníkem alt, potom existují part,property tak, že part je a minimální částí obj a property je atributem part právě před doba existence alt a property není atributem part právě po doba existence alt.
(=>
(and
(instance ?ALT SurfaceChange)
(patient ?ALT ?OBJ))
(exists
(?PART ?PROPERTY)
(and
(superficialPart ?PART ?OBJ)
(holdsDuring
(ImmediatePastFn
(WhenFn ?ALT))
(attribute ?PART ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ALT))
(not
(attribute ?PART ?PROPERTY))))))
Jestliže alt je instancí třídy změna tvaru a obj je účastníkem alt, potom existuje tvar property tak, že
(=>
(and
(instance ?ALT ShapeChange)
(patient ?ALT ?OBJ))
(exists
(?PROPERTY)
(and
(instance ?PROPERTY ShapeAttribute)
(or
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?ALT))
(attribute ?OBJ ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ALT))
(not
(attribute ?OBJ ?PROPERTY))))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?ALT))
(not
(attribute ?OBJ ?PROPERTY)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ALT))
(attribute ?OBJ ?PROPERTY)))))))
Jestliže coloring je instancí třídy barvení a obj je účastníkem coloring, potom existuje atribut barvy property tak, že property je atributem obj právě před doba existence coloring a property není atributem obj právě po doba existence coloring.
(=>
(and
(instance ?COLORING Coloring)
(patient ?COLORING ?OBJ))
(exists
(?PROPERTY)
(and
(instance ?PROPERTY ColorAttribute)
(holdsDuring
(ImmediatePastFn
(WhenFn ?COLORING))
(attribute ?OBJ ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?COLORING))
(not
(attribute ?OBJ ?PROPERTY))))))
process je instancí třídy vytváření tehdy a jen tehdy pokud existuje patient tak, že patient je účastníkem process a patient exists during "právě po doba existence process" a patient doesn't exist during "právě před doba existence process".
(<=>
(instance ?PROCESS Creation)
(exists
(?PATIENT)
(and
(patient ?PROCESS ?PATIENT)
(time
?PATIENT
(ImmediateFutureFn
(WhenFn ?PROCESS)))
(not
(time
?PATIENT
(ImmediatePastFn
(WhenFn ?PROCESS)))))))
Jestliže pursue je instancí třídy sledování a agent je původcem pursue a obj je účastníkem pursue, potom agent doesn't posess obj během pursue.
(=>
(and
(instance ?PURSUE Pursuing)
(agent ?PURSUE ?AGENT)
(patient ?PURSUE ?OBJ))
(holdsDuring
?PURSUE
(not
(possesses ?AGENT ?OBJ))))
Jestliže investigate je instancí třídy vyšetřování a agent je původcem investigate a prop je účastníkem investigate, potom agent doesn't know prop doba existence investigate.
(=>
(and
(instance ?INVESTIGATE Investigating)
(agent ?INVESTIGATE ?AGENT)
(patient ?INVESTIGATE ?PROP))
(holdsDuring
(WhenFn ?INVESTIGATE)
(not
(knows ?AGENT ?PROP))))
Jestliže interaction je instancí třídy sociální interakce, potom existují agent1,agent2 tak, že agent1 je původcem interaction a agent2 je původcem interaction a agent1 se nerovná agent2.
(=>
(instance ?INTERACTION SocialInteraction)
(exists
(?AGENT1 ?AGENT2)
(and
(agent ?INTERACTION ?AGENT1)
(agent ?INTERACTION ?AGENT2)
(not
(equal ?AGENT1 ?AGENT2)))))
Jestliže disseminate je instancí třídy šíření, potom existují myslící agent agent1,myslící agent agent2 tak, že disseminate končí v agent1 a disseminate končí v agent2 a agent1 se nerovná agent2.
(=>
(instance ?DISSEMINATE Disseminating)
(exists
(?AGENT1 ?AGENT2)
(and
(destination ?DISSEMINATE ?AGENT1)
(instance ?AGENT1 CognitiveAgent)
(destination ?DISSEMINATE ?AGENT2)
(instance ?AGENT2 CognitiveAgent)
(not
(equal ?AGENT1 ?AGENT2)))))
Jestliže question je instancí třídy dotaz a agent je původcem question a formula je účastníkem question a formula je instancí třídy formule, potom agent doesn't know formula doba existence question.
(=>
(and
(instance ?QUESTION Questioning)
(agent ?QUESTION ?AGENT)
(patient ?QUESTION ?FORMULA)
(instance ?FORMULA Formula))
(holdsDuring
(WhenFn ?QUESTION)
(not
(knows ?AGENT ?FORMULA))))
Jestliže contest je instancí třídy soutěž, potom existují agent1,agent2,purp1,purp2 tak, že agent1 je původcem contest a agent2 je původcem contest a contest has purpose purp1 for agent1 a contest has purpose purp2 for agent2 a agent1 se nerovná agent2 a purp1 se nerovná purp2.
(=>
(instance ?CONTEST Contest)
(exists
(?AGENT1 ?AGENT2 ?PURP1 ?PURP2)
(and
(agent ?CONTEST ?AGENT1)
(agent ?CONTEST ?AGENT2)
(hasPurposeForAgent ?CONTEST ?PURP1 ?AGENT1)
(hasPurposeForAgent ?CONTEST ?PURP2 ?AGENT2)
(not
(equal ?AGENT1 ?AGENT2))
(not
(equal ?PURP1 ?PURP2)))))
Jestliže process je instancí třídy změna skupenství a obj je účastníkem process, potom existují part,skupenství state1,skupenství state2 tak, že part je částí obj a state1 se nerovná state2 a state1 je atributem part právě před doba existence process a state2 je atributem part právě po doba existence freeze.
(=>
(and
(instance ?PROCESS StateChange)
(patient ?PROCESS ?OBJ))
(exists
(?PART ?STATE1 ?STATE2)
(and
(part ?PART ?OBJ)
(instance ?STATE1 PhysicalState)
(instance ?STATE2 PhysicalState)
(not
(equal ?STATE1 ?STATE2))
(holdsDuring
(ImmediatePastFn
(WhenFn ?PROCESS))
(attribute ?PART ?STATE1))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?FREEZE))
(attribute ?PART ?STATE2)))))
Jestliže island je instancí třídy ostrov, potom neexistují souš area,part1,part2 tak, že part1 je částí island a part2 je částí area a island není částí area a area není částí island a part1 je spojen s part2.
(=>
(instance ?ISLAND Island)
(not
(exists
(?AREA ?PART1 ?PART2)
(and
(instance ?AREA LandArea)
(part ?PART1 ?ISLAND)
(part ?PART2 ?AREA)
(not
(part ?ISLAND ?AREA))
(not
(part ?AREA ?ISLAND))
(connected ?PART1 ?PART2)))))
Jestliže part je instancí třídy část těla, potom neexistuje patologický proces proc tak, že part je výsledkem proc.
(=>
(instance ?PART BodyPart)
(not
(exists
(?PROC)
(and
(instance ?PROC PathologicProcess)
(result ?PROC ?PART)))))
Jestliže junct je instancí třídy tělní kloub, potom existují část těla struct1,část těla struct2 tak, že junct je spojen s struct1 a junct je spojen s struct2 a struct1 se nerovná struct2.
(=>
(instance ?JUNCT BodyJunction)
(exists
(?STRUCT1 ?STRUCT2)
(and
(connected ?JUNCT ?STRUCT1)
(connected ?JUNCT ?STRUCT2)
(instance ?STRUCT1 BodyPart)
(instance ?STRUCT2 BodyPart)
(not
(equal ?STRUCT1 ?STRUCT2)))))
Jestliže morph je instancí třídy morfém, potom neexistuje morfém othermorph tak, že othermorph je částí morph a othermorph se nerovná morph.
(=>
(instance ?MORPH Morpheme)
(not
(exists
(?OTHERMORPH)
(and
(instance ?OTHERMORPH Morpheme)
(part ?OTHERMORPH ?MORPH)
(not
(equal ?OTHERMORPH ?MORPH))))))
Jestliže phrase je instancí třídy fráze, potom existují slovo part1,slovo part2 tak, že part1 je částí phrase a part2 je částí phrase a part1 se nerovná part2.
(=>
(instance ?PHRASE Phrase)
(exists
(?PART1 ?PART2)
(and
(part ?PART1 ?PHRASE)
(part ?PART2 ?PHRASE)
(instance ?PART1 Word)
(instance ?PART2 Word)
(not
(equal ?PART1 ?PART2)))))
Jestliže series je instancí třídy řada, potom existují kniha book1,kniha book2 tak, že subsumes content instance(series,book1) platí a subsumes content instance(series,book2) platí a book1 se nerovná book2.
(=>
(instance ?SERIES Series)
(exists
(?BOOK1 ?BOOK2)
(and
(instance ?BOOK1 Book)
(instance ?BOOK2 Book)
(subsumesContentInstance ?SERIES ?BOOK1)
(subsumesContentInstance ?SERIES ?BOOK2)
(not
(equal ?BOOK1 ?BOOK2)))))
Jestliže mole je instancí třídy molekula, potom existují atom atom1,atom atom2 tak, že atom1 je částí mole a atom2 je částí mole a atom1 se nerovná atom2.
(=>
(instance ?MOLE Molecule)
(exists
(?ATOM1 ?ATOM2)
(and
(instance ?ATOM1 Atom)
(instance ?ATOM2 Atom)
(part ?ATOM1 ?MOLE)
(part ?ATOM2 ?MOLE)
(not
(equal ?ATOM1 ?ATOM2)))))
Jestliže connected engineering components(comp1,comp2) platí, potom engineering subcomponent(comp1,comp2) doesn't hold a engineering subcomponent(comp2,comp1) doesn't hold.
(=>
(connectedEngineeringComponents ?COMP1 ?COMP2)
(and
(not
(engineeringSubcomponent ?COMP1 ?COMP2))
(not
(engineeringSubcomponent ?COMP2 ?COMP1))))
Jestliže connected engineering components(comp1,comp2) platí, potom comp1 není instancí třídy spojení inženýrských komponent a comp2 není instancí třídy spojení inženýrských komponent.
(=>
(connectedEngineeringComponents ?COMP1 ?COMP2)
(not
(or
(instance ?COMP1 EngineeringConnection)
(instance ?COMP2 EngineeringConnection))))
Jestliže obj1 je attr1 vzhledem k obj2 a contrary attribute() platí a attr1 je a member of "()" a attr2 je a member of "()" a attr1 se nerovná attr2, potom obj1 není attr2 vzhledem k obj2.
(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(contraryAttribute @ROW)
(inList
?ATTR1
(ListFn @ROW))
(inList
?ATTR2
(ListFn @ROW))
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))
Jestliže obj1 je attr1 vzhledem k obj2 a attr1 je instancí třídy směrový atribut a attr2 je instancí třídy směrový atribut a attr1 se nerovná attr2, potom obj1 není attr2 vzhledem k obj2.
(=>
(and
(orientation ?OBJ1 ?OBJ2 ?ATTR1)
(instance ?ATTR1 DirectionalAttribute)
(instance ?ATTR2 DirectionalAttribute)
(not
(equal ?ATTR1 ?ATTR2)))
(not
(orientation ?OBJ1 ?OBJ2 ?ATTR2)))
Jestliže obj1 je above vzhledem k obj2, potom obj1 není spojen s obj2.
(=>
(orientation ?OBJ1 ?OBJ2 Above)
(not
(connected ?OBJ1 ?OBJ2)))
Jestliže obj1 je near vzhledem k obj2, potom obj1 není spojen s obj2.
(=>
(orientation ?OBJ1 ?OBJ2 Near)
(not
(connected ?OBJ1 ?OBJ2)))
Jestliže obj1 je on vzhledem k obj2, potom obj2 není on vzhledem k obj1.
(=>
(orientation ?OBJ1 ?OBJ2 On)
(not
(orientation ?OBJ2 ?OBJ1 On)))
Pro všechny org platí: org doesn't employ person a person je instancí třídy člověk tehdy a jen tehdy pokud unemployed je atributem person.
(<=>
(forall
(?ORG)
(and
(not
(employs ?ORG ?PERSON))
(instance ?PERSON Human)))
(attribute ?PERSON Unemployed))
modal attribute(formula,necessity) platí tehdy a jen tehdy pokud modal attribute(formula,possibility) doesn't hold.
(<=>
(modalAttribute ?FORMULA Necessity)
(not
(modalAttribute
(not ?FORMULA)
Possibility)))
modal attribute(formula,obligation) platí tehdy a jen tehdy pokud modal attribute(formula,permission) doesn't hold.
(<=>
(modalAttribute ?FORMULA Obligation)
(not
(modalAttribute
(not ?FORMULA)
Permission)))
Jestliže polychromatic je atributem obj, potom existují part1,part2,atribut barvy color1,atribut barvy color2 tak, že part1 je a minimální částí obj a part2 je a minimální částí obj a color1 je atributem part1 a color2 je atributem part2 a color1 se nerovná color2.
(=>
(attribute ?OBJ Polychromatic)
(exists
(?PART1 ?PART2 ?COLOR1 ?COLOR2)
(and
(superficialPart ?PART1 ?OBJ)
(superficialPart ?PART2 ?OBJ)
(attribute ?PART1 ?COLOR1)
(attribute ?PART2 ?COLOR2)
(instance ?COLOR1 ColorAttribute)
(instance ?COLOR2 ColorAttribute)
(not
(equal ?COLOR1 ?COLOR2)))))
Jestliže dry je atributem obj, potom neexistuje subobj tak, že subobj je částí obj a liquid je atributem subobj.
(=>
(attribute ?OBJ Dry)
(not
(exists
(?SUBOBJ)
(and
(part ?SUBOBJ ?OBJ)
(attribute ?SUBOBJ Liquid)))))
Jestliže unbreakable je atributem obj, potom neexistuje poškození damage tak, že obj je účastníkem damage.
(=>
(attribute ?OBJ Unbreakable)
(not
(exists
(?DAMAGE)
(and
(instance ?DAMAGE Damaging)
(patient ?DAMAGE ?OBJ)))))
Jestliže embryonic je atributem org během time, potom neexistuje narození birth tak, že org prodělává birth během time.
(=>
(holdsDuring
?TIME
(attribute ?ORG Embryonic))
(holdsDuring
?TIME
(not
(exists
(?BIRTH)
(and
(instance ?BIRTH Birth)
(experiencer ?BIRTH ?ORG))))))
entity je instancí třídy "complement fn(class)" tehdy a jen tehdy pokud entity není instancí třídy class.
(<=>
(instance
?ENTITY
(ComplementFn ?CLASS))
(not
(instance ?ENTITY ?CLASS)))
