Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - not
not

appearance as argument number 2
-------------------------


No TPTP formula. May not be expressible in strict first order. domainEnglishFormat.kif 7300-7300 "not" is the printable form of not in english language

antecedent
-------------------------


( ! [V__PERSON] :
   ((s__instance(V__PERSON,s__Human) &
       (! [V__ORG] :
         (~ s__employs(V__ORG,V__PERSON))))
   <=>
   s__attribute(V__PERSON,s__Unemployed))
)

Merge.kif 17552-17558 A cognitive agent is an instance of human and for all an agent the agent doesn't employ the cognitive agent if and only if unemployed is an attribute of the cognitive agent
( ! [V__Withdrawal,V__Account] :
   ((s__instance(V__Withdrawal,s__Withdrawal) &
       s__instance(V__Account,s__FinancialAccount) &
       s__origin(V__Withdrawal,s__CurrencyFn(V__Account))
   &
   (~ (? [V__Penalty] :
       (s__instance(V__Penalty,s__Penalty) &
         s__destination(V__Penalty,s__CurrencyFn(V__Account))
     &
     s__causes(V__Withdrawal,V__Penalty)))))
<=>
s__liquidity(V__Account,s__HighLiquidity))
)

FinancialOntology.kif 1756-1766 A process is an instance of withdrawal and a financial account is an instance of financial account and the process originates at the currency of the financial account and there doesn't exist another process such that the other process is an instance of penalty and the other process ends up at the currency of the financial account and the process causes the other process if and only if the liqudity of the financial account is high liquidity
( ! [V__AREA] :
   ((s__attribute(V__AREA,s__HighIncomeCountry) &
       (~ s__member(V__AREA,s__OrganizationOfPetroleumExportingCountries)))
     =>
     s__economyType(V__AREA,s__DevelopedCountry))
   )

Economy.kif 501-505
( ! [V__FOOD1,V__MEAS1,V__FOOD2,V__MEAS2,V__CLASS] :
   ((s__attribute(V__FOOD1,s__FamilyStylePortion) &
       s__measure(V__FOOD1,V__MEAS1)
     &
     (~ s__attribute(V__FOOD2,s__FamilyStylePortion))
     &
     s__measure(V__FOOD2,V__MEAS2)
   &
   s__instance(V__FOOD1,V__CLASS)
&
s__instance(V__FOOD2,V__CLASS))
=>
s__greaterThan(V__MEAS1,V__MEAS2))
)

Dining.kif 1119-1127
( ! [V__O,V__P] :
   ((s__attribute(V__O,V__P)
     &
     s__instance(V__P,s__Fingerprint) &
     (~ s__instance(V__O,s__Finger)))
   =>
   (? [V__PR,V__F] :
     (s__instrument(V__PR,V__F)
     &
     s__instance(V__F,s__Finger) &
     s__attribute(V__F,V__P)
   &
   s__patient(V__PR,V__O))))
)

Mid-level-ontology.kif 10255-10265
( ! [V__BOTTOM,V__OBJECT,V__PART] :
   ((s__bottom(V__BOTTOM,V__OBJECT)
     &
     s__part(V__PART,V__OBJECT)
   &
   (~ s__connected(V__PART,V__BOTTOM)))
=>
s__orientation(V__PART,V__BOTTOM,s__Above))
)

Merge.kif 9673-9678
( ! [V__P,V__C] :
   ((s__citizen(V__P,V__C)
     &
     (~ (? [V__L] :
         s__located(V__P,V__L))))
=>
s__located(V__P,V__C))
)

Military.kif 772-778
No TPTP formula. May not be expressible in strict first order. Dining.kif 1102-1110
No TPTP formula. May not be expressible in strict first order. Dining.kif 130-153
No TPTP formula. May not be expressible in strict first order. Hotel.kif 1294-1305
( ! [V__PATH,V__GRAPH,V__NODE1,V__NODE2] :
   ((s__graphPart(V__PATH,V__GRAPH)
     &
     (~ s__instance(V__GRAPH,s__DirectedGraph)))
   =>
   ((s__GraphPathFn(V__NODE1,V__NODE2)
     = V__PATH)
   <=>
   (s__GraphPathFn(V__NODE2,V__NODE1)
   = V__PATH)))
)

