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

Formal Language: 



KB Term:  Term intersection
English Word: 

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 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