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

Formal Language: 



KB Term:  Term intersection
English Word: 

  and

Sigma KEE - and
and

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


No TPTP formula. May not be expressible in strict first order. domainEnglishFormat.kif 1669-1669

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


( ∀ [V__Account,V__Agent]
   ((s__accountHolder(V__Account,V__Agent)
     ∧
     s__instance(V__Agent,s__Corporation))
   <⇒
   s__instance(V__Account,s__CorporateAccount))
)

FinancialOntology.kif 963-967
( ∀ [V__Account,V__Agent]
   ((s__accountHolder(V__Account,V__Agent)
     ∧
     s__instance(V__Agent,s__Human))
   <⇒
   s__instance(V__Account,s__PersonalAccount))
)

FinancialOntology.kif 941-945
( ∀ [V__Account,V__Period,V__End]
   ((s__agreementPeriod(V__Account,V__Period)
     ∧
     s__finishes(V__End,V__Period))
<⇒
s__maturityDate(V__Account,V__End))
)

FinancialOntology.kif 602-606
( ∀ [V__AIRCRAFT,V__OBJ2,V__QUANTITY]
   ((s__altitude(V__AIRCRAFT,V__OBJ2,V__QUANTITY)
     ∧
     s__surface(V__OBJ2,s__PlanetEarth) ∧
     s__instance(V__AIRCRAFT,s__Aircraft))
   <⇒
   s__absoluteHeight(V__AIRCRAFT,V__QUANTITY))
)

MilitaryDevices.kif 1461-1466
( ∀ [V__INDIVIDUAL,V__CH]
   ((s__attribute(V__INDIVIDUAL,V__CH)
     ∧
     s__instance(V__CH,s__Christian))
   <⇒
   s__member(V__INDIVIDUAL,s__Christianity))
)

People.kif 797-801
( ∀ [V__NUMBER1,V__NUMBER2]
   (((s__AbsoluteValueFn(V__NUMBER1)
       = V__NUMBER2)
     ∧
     s__instance(V__NUMBER1,s__RealNumber) ∧
     s__instance(V__NUMBER2,s__RealNumber))
   <⇒
   ((s__instance(V__NUMBER1,s__NonnegativeRealNumber) ∧
       (V__NUMBER1 = V__NUMBER2))
     ∨
     (s__instance(V__NUMBER1,s__NegativeRealNumber) ∧
       (V__NUMBER2 = s__SubtractionFn(0,V__NUMBER1)))))
)

Merge.kif 4911-4922
( ∀ [V__AGENT]
   ((s__instance(V__AGENT,s__SentientAgent) ∧
       s__attribute(V__AGENT,s__Living))
     <⇒
     (∃ [V__ATTR]
       (s__instance(V__ATTR,s__ConsciousnessAttribute) ∧
         s__attribute(V__AGENT,V__ATTR))))
)

Merge.kif 18649-18656
( ∀ [V__Account,V__Agent,V__Asset]
   ((s__instance(V__Account,s__FinancialAccount) ∧
       s__possesses(V__Agent,V__Asset)
     ∧
     (V__Account = s__AccountFn(V__Asset)))
<⇒
s__accountHolder(V__Account,V__Agent))
)

FinancialOntology.kif 2252-2257
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 952-956
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28252-28262
No TPTP formula. May not be expressible in strict first order. Merge.kif 12318-12325
( ∀ [V__LD,V__S]
   ((s__instance(V__LD,s__LiquidDrop) ∧
       s__approximateDiameter(V__LD,s__MeasureFn(V__S,s__Micrometer))
     ∧
     s__lessThan(500,V__S))
<⇒
s__instance(V__LD,s__Droplet))
)