Merge.kif 6178-6184
( ! [V__WIN1,V__SCREEN,V__WIN2] :
   ((s__hasGUEState(V__WIN1,s__GUE_UncoveredState) &
       s__hasGUEState(V__WIN1,s__GUE_MaximizedState) &
       s__screenOfGUIE(V__WIN1,V__SCREEN)
     &
     s__instance(V__WIN2,s__InterfaceWindow) &
     s__screenOfGUIE(V__WIN2,V__SCREEN)
   &
   (~ (V__WIN1 = V__WIN2)))
=>
(s__hasGUEState(V__WIN2,s__GUE_CoveredState) |
   s__hasGUEState(V__WIN2,s__GUE_PartiallyCoveredState) |
   s__hasGUEState(V__WIN2,s__GUE_OffscreenState)))
)

ComputerInput.kif 1738-1749
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28718-28739
( ! [V__A,V__S1,V__S2,V__S1_START,V__S2_START] :
   ((s__instance(V__A,s__Ambulating) &
       s__subProcess(V__S1,V__A)
     &
     s__instance(V__S1,s__Stepping) &
     s__subProcess(V__S2,V__A)
   &
   s__instance(V__S2,s__Stepping) &
   (V__S1_START = s__BeginFn(s__WhenFn(V__S1)))
&
(V__S2_START = s__BeginFn(s__WhenFn(V__S2)))
&
(~ (s__before(V__S1_START,V__S2_START)
|
s__before(V__S2_START,V__S1_START))))
=>
(V__S1 = V__S2))
)

Mid-level-ontology.kif 676-689
( ! [V__A1,V__A2,V__S1,V__R1,V__R2] :
   ((s__instance(V__A1,s__Automobile) &
       s__instance(V__A2,s__Automobile) &
       s__instance(V__S1,s__AutomobileShock) &
       s__part(V__S1,V__A1)
     &
     (~ (? [V__S2] :
         (s__instance(V__S2,s__AutomobileShock) &
           s__part(V__S2,V__A2))))
   &
   s__dampingRatio(V__A1,V__R1)
&
s__dampingRatio(V__A2,V__R2))
=>
s__greaterThan(V__R2,V__R1))
)

Cars.kif 843-856
No TPTP formula. May not be expressible in strict first order. Dining.kif 729-752
( ! [V__ANI,V__D] :
   ((s__instance(V__ANI,s__Animal) &
       s__instance(V__D,s__DiseaseOrSyndrome) &
       (~ s__attribute(V__ANI,V__D)))
   =>
   (? [V__P,V__W] :
     (s__instance(V__P,s__BiologicalProcess) &
       s__instance(V__P,s__Removing) &
       s__origin(V__P,V__ANI)
     &
     s__instance(V__W,s__Sewage) &
     s__agent(V__P,V__ANI)
   &
   s__patient(V__P,V__W))))
)

Mid-level-ontology.kif 2621-2634
( ! [V__B] :
   ((s__instance(V__B,s__Bubble) &
       (~ (? [V__X,V__S] :
           (s__attribute(V__X,V__S)
           &
           (~ (V__X = s__Gas))
             &
             s__meetsSpatially(V__X,V__B)))))
   =>
   s__attribute(V__B,s__RoundShape))
)

Mid-level-ontology.kif 5318-5327
No TPTP formula. May not be expressible in strict first order. Cars.kif 4047-4077
( ! [V__C,V__X1,V__X2] :
   ((s__instance(V__C,s__Convoy) &
       s__member(V__X1,V__C)
     &
     s__member(V__X2,V__C)
   &
   (~ (V__X1 = V__X2)))
=>
(? [V__P1,V__P2,V__D] :
   (s__instance(V__P1,s__Transportation) &
     s__instance(V__P2,s__Transportation) &
     s__agent(V__P1,V__X1)
   &
   s__agent(V__P2,V__X2)
&
s__destination(V__P1,V__D)
&
s__destination(V__P2,V__D))))
)

Military.kif 108-122
( ! [V__C,V__Sub,V__S,V__X,V__MBR] :
   ((s__instance(V__C,s__Crystal) &
       s__attribute(V__C,s__MonoCrystalline) &
       s__instance(V__Sub,s__Substance) &
       s__attribute(V__Sub,s__Solid) &
       s__attribute(V__Sub,s__PolyCrystalline) &
       s__instance(V__S,s__Substance) &
       s__surface(V__S,V__Sub)
     &
     (~ s__part(V__C,V__S)))
=>
(? [V__CLNT] :
   (s__instance(V__CLNT,s__Collection) &
     s__memberCount(V__CLNT,V__X)
   &
   s__greaterThanOrEqualTo(V__X,4)
&
(s__member(V__MBR,V__CLNT)
=>
(s__part(V__MBR,V__Sub)
&
s__meetsSpatially(V__C,V__MBR))))))
)

