| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 290-291 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 288-289 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 286-286 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 287-287 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 283-283 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 284-284 | |
| s__instance(s__RelationExtendedToQuantities,s__SetOrClass)
|
Merge.kif 285-285 |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 297-297 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 181-181 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 171-171 | |
| No TPTP formula. May not be expressible in strict first order. | relations-it.txt 96-96 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 123-123 | |
| No TPTP formula. May not be expressible in strict first order. | arabic_format.kif 116-116 | |
| No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 179-179 | |
| No TPTP formula. May not be expressible in strict first order. | relations-de.txt 387-387 | |
| No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 136-136 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 205-205 | |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 298-298 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 4141-4141 | |
| No TPTP formula. May not be expressible in strict first order. | arabic_format.kif 566-566 | |
| No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 206-206 |
| antecedent |
|
|
| ( ! [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__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 | |
| ( ! [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 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 104-117 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 138-151 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 253-277 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 411-442 | |
| ( ! [V__LIST,V__ITEM] : ((s__LastFn(V__LIST) = V__ITEM) <=> (? [V__NUMBER] : ((s__ListLengthFn(V__LIST) = V__NUMBER) & (s__ListOrderFn(V__LIST,V__NUMBER) = V__ITEM)))) )
|
Mid-level-ontology.kif 6346-6351 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 323-353 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 367-398 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 221-238 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 174-202 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 77-86 | |
| ( ! [V__NUMBER1,V__NUMBER2,V__NUMBER] : ((s__RemainderFn(V__NUMBER1,V__NUMBER2) = V__NUMBER) <=> (s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2)) ,V__NUMBER2) ,V__NUMBER) = V__NUMBER1)) )
|
Merge.kif 5248-5250 | |
| ( ! [V__PERSON,V__AMOUNT] : ((s__WealthFn(V__PERSON) = V__AMOUNT) <=> s__monetaryValue(s__PropertyFn(V__PERSON) ,V__AMOUNT)) )
|
Merge.kif 7994-7996 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4357-4359 | |
| ( ! [V__Agent,V__Activity,V__ATIncome] : ((? [V__Income,V__Tax,V__TaxAmount] : (s__incomeEarned(V__Agent,V__Income,V__Activity) & s__amountCharged(V__Tax,V__TaxAmount) & s__causes(V__Activity,V__Tax) & (V__ATIncome = s__SubtractionFn(V__Income,V__TaxAmount)))) <=> s__afterTaxIncome(V__Agent,V__ATIncome,V__Activity)) )
|
FinancialOntology.kif 3222-3229 | |
| ( ! [V__Option,V__Time] : ((? [V__Stock,V__StockPrice,V__StrikePrice] : (s__instance(V__Option,s__Option) & s__underlier(V__Option,V__Stock) & s__price(V__Stock,V__StockPrice,V__Time) & s__strikePrice(V__Option,V__StrikePrice) & (V__StockPrice = V__StrikePrice))) <=> s__atTheMoney(V__Option,V__Time)) )
|
FinancialOntology.kif 2948-2956 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 11682-11692 | |
| ( ! [V__REGION,V__FRACTION,V__TOTAL,V__UNIT,V__AMOUNT] : ((s__arableLandArea(V__REGION,V__FRACTION) & s__greaterThanOrEqualTo(V__FRACTION,0) & s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT)) & s__instance(V__UNIT,s__UnitOfArea) & (V__AMOUNT = s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL) ,V__UNIT))) => s__arableLandArea(V__REGION,V__AMOUNT)) )
|
Geography.kif 2028-2035 | |
| ( ! [V__REGION,V__FRACTION,V__TOTAL,V__AMOUNT] : ((s__arableLandArea(V__REGION,V__FRACTION) & s__greaterThanOrEqualTo(V__FRACTION,0) & s__totalArea(V__REGION,V__TOTAL) & s__instance(V__TOTAL,s__AreaMeasure) & (V__AMOUNT = s__MultiplicationFn(V__FRACTION,V__TOTAL))) => s__arableLandArea(V__REGION,V__AMOUNT)) )
|
Geography.kif 2019-2026 | |
| No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 193-210 | |
| ( ! [V__A3,V__CURRENCY,V__A2,V__AREA] : ((s__codeMapping(s__ISO_4217_A,V__A3,V__CURRENCY) & s__codeMapping(s__ISO_3166_1_alpha_2,V__A2,V__AREA) & s__subclass(V__AREA,s__GeopoliticalArea) & (V__A2 = s__SubstringFn(V__A3,0,2))) => s__currencyType(V__AREA,V__CURRENCY)) )
|
Media.kif 2859-2865 | |
| ( ! [V__EXPERIMENT,V__CONFIDENCE,V__EXPERIMENTING,V__FORMULA] : ((s__confidenceInterval(V__EXPERIMENT,V__CONFIDENCE) & s__instance(V__EXPERIMENT,V__EXPERIMENTING) & s__instance(V__FORMULA,s__Formula) & s__patient(V__EXPERIMENT,V__FORMULA) & (V__CONFIDENCE = 100)) => s__truth(V__FORMULA,'$false__m')) )
|
UXExperimentalTerms.kif 680-687 | |
| ( ! [V__EXPERIMENT,V__CONFIDENCE,V__EXPERIMENTING,V__FORMULA] : ((s__confidenceInterval(V__EXPERIMENT,V__CONFIDENCE) & s__instance(V__EXPERIMENT,V__EXPERIMENTING) & s__instance(V__FORMULA,s__Formula) & s__patient(V__EXPERIMENT,V__FORMULA) & (V__CONFIDENCE = 100)) => s__truth(V__FORMULA,'$true__m')) )
|
UXExperimentalTerms.kif 671-678 | |
| 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__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__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__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__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__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 | |
| ( ! [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__PHYS1,V__PHYS2] : (s__cooccur(V__PHYS1,V__PHYS2) <=> (s__WhenFn(V__PHYS1) = s__WhenFn(V__PHYS2))) )
|
Merge.kif 8483-8485 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 104-117 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 138-151 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 253-277 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 411-442 | |
| ( ! [V__LIST,V__ITEM] : ((s__LastFn(V__LIST) = V__ITEM) <=> (? [V__NUMBER] : ((s__ListLengthFn(V__LIST) = V__NUMBER) & (s__ListOrderFn(V__LIST,V__NUMBER) = V__ITEM)))) )
|
Mid-level-ontology.kif 6346-6351 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 323-353 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 367-398 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 221-238 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 174-202 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 77-86 | |
| ( ! [V__NUMBER1,V__NUMBER2,V__NUMBER] : ((s__RemainderFn(V__NUMBER1,V__NUMBER2) = V__NUMBER) <=> (s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2)) ,V__NUMBER2) ,V__NUMBER) = V__NUMBER1)) )
|
Merge.kif 5248-5250 | |
| ( ! [V__BG,V__N,V__R,V__P,V__N1,V__P2,V__N2] : (s__ethnicityPercentInRegion(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 1545-1556 | |
| ( ! [V__INTERVAL1,V__INTERVAL2] : (s__finishes(V__INTERVAL1,V__INTERVAL2) <=> (s__before(s__BeginFn(V__INTERVAL2) ,s__BeginFn(V__INTERVAL1)) & (s__EndFn(V__INTERVAL2) = s__EndFn(V__INTERVAL1)))) )
|
Merge.kif 8261-8269 | |
| ( ! [V__NUMBER1,V__NUMBER2] : (s__greaterThanOrEqualTo(V__NUMBER1,V__NUMBER2) <=> ((V__NUMBER1 = V__NUMBER2) | s__greaterThan(V__NUMBER1,V__NUMBER2))) )
|
Merge.kif 1940-1944 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 28294-28305 | |
| ( ! [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 | |
| ( ! [V__CONTINENT] : (s__instance(V__CONTINENT,s__Continent) <=> ((s__Africa = V__CONTINENT) | (s__NorthAmerica = V__CONTINENT) | (s__SouthAmerica = V__CONTINENT) | (s__Antarctica = V__CONTINENT) | (s__Europe = V__CONTINENT) | (s__Asia = V__CONTINENT) | (s__Oceania = V__CONTINENT))) )
|
Geography.kif 3350-3359 | |
| 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. | Military.kif 928-941 | |
| (! [V__NUMBER] : (s__MeasureFn(V__NUMBER,s__OunceMass) = s__MeasureFn(s__DivisionFn(V__NUMBER,16) ,s__PoundMass)))
|
Mid-level-ontology.kif 10946-10949 | |
| (! [V__NUMBER] : (s__PredecessorFn(V__NUMBER) = s__SubtractionFn(V__NUMBER,1)))
|
Merge.kif 4874-4875 | |
| (! [V__NUMBER] : (s__SuccessorFn(V__NUMBER) = s__AdditionFn(V__NUMBER,1)))
|
Merge.kif 4854-4855 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3224-3227 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3229-3233 | |
| (~ (s__BigSix = s__GroupOf6))
|
Government.kif 2852-2852 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Military.kif 867-876 | |
| (s__BeginFn(s__BeforeCommonEra) = s__NegativeInfinity)
|
Mid-level-ontology.kif 7589-7589 | |
| (s__CardinalityFn(s__Continent) = 7)
|
Merge.kif 14144-14144 | |
| (s__CardinalityFn(s__NativityMagi) = 3)
|
Media.kif 2005-2005 | |
| No TPTP formula. May not be expressible in strict first order. | People.kif 462-472 | |
| (s__EndFn(s__CommonEra) = s__PositiveInfinity)
|
Mid-level-ontology.kif 7597-7597 | |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 890-901 | |
| (s__MeasureFn(0.0,s__AngularDegree) = s__MeasureFn(360.0,s__AngularDegree))
|
Merge.kif 7644-7644 | |
| (s__MeasureFn(1,s__AngularDegree) = s__MeasureFn(60,s__ArcMinute))
|
Geography.kif 382-382 | |
| (s__MeasureFn(1,s__ArcMinute) = s__MeasureFn(60,s__ArcSecond))
|
Geography.kif 401-401 | |
| (s__MeasureFn(1,s__CubicFoot) = s__MultiplicationFn(s__MeasureFn(1,s__FootLength),s__MultiplicationFn(s__MeasureFn(1,s__FootLength),s__MeasureFn(1,s__FootLength))))
|
Mid-level-ontology.kif 11223-11229 | |
| (s__MeasureFn(1,s__Fathom) = s__MeasureFn(6,s__FootLength))
|
Geography.kif 3664-3664 | |
| (s__MeasureFn(1,s__KilowattHour) = s__MeasureFn(3.6,s__MegaFn(s__Joule)))
|
Economy.kif 2012-2012 | |
| (s__MeasureFn(1,s__KilowattHour) = s__MeasureFn(3600000,s__Joule))
|
Economy.kif 2013-2013 | |
| (s__MeasureFn(1,s__MetricTon) = s__MeasureFn(2205,s__PoundMass))
|
Mid-level-ontology.kif 11195-11197 | |
| (s__MeasureFn(1,s__NauticalMile) = s__MeasureFn(1852,s__Meter))
|
Geography.kif 3684-3684 | |
| (s__MeasureFn(1,s__NauticalMile) = s__MeasureFn(6076.1,s__FootLength))
|
Geography.kif 3683-3683 | |
| (s__MeasureFn(1,s__SquareKilometer) = s__MultiplicationFn(s__MeasureFn(1,s__KiloFn(s__Meter)) ,s__MeasureFn(1,s__KiloFn(s__Meter))))
|
Geography.kif 621-622 | |
| (s__MeasureFn(1,s__SquareMeter) = s__MultiplicationFn(s__MeasureFn(1,s__Meter),s__MeasureFn(1,s__Meter)))
|
Geography.kif 3736-3737 | |
| (s__MeasureFn(1,s__SquareMile) = s__PerFn(s__MeasureFn(1,s__Mile),s__MeasureFn(1,s__Mile)))
|
Mid-level-ontology.kif 11279-11283 | |
| (s__MeasureFn(1,s__SquareYard) = s__PerFn(s__MeasureFn(1,s__YardLength),s__MeasureFn(1,s__YardLength)))
|
Mid-level-ontology.kif 11289-11293 | |
| ( ! [V__DEG] : (s__MeasureFn(V__DEG,s__ArcMinute) = s__MeasureFn(s__MultiplicationFn(60,V__DEG) ,s__ArcSecond)) )
|
Geography.kif 402-402 | |
| ( ! [V__MUMBER,V__NUMBER] : (s__MeasureFn(V__MUMBER,s__Micrometer) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,0.0000001) ,s__Meter)) )
|
Geography.kif 6450-6453 | |
| ( ! [V__NUM] : (s__MeasureFn(V__NUM,s__AngularDegree) = s__MeasureFn(s__MultiplicationFn(60,V__NUM) ,s__ArcMinute)) )
|
Geography.kif 383-383 | |
| ( ! [V__NUMBER] : (s__MeasureFn(V__NUMBER,s__Amu) = s__MeasureFn(s__MultiplicationFn(V__NUMBER,1.6605402E-24) ,s__Gram)) )
|
Merge.kif 7404-7406 | |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
|
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