Geography.kif 6905-6911
( ∀ [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
( ∀ [V__PM,V__P,V__S]
   ((s__instance(V__PM,s__ParticulateMatter) ∧
       s__part(V__P,V__PM)
     ∧
     s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
   ∧
   s__greaterThan(10,V__S)

s__greaterThan(V__S,2.5))
<⇒
(∃ [V__PM10]
(s__instance(V__PM10,s__CoarseParticulateMatter) ∧
s__part(V__PM10,V__PM))))
)

Geography.kif 6821-6832
( ∀ [V__PM,V__P,V__S]
   ((s__instance(V__PM,s__ParticulateMatter) ∧
       s__part(V__P,V__PM)
     ∧
     s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
   ∧
   s__greaterThanOrEqualTo(V__S,2.5))
<⇒
(∃ [V__PM25]
(s__instance(V__PM25,s__FineParticulateMatter) ∧
   s__part(V__PM25,V__PM))))
)

Geography.kif 6850-6860
( ∀ [V__ROW1]
   ((s__instance(s__duration__m,s__TotalValuedRelation) ∧
       s__instance(s__duration__m,s__Predicate))
     <⇒
     (∃ [V__VALENCE]
       (s__instance(s__duration__m,s__Relation) ∧
         s__valence(s__duration__m,V__VALENCE)
       ∧
       ((∀ [V__NUMBER,V__ELEMENT,V__CLASS]
           ((s__lessThan(V__NUMBER,V__VALENCE)
             ∧
             s__domain(s__duration__m,V__NUMBER,V__CLASS)
           ∧
           (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
          ,V__NUMBER)))
     ⇒
     s__instance(V__ELEMENT,V__CLASS)))

(∃ [V__ITEM]
s__duration(V__ROW1,V__ITEM))))))
)

Merge.kif 2318-2335
( ∀ [V__SCROLL]
   ((s__instance(V__SCROLL,s__WindowScrolling) ∧
       s__instance(V__SCROLL,s__UserSignifiedGraphicalAction))
     <⇒
     s__instance(V__SCROLL,s__WindowScrollingByUser))
   )

ComputerInput.kif 1447-1451
( ∀ [V__UNIT,V__AMOUNT]
   ((s__instance(V__UNIT,s__UnitOfMeasure) ∧
       (V__AMOUNT = s__MeasureFn(1,s__SquareUnitFn(V__UNIT))))
<⇒
(V__AMOUNT = s__MultiplicationFn(s__MeasureFn(1,V__UNIT)
,s__MeasureFn(1,V__UNIT))))
)

Geography.kif 3748-3752
( ∀ [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
No TPTP formula. May not be expressible in strict first order. Weather.kif 1086-1096
( ∀ [V__PLACE,V__AREA]
   ((s__located(V__PLACE,V__AREA)
     ∧
     s__instance(V__PLACE,s__PostalPlace) ∧
     s__instance(V__AREA,s__PostcodeArea))
   <⇒
   s__postPostcodeArea(V__PLACE,V__AREA))
)

Mid-level-ontology.kif 22553-22558
( ∀ [V__PLACE,V__GEO]
   ((s__located(V__PLACE,V__GEO)
     ∧
     s__instance(V__PLACE,s__PostalPlace) ∧
     s__instance(V__GEO,s__City))
   <⇒
   s__postCity(V__PLACE,V__GEO))
)

Mid-level-ontology.kif 22526-22531
( ∀ [V__PLACE,V__GEO]
   ((s__located(V__PLACE,V__GEO)
     ∧
     s__instance(V__PLACE,s__PostalPlace) ∧
     s__instance(V__GEO,s__Neighborhood))
   <⇒
   s__postNeighborhood(V__PLACE,V__GEO))
)

Mid-level-ontology.kif 22439-22444
( ∀ [V__PLACE,V__GEO]
   ((s__located(V__PLACE,V__GEO)
     ∧
     s__instance(V__PLACE,s__PostalPlace) ∧
     s__instance(V__GEO,s__StateOrProvince))
   <⇒
   s__postDistrict(V__PLACE,V__GEO))
)

Mid-level-ontology.kif 22510-22515
( ∀ [V__PLACE,V__GEO]
   ((s__located(V__PLACE,V__GEO)
     ∧
     s__instance(V__PLACE,s__PostalPlace) ∧
     (s__instance(V__GEO,s__Nation) ∨
       s__instance(V__GEO,s__DependencyOrSpecialSovereigntyArea)))
   <⇒
   s__postCountry(V__PLACE,V__GEO))
)

Mid-level-ontology.kif 22476-22483

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


( ∀ [V__NUMBER1,V__NUMBER2]
   (((s__AbsoluteValueFn(V__NUMBER1)
       = V__NUMBER2)
     ∧
     s__instance(V__NUMBER1,s__RealNumber) ∧
     s__instance(V__NUMBER2,s__RealNumber))
   <⇒
   ((s__instance(V__NUMBER1,s__NonnegativeRealNumber) ∧
       (V__NUMBER1 = V__NUMBER2))
     ∨
     (s__instance(V__NUMBER1,s__NegativeRealNumber) ∧
       (V__NUMBER2 = s__SubtractionFn(0,V__NUMBER1)))))
)

Merge.kif 4911-4922
( ∀ [V__AGENT]
   ((s__instance(V__AGENT,s__SentientAgent) ∧
       s__attribute(V__AGENT,s__Living))
     <⇒
     (∃ [V__ATTR]
       (s__instance(V__ATTR,s__ConsciousnessAttribute) ∧
         s__attribute(V__AGENT,V__ATTR))))
)

Merge.kif 18649-18656
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28252-28262
No TPTP formula. May not be expressible in strict first order. Merge.kif 12318-12325
( ∀ [V__PM,V__P,V__S]
   ((s__instance(V__PM,s__ParticulateMatter) ∧
       s__part(V__P,V__PM)
     ∧
     s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
   ∧
   s__greaterThan(10,V__S)

s__greaterThan(V__S,2.5))
<⇒
(∃ [V__PM10]
(s__instance(V__PM10,s__CoarseParticulateMatter) ∧
s__part(V__PM10,V__PM))))
)

Geography.kif 6821-6832
( ∀ [V__PM,V__P,V__S]
   ((s__instance(V__PM,s__ParticulateMatter) ∧
       s__part(V__P,V__PM)
     ∧
     s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
   ∧
   s__greaterThanOrEqualTo(V__S,2.5))
<⇒
(∃ [V__PM25]
(s__instance(V__PM25,s__FineParticulateMatter) ∧
   s__part(V__PM25,V__PM))))
)

Geography.kif 6850-6860
( ∀ [V__ROW1]
   ((s__instance(s__duration__m,s__TotalValuedRelation) ∧
       s__instance(s__duration__m,s__Predicate))
     <⇒
     (∃ [V__VALENCE]
       (s__instance(s__duration__m,s__Relation) ∧
         s__valence(s__duration__m,V__VALENCE)
       ∧
       ((∀ [V__NUMBER,V__ELEMENT,V__CLASS]
           ((s__lessThan(V__NUMBER,V__VALENCE)
             ∧
             s__domain(s__duration__m,V__NUMBER,V__CLASS)
           ∧
           (V__ELEMENT = s__ListOrderFn(s__ListFn_1(V__ROW1)
          ,V__NUMBER)))
     ⇒
     s__instance(V__ELEMENT,V__CLASS)))

(∃ [V__ITEM]
s__duration(V__ROW1,V__ITEM))))))
)

Merge.kif 2318-2335
No TPTP formula. May not be expressible in strict first order. Weather.kif 1086-1096
No TPTP formula. May not be expressible in strict first order. Economy.kif 1523-1528
No TPTP formula. May not be expressible in strict first order. Economy.kif 1494-1499
( ∀ [V__H]
   (s__attribute(V__H,s__LiteracyAttribute) <⇒
     (s__hasSkill(s__Reading,V__H)
     ∧
     s__hasSkill(s__Writing,V__H)))
)

Mid-level-ontology.kif 12702-12706
( ∀ [V__HOLE1]
   (s__attribute(V__HOLE1,s__Fillable) <⇒
     (∃ [V__HOLE2]
       (s__instance(V__HOLE2,s__Hole) ∧
         s__part(V__HOLE1,V__HOLE2))))
)

Merge.kif 9934-9939
( ∀ [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
( ∀ [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
( ∀ [V__A,V__H]
   (s__aunt(V__A,V__H)
   <⇒
   (∃ [V__P]
     (s__sister(V__A,V__P)
     ∧
     s__parent(V__H,V__P))))
)

Mid-level-ontology.kif 20908-20913
( ∀ [V__LIST1,V__AVERAGE,V__LASTPLACE]
   (s__average(V__LIST1,V__AVERAGE)
   <⇒
   (∃ [V__LIST2]
     ((s__ListLengthFn(V__LIST2)
       = s__ListLengthFn(V__LIST1))
   ∧
   (s__ListOrderFn(V__LIST2,1)
   = s__ListOrderFn(V__LIST1,1))

(∀ [V__ITEMFROM2]
(s__inList(V__ITEMFROM2,V__LIST2)

(∃ [V__POSITION,V__POSITIONMINUSONE,V__ITEMFROM1,V__PRIORFROM2]
   (s__greaterThan(V__POSITION,1)
   ∧
   s__lessThanOrEqualTo(V__POSITION,s__ListLengthFn(V__LIST2))

(s__ListOrderFn(V__LIST2,V__ITEMFROM2)
= V__POSITION)

s__inList(V__ITEMFROM1,V__LIST1)

(V__POSITION = s__ListOrderFn(V__LIST1,V__ITEMFROM1))

s__inList(V__PRIORFROM2,V__LIST2)

(V__POSITIONMINUSONE = s__SubtractionFn(V__POSITION,1))

(V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2))

(V__ITEMFROM2 = s__AdditionFn(V__ITEMFROM1,V__PRIORFROM2))))))

(V__LASTPLACE = s__ListLengthFn(V__LIST2))

(V__AVERAGE = s__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__LASTPLACE)))))
)

People.kif 285-306
( ∀ [V__AccountType,V__Bank]
   (s__bankAccount(V__AccountType,V__Bank)
   <⇒
   (∃ [V__Account]
     (s__instance(V__Account,V__AccountType)
     ∧
     s__accountAt(V__Account,V__Bank))))
)

FinancialOntology.kif 3779-3784
( ∀ [V__BG,V__N,V__R,V__P,V__N1,V__P2,V__N2]
   (s__beliefGroupPercentInRegion(V__BG,V__N,V__R)
   <⇒
   (∃ [V__G1,V__G2]
     (s__located(V__P,V__R)
     ∧
     s__member(V__P,V__BG)
   ∧
   s__member(V__P,V__G1)

s__memberCount(V__G1,V__N1)

s__located(V__P2,V__R)

s__member(V__P2,V__G2)

s__memberCount(V__G2,V__N2)

(s__DivisionFn(V__N,100)
= s__DivisionFn(V__N1,V__N2)))))
)

People.kif 1526-1537
No TPTP formula. May not be expressible in strict first order. Economy.kif 1569-1574
( ∀ [V__E,V__R,V__MIN,V__M,V__MAX]
   (s__compressionRatio(V__E,V__R)
   <⇒
   (s__minCylinderVolume(V__E,s__MeasureFn(V__MIN,V__M))

s__maxCylinderVolume(V__E,s__MeasureFn(V__MAX,V__M))

(V__R = s__DivisionFn(V__MIN,V__MAX))))
)

Cars.kif 1917-1922
( ∀ [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
( ∀ [V__OBJ1,V__OBJ2]
   (s__contains(V__OBJ1,V__OBJ2)
   <⇒
   (∃ [V__HOLE]
     (s__hole(V__HOLE,V__OBJ1)
     ∧
     s__properlyFills(V__OBJ2,V__HOLE))))
)

Merge.kif 1046-1051
( ∀ [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
No TPTP formula. May not be expressible in strict first order. Economy.kif 3664-3669
No TPTP formula. May not be expressible in strict first order. Economy.kif 3671-3676

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. Government.kif 1202-1209
No TPTP formula. May not be expressible in strict first order. Government.kif 916-924
No TPTP formula. May not be expressible in strict first order. Government.kif 1069-1078
No TPTP formula. May not be expressible in strict first order. Government.kif 1129-1141
No TPTP formula. May not be expressible in strict first order. WMD.kif 870-878
No TPTP formula. May not be expressible in strict first order. Military.kif 867-876
No TPTP formula. May not be expressible in strict first order. People.kif 462-472
No TPTP formula. May not be expressible in strict first order. Military.kif 890-901
No TPTP formula. May not be expressible in strict first order. People.kif 49-54
No TPTP formula. May not be expressible in strict first order. Military.kif 928-941
(∃ [V__T]
   (s__subclass(V__T,s__HandToolBox) ∧
     s__manufacturer(s__SortimoCorp,V__T)))

Cars.kif 5080-5083
No TPTP formula. May not be expressible in strict first order. Media.kif 1972-1980
No TPTP formula. May not be expressible in strict first order. WMD.kif 761-767
( ∀ [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
( ∀ [V__CURSOR]
   (¬ (s__instance(V__CURSOR,s__Cursor) ∧
       s__hasGUEState(V__CURSOR,s__GUE_SelectedState)))
   )

ComputerInput.kif 1825-1828
( ∀ [V__CURSOR]
   (¬ (s__instance(V__CURSOR,s__MouseCursor) ∧
       s__hasGUEState(V__CURSOR,s__GUE_ActiveState)))
   )

ComputerInput.kif 1593-1596
( ∀ [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


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

Show without tree


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