Geography.kif 6495-6515
No TPTP formula. May not be expressible in strict first order. Media.kif 224-231
( ! [V__CITY] :
   ((s__instance(V__CITY,s__AmericanCity) &
       s__part(V__CITY,s__California) &
       (~ (V__CITY = s__LosAngelesCalifornia)))
       =>
       s__greaterThan(s__CardinalityFn(s__ResidentFn(s__LosAngelesCalifornia))
    ,s__CardinalityFn(s__ResidentFn(V__CITY))))
)

CountriesAndRegions.kif 812-817
( ! [V__COLL,V__SITE,V__AGENT,V__LISTING,V__TIME] :
   ((s__instance(V__COLL,s__Collection) &
       s__instance(V__SITE,s__WebSite) &
       s__instance(V__AGENT,s__Agent) &
       s__instance(V__LISTING,s__WebListing) &
       s__instance(V__TIME,s__TimePoint) &
       s__listingSeller(V__LISTING,V__AGENT)
     &
     (~ s__member(V__LISTING,V__COLL))
   &
   (! [V__ITEM] :
     ((s__instance(V__ITEM,s__WebListing) &
         s__member(V__ITEM,s__SellersItemsFn(V__AGENT,V__SITE))
     &
     s__temporalPart(V__TIME,s__WhenFn(V__ITEM))
&
(~ (V__ITEM = V__LISTING)))
=>
s__member(V__ITEM,V__COLL)))
&
(! [V__MEMBER] :
(s__member(V__MEMBER,V__COLL)
=>
(s__temporalPart(V__TIME,s__WhenFn(V__ITEM))
&
s__instance(V__MEMBER,s__WebListing)))))
=>
(s__SellersOtherItemsFn(V__AGENT,V__SITE,V__LISTING,V__TIME)
= V__COLL))
)

UXExperimentalTerms.kif 1229-1256
( ! [V__CS1,V__CLASS,V__ECLASS,V__N,V__G,V__E] :
   ((s__instance(V__CS1,V__CLASS)
     &
     s__subclass(V__CLASS,s__CompoundSubstance) &
     (~ (? [V__CS2] :
         (s__instance(V__CS2,V__CLASS)
         &
         s__part(V__CS2,V__CS1))))
&
s__molecularRatio(V__ECLASS,V__N,V__CLASS)
&
s__instance(V__G,s__Group) &
s__member(V__E,V__G)
&
s__part(V__E,V__CS1)
&
s__instance(V__E,V__ECLASS))
=>
s__memberCount(V__G,V__N))
)

Cars.kif 1767-1781

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

consequent
-------------------------


No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28252-28262 An object is an instance of body part and Bare is an attribute of the object holds during an entity if and only if there doesn't exist another object such that the other object is an instance of clothing and the other object covers the object holds during the entity
No TPTP formula. May not be expressible in strict first order. Merge.kif 12318-12325 A process is an instance of combining and an object is a resource for the process and another object is a result of the process if and only if the object is not a part of the other object holds during the beginning of the time of existence of the process and the object is a part of the other object holds during the end of the time of existence of the process
( ! [V__MUSIC] :
   (s__attribute(V__MUSIC,s__PolyphonicMusic) <=>
     (? [V__PART1,V__PART2] :
       (s__instance(V__MUSIC,s__MakingMusic) &
         s__instance(V__PART1,s__MakingMusic) &
         s__instance(V__PART2,s__MakingMusic) &
         s__subProcess(V__PART1,V__MUSIC)
       &
       s__subProcess(V__PART2,V__MUSIC)
     &
     (~ (V__PART1 = V__PART2))
     &
     s__cooccur(V__PART1,V__MUSIC)
   &
   s__cooccur(V__PART2,V__MUSIC))))
)

Mid-level-ontology.kif 927-938 Polyphonic music is an attribute of an object if and only if there exist a process and another process such that the object is an instance of making music and the process is an instance of making music and the other process is an instance of making music and the process is a subprocess of the object and the other process is a subprocess of the object and the process is not equal to the other process and the process occurs at the same time as the object and the other process occurs at the same time as the object
( ! [V__WATER,V__AREA,V__DIST] :
   (s__attribute(V__WATER,s__OpenSea) <=>
     (! [V__LAND] :
       (s__instance(V__AREA,s__SaltWaterArea) &
         (~ s__instance(V__WATER,s__LandlockedWater))
         &
         s__distance(V__LAND,V__WATER,V__DIST)
       &
       s__greaterThan(V__DIST,s__MeasureFn(5,s__NauticalMile)))))
)

Geography.kif 4409-4416 Open sea is an attribute of an object if and only if for all a physical an entity is an instance of salt water area and the object is not an instance of landlocked water and the distance between the physical and the object is a length measure and the length measure is greater than 5 nautical mile(s)
( ! [V__OBJ1,V__OBJ2,V__OBJ3] :
   (s__connects(V__OBJ1,V__OBJ2,V__OBJ3)
   <=>
   (s__connected(V__OBJ1,V__OBJ2)
   &
   s__connected(V__OBJ1,V__OBJ3)
&
(~ s__connected(V__OBJ2,V__OBJ3))))
)

Merge.kif 9514-9520 An object connects another object and a third object if and only if the object is connected to the other object and the object is connected to the third object and the other object is not connected to the third object
( ! [V__P1,V__P2] :
   (s__cousin(V__P1,V__P2)
   <=>
   ((? [V__G1,V__G2] :
       (s__grandmother(V__P1,V__G1)
       &
       s__grandfather(V__P1,V__G2)
     &
     s__grandmother(V__P2,V__G1)
   &
   s__grandfather(V__P2,V__G2)))
&
(~ (? [V__M,V__F] :
(s__mother(V__P1,V__M)
&
s__father(V__P1,V__F)
&
s__mother(V__P2,V__M)
&
s__father(V__P2,V__F))))))
)

Mid-level-ontology.kif 20923-20938 A human and another human are cousins if and only if there exist a woman and a man such that the grandmother of the human is the woman and the grandfather of the human is the man and the grandmother of the other human is the woman and the grandfather of the other human is the man and there don't exist an organism and another organism such that the organism is a mother of the human and the other organism is a father of the human and the organism is a mother of the other human and the other organism is a father of the other human
No TPTP formula. May not be expressible in strict first order. People.kif 411-442 The female life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order. People.kif 323-353 The life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order. People.kif 367-398 The male life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
No TPTP formula. May not be expressible in strict first order. People.kif 174-202 The migrants per thousand of a geopolitical area and the year an integer is equal to a real number if and only if (the integer and another integer) is equal to 1 and the population of the geopolitical area is equal to a third integer holds during the year the integer and the third integer and 1000 is equal to a quantity and a fourth integer is equal to the number of instances in the class described by an organism and a fifth integer is equal to the number of instances in the class described by the organism and (the fourth integer and the fifth integer) is equal to another quantity and the other quantity and the quantity is equal to the real number
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28209-28217 Barefoot is an attribute of an animal holds during an entity if and only if there doesn't exist a wearable item such that the wearable item is an instance of shoe and the animal wears the wearable item holds during the entity
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28221-28229 Naked is an attribute of an animal holds during an entity if and only if there doesn't exist a wearable item such that the wearable item is an instance of clothing and the animal wears the wearable item holds during the entity
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28294-28305 Alone is an attribute of an object holds during an entity if and only if there don't exist another entity and a process such that a third entity is not equal to the other entity and the other entity is an instance of agent and the process is an instance of social interaction and the third entity is an involved in event of the process and the other entity is an involved in event of the process
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28338-28346 Mute is an attribute of an agent holds during a time interval if and only if there doesn't exist a process such that the process is an instance of speaking and the time of existence of the process takes place during the time interval and the agent is an agent of the process
( ! [V__COMPOUND] :
   (s__instance(V__COMPOUND,s__CompoundSubstance) <=>
     (? [V__ELEMENT1,V__ELEMENT2,V__PROCESS] :
       (s__instance(V__ELEMENT1,s__ElementalSubstance) &
         s__instance(V__ELEMENT2,s__ElementalSubstance) &
         (~ (V__ELEMENT1 = V__ELEMENT2))
         &
         s__instance(V__PROCESS,s__ChemicalSynthesis) &
         s__resource(V__PROCESS,V__ELEMENT1)
       &
       s__resource(V__PROCESS,V__ELEMENT2)
     &
     s__result(V__PROCESS,V__COMPOUND))))
)

Merge.kif 12391-12401 An entity is an instance of compound substance if and only if there exist an object, another object and a process such that the object is an instance of elemental substance and the other object is an instance of elemental substance and the object is not equal to the other object and the process is an instance of chemical synthesis and the object is a resource for the process and the other object is a resource for the process and the entity is a result of the process
( ! [V__CS] :
   (s__instance(V__CS,s__ConjugatedSubstance) <=>
     (? [V__C1,V__C2,V__P] :
       (s__instance(V__C1,s__CompoundSubstance) &
         s__instance(V__C2,s__CompoundSubstance) &
         (~ (V__C1 = V__C2))
         &
         s__instance(V__P,s__ChemicalSynthesis) &
         s__resource(V__P,V__C1)
       &
       s__resource(V__P,V__C2)
     &
     s__result(V__P,V__CS))))
)

Mid-level-ontology.kif 6166-6176 An entity is an instance of conjugated substance if and only if there exist an object, another object and a process such that the object is an instance of compound substance and the other object is an instance of compound substance and the object is not equal to the other object and the process is an instance of chemical synthesis and the object is a resource for the process and the other object is a resource for the process and the entity is a result of the process
( ! [V__GRAPH] :
   (s__instance(V__GRAPH,s__MultiGraph) <=>
     (? [V__ARC1,V__ARC2,V__NODE1,V__NODE2] :
       (s__graphPart(V__ARC1,V__GRAPH)
       &
       s__graphPart(V__ARC2,V__GRAPH)
     &
     s__graphPart(V__NODE1,V__GRAPH)
   &
   s__graphPart(V__NODE2,V__GRAPH)
&
s__links(V__NODE1,V__NODE2,V__ARC1)
&
s__links(V__NODE1,V__NODE2,V__ARC2)
&
(~ (V__ARC1 = V__ARC2)))))
)

Merge.kif 5885-5895 A graph is an instance of multi graph if and only if there exist a graph arc, another graph arc,, , a graph node and another graph node such that the graph arc is a part of the graph and the other graph arc is a part of the graph and the graph node is a part of the graph and the other graph node is a part of the graph and the graph arc links the graph node and the other graph node and the other graph arc links the graph node and the other graph node and the graph arc is not equal to the other graph arc
( ! [V__PROCESS] :
   (s__instance(V__PROCESS,s__Creation) <=>
     (? [V__PATIENT] :
       (s__patient(V__PROCESS,V__PATIENT)
       &
       s__time(V__PATIENT,s__EndFn(s__WhenFn(V__PROCESS)))
&
(~ s__time(V__PATIENT,s__BeginFn(s__WhenFn(V__PROCESS)))))))
)

Merge.kif 12669-12676 A process is an instance of creation if and only if there exists a physical such that the physical is a patient of the process and the physical exists during the end of the time of existence of the process and the physical doesn't exist during the beginning of the time of existence of the process
( ! [V__PROCESS] :
   (s__instance(V__PROCESS,s__Destruction) <=>
     (? [V__PATIENT] :
       (s__patient(V__PROCESS,V__PATIENT)
       &
       s__time(V__PATIENT,s__BeginFn(s__WhenFn(V__PROCESS)))
&
(~ s__time(V__PATIENT,s__EndFn(s__WhenFn(V__PROCESS)))))))
)

Merge.kif 12162-12169 A process is an instance of destruction if and only if there exists a physical such that the physical is a patient of the process and the physical exists during the beginning of the time of existence of the process and the physical doesn't exist during the end of the time of existence of the process
No TPTP formula. May not be expressible in strict first order. Transportation.kif 291-303 A length measure is a length of unclassified gauge railway of a geographic area if and only if the length of the class described by a physical is the length measure
( ! [V__P] :
   (s__manner(V__P,s__Harmless) <=>
     ((~ s__instance(V__P,s__Damaging))
       &
       (~ (? [V__P2] :
           (s__instance(V__P2,s__Damaging) &
             s__subProcess(V__P2,V__P))))
     &
     (~ (? [V__P2] :
         (s__instance(V__P2,s__Damaging) &
           s__causes(V__P,V__P2))))))
)

Mid-level-ontology.kif 28355-28369 A process is performed in the manner Harmless if and only if the process is not an instance of damaging and there doesn't exist the process2 such that the process2 is an instance of damaging and the process2 is a subprocess of the process and there doesn't exist the process2 such that the process2 is an instance of damaging and the process causes the process2
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11454-11461 The statement a formula has the modal force of legal if and only if there doesn't exist another formula such that the statement the other formula has the modal force of law and the other formula is not a consistent of the formula
No TPTP formula. May not be expressible in strict first order. Merge.kif 17757-17759 The statement a formula has the modal force of necessity if and only if the statement the formula doesn't have the modal force of possibility
No TPTP formula. May not be expressible in strict first order. Merge.kif 17836-17838 The statement a formula has the modal force of obligation if and only if the statement the formula doesn't have the modal force of permission
No TPTP formula. May not be expressible in strict first order. Merge.kif 17878-17880 The statement a formula has the modal force of prohibition if and only if the statement the formula doesn't have the modal force of permission

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement
-------------------------


No TPTP formula. May not be expressible in strict first order. Media.kif 2519-2520 Serbia and montenegro is not an instance of independent state holds during after the day 3

appearance as argument number 0
-------------------------


( ! [V__WINDOW] :
   (~ (s__hasGUEState(V__WINDOW,s__GUE_NonVisibleState) &
       s__hasGUEState(V__WINDOW,s__GUE_ActiveState) &
       s__instance(V__WINDOW,s__InterfaceWindow)))
   )

ComputerInput.kif 1648-1652 ~{ A GUIElement has state GUE_NonVisibleState } or ~{ the GUIElement has state GUE_ActiveState } or ~{ the GUIElement is an instance of InterfaceWindow }
( ! [V__CURSOR] :
   (~ (s__instance(V__CURSOR,s__Cursor) &
       s__hasGUEState(V__CURSOR,s__GUE_SelectedState)))
   )

ComputerInput.kif 1825-1828 ~{ A GUIElement is an instance of Cursor } or ~{ the GUIElement has state GUE_SelectedState }
( ! [V__CURSOR] :
   (~ (s__instance(V__CURSOR,s__MouseCursor) &
       s__hasGUEState(V__CURSOR,s__GUE_ActiveState)))
   )

ComputerInput.kif 1593-1596 ~{ A GUIElement is an instance of MouseCursor } or ~{ the GUIElement has state GUE_ActiveState }
(~ (s__BigSix = s__GroupOf6))

Government.kif 2852-2852 Big six is not equal to group of6
( ! [V__GRAPH,V__NUMBER1,V__NUMBER2] :
   (~ (? [V__PATH1,V__PATH2] :
       (s__instance(V__PATH1,s__CutSetFn(V__GRAPH))
     &
     s__instance(V__PATH2,s__MinimalCutSetFn(V__GRAPH))
&
s__pathLength(V__PATH1,V__NUMBER1)
&
s__pathLength(V__PATH2,V__NUMBER2)
&
s__lessThan(V__NUMBER1,V__NUMBER2))))
)

Merge.kif 6217-6224 There don't exist a graph path and another graph path such that the graph path is an instance of the set of paths that partition a graph into two separate graphs and the other graph path is an instance of the set of minimal paths that partition the graph into two separate graphs and the length of the graph path is a positive integer and the length of the other graph path is another positive integer and the positive integer is less than the other positive integer
(~ s__member(s__Denmark,s__EuropeanMonetaryUnion))

Government.kif 3156-3156 Denmark is not a member of european monetary union
(~ s__member(s__Sweden,s__EuropeanMonetaryUnion))

Government.kif 3157-3157 Sweden is not a member of european monetary union
(~ s__member(s__UnitedKingdom,s__EuropeanMonetaryUnion))

Government.kif 3158-3158 United kingdom is not a member of european monetary union
(~ s__overlapsTemporally(s__CommonEra,s__BeforeCommonEra))

Mid-level-ontology.kif 7591-7591 Before common era doesn't overlap common era
(~ s__vegetationType(s__ArcticRegion,s__BotanicalTree))

Geography.kif 3431-3431 Not botanical tree is found in arctic region


Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)



Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners