| No TPTP formula. May not be expressible in strict first order. |
FinancialOntology.kif 961-965 |
An entity is an instance of personal account and the number of instances in the class described by a symbolic string is greater than 1 if and only if the entity is an instance of joint account |
( ! [V__P,V__S,V__PM] :
(((s__instance(V__P,s__SelfConnectedObject) &
s__instance(V__S,s__RealNumber))
=>
((((s__instance(V__PM,s__ParticulateMatter) &
s__part(V__P,V__PM)
&
s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
&
s__greaterThan(n__10,V__S)
&
s__greaterThan(V__S,n__2_5))
=>
( ? [V__PM10] :
((s__instance(V__PM10,s__CoarseParticulateMatter) &
s__part(V__PM10,V__PM)))))
&
(( ? [V__PM10] :
((s__instance(V__PM10,s__CoarseParticulateMatter) &
s__part(V__PM10,V__PM))))
=>
(s__instance(V__PM,s__ParticulateMatter) &
s__part(V__P,V__PM)
&
s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
&
s__greaterThan(n__10,V__S)
&
s__greaterThan(V__S,n__2_5))))))
)
)
|
Geography.kif 6998-7009 |
An object is an instance of PM and a self connected object is a part of the object and the approximate diameter of the self connected object is a real number micrometer(s) and 10 is greater than the real number and the real number is greater than 2.5 if and only if there exists the object10 such that the object10 is an instance of PM10 and the object10 is a part of the object |
| No TPTP formula. May not be expressible in strict first order. |
Cars.kif 809-825 |
|
( ! [V__TEXT,V__EDITION1,V__CBO2,V__EDITION2,V__CBO1,V__INT2,V__PUB2,V__DATE1,V__INT1,V__DATE2,V__PUB1] :
(((s__subclass(V__TEXT,s__ContentBearingObject) &
s__subclass(V__EDITION1,s__ContentBearingObject) &
s__instance(V__EDITION1,s__Class) &
s__subclass(V__EDITION2,s__ContentBearingObject) &
s__instance(V__EDITION2,s__Class) &
s__instance(V__INT2,s__PositiveInteger) &
s__instance(V__DATE1,s__Day) &
s__instance(V__INT1,s__PositiveInteger) &
s__instance(V__DATE2,s__Day))
=>
((((s__EditionFn(V__TEXT,V__INT1)
= V__EDITION1)
&
(s__EditionFn(V__TEXT,V__INT2)
= V__EDITION2)
&
s__greaterThan(V__INT2,V__INT1)
&
s__instance(V__PUB1,s__Publication) &
s__instance(V__PUB2,s__Publication) &
s__instance(V__CBO1,V__EDITION1)
&
s__instance(V__CBO2,V__EDITION2)
&
s__patient(V__PUB1,V__CBO1)
&
s__patient(V__PUB2,V__CBO2)
&
s__date(V__PUB1,V__DATE1)
&
s__date(V__PUB2,V__DATE2))
=>
(s__before(s__EndFn(V__DATE1)
,s__EndFn(V__DATE2))))))
)
)
|
Merge.kif 14744-14761 |
|
( ! [V__A,V__L] :
(((s__instance(V__A,s__Number) &
s__instance(V__L,s__List))
=>
((((V__A = s__AverageFn(V__L))
&
s__greaterThan(s__ListLengthFn(V__L)
,n__0))
=>
((V__A = s__DivisionFn(s__ListSumFn(V__L)
,s__ListLengthFn(V__L)))))))
)
)
|
Merge.kif 3168-3175 |
|
( ! [V__A,V__L] :
(((s__instance(V__A,s__Number) &
s__instance(V__L,s__List))
=>
((((V__A = s__ListSumFn(V__L))
&
s__greaterThan(s__ListLengthFn(V__L)
,n__1))
=>
((V__A = s__AdditionFn(s__FirstFn(V__L)
,s__ListSumFn(s__SubListFn(n__2,s__ListLengthFn(V__L)
,V__L))))))))
)
)
|
Merge.kif 3149-3159 |
|
( ! [V__OUT,V__IN,V__S,V__PIVOT,V__LEN,V__NEW,V__N] :
(((s__instance(V__OUT,s__SymbolicString) &
s__instance(V__IN,s__SymbolicString) &
s__instance(V__S,s__SymbolicString) &
s__instance(V__PIVOT,s__Integer) &
s__instance(V__LEN,s__NonnegativeInteger) &
s__instance(V__NEW,s__NonnegativeInteger) &
s__instance(V__N,s__NonnegativeInteger))
=>
((((V__OUT = s__ReverseFn(V__IN))
&
(V__LEN = s__StringLengthFn(V__IN))
&
s__greaterThan(V__LEN,n__1)
&
s__greaterThan(V__N,n__0)
&
s__lessThan(V__N,V__LEN)
&
(V__PIVOT = s__CeilingFn(s__DivisionFn(s__SubtractionFn(V__LEN,n__1)
,n__2)))
&
(V__NEW = s__AdditionFn(s__SubtractionFn(V__PIVOT,V__N)
,V__PIVOT))
&
(V__S = s__SubstringFn(V__IN,V__N,s__AdditionFn(n__1,V__N))))
=>
((V__S = s__SubstringFn(V__OUT,V__NEW,s__AdditionFn(n__1,V__NEW)))))))
)
)
|
Media.kif 3038-3059 |
|
( ! [V__R,V__S,V__E,V__L] :
(((s__instance(V__R,s__List) &
s__instance(V__S,s__Integer) &
s__instance(V__E,s__Integer) &
s__instance(V__L,s__List))
=>
((((V__R = s__SubListFn(V__S,V__E,V__L))
&
s__greaterThan(s__SubtractionFn(V__E,V__S)
,n__1))
=>
((V__R = s__ListConcatenateFn(s__ListFn__1Fn(s__ListOrderFn(V__L,V__S))
,s__SubListFn(s__AdditionFn(n__1,V__S)
,V__E,V__L)))))))
)
)
|
Merge.kif 3085-3097 |
|
( ! [V__VA,V__L,V__M] :
(((s__instance(V__VA,s__Number) &
s__instance(V__L,s__List) &
s__instance(V__M,s__Number))
=>
((((V__VA = s__VarianceAverageFn(V__M,V__L))
&
s__greaterThan(s__ListLengthFn(V__L)
,n__1))
=>
((V__VA = s__AdditionFn(s__VarianceAverageFn(V__M,s__ListOrderFn(V__L,n__1))
,s__VarianceAverageFn(V__M,s__SubListFn(n__2,s__ListLengthFn(V__L)
,V__L))))))))
)
)
|
Weather.kif 1452-1464 |
|
( ! [V__COUNT,V__HOME,V__REGISTER,V__MM] :
(((s__instance(V__COUNT,s__NonnegativeInteger) &
s__instance(V__HOME,s__GeopoliticalArea) &
s__instance(V__REGISTER,s__ShipRegister) &
s__instance(V__MM,s__MerchantMarine))
=>
(((s__fOCShipsByOrigin(V__MM,V__HOME,V__COUNT)
&
s__greaterThan(V__COUNT,n__0)
&
s__marineInventory(V__MM,V__REGISTER))
=>
(s__instance(V__REGISTER,s__FlagOfConvenienceRegister)))))
)
)
|
Transportation.kif 1070-1075 |
|
| No TPTP formula. May not be expressible in strict first order. |
Cars.kif 2898-2916 |
|
( ! [V__MO,V__AREA,V__TEMP] :
(((s__instance(V__MO,s__Class) &
s__instance(V__MO,s__TimeDuration) &
s__instance(V__TEMP,s__RealNumber))
=>
(((s__instance(V__AREA,s__DesertClimateZone) &
s__subclass(V__MO,s__Month) &
s__averageTemperatureForPeriod(V__AREA,V__MO,s__MeasureFn(V__TEMP,s__CelsiusDegree))
&
s__greaterThan(V__TEMP,n__18))
=>
(s__instance(V__AREA,s__SubtropicalDesertClimateZone)))))
)
)
|
Geography.kif 1360-1367 |
|
( ! [V__MO,V__AREA,V__TEMP] :
(((s__instance(V__MO,s__Class) &
s__instance(V__MO,s__TimeDuration) &
s__instance(V__TEMP,s__RealNumber))
=>
(((s__instance(V__AREA,s__GeographicArea) &
s__subclass(V__MO,s__Month) &
s__averageTemperatureForPeriod(V__AREA,V__MO,s__MeasureFn(V__TEMP,s__CelsiusDegree))
&
s__greaterThan(n__10,V__TEMP))
=>
(s__instance(V__AREA,s__PolarClimateZone)))))
)
)
|
Geography.kif 1546-1553 |
|
( ! [V__OFFER1,V__U,V__OFFER2,V__ITEM,V__BIDDER2,V__BIDDER1,V__AUCTIONING] :
(((s__instance(V__OFFER1,s__RealNumber) &
s__instance(V__OFFER2,s__RealNumber))
=>
(((s__instance(V__AUCTIONING,s__Auctioning) &
s__instance(V__BIDDER1,s__Agent) &
s__instance(V__BIDDER2,s__Agent) &
s__instance(V__ITEM,s__Object) &
s__instance(V__U,s__UnitOfCurrency) &
s__patient(V__AUCTIONING,V__ITEM)
&
s__bidPrice(V__ITEM,s__MeasureFn(V__OFFER1,V__U)
,V__BIDDER1)
&
s__bidPrice(V__ITEM,s__MeasureFn(V__OFFER2,V__U)
,V__BIDDER2)
&
s__greaterThan(V__OFFER1,V__OFFER2))
=>
(s__destination(V__AUCTIONING,V__BIDDER1)))))
)
)
|
UXExperimentalTerms.kif 437-448 |
|
( ! [V__N1,V__N2,V__Y,V__D1,V__T1,V__D2,V__T2,V__M] :
(((s__instance(V__N1,s__PositiveInteger) &
s__instance(V__N2,s__PositiveInteger) &
s__instance(V__Y,s__Integer) &
s__instance(V__D1,s__TimeInterval) &
s__instance(V__T1,s__TimePoint) &
s__instance(V__D2,s__TimeInterval) &
s__instance(V__T2,s__TimePoint) &
s__subclass(V__M,s__Month))
=>
(((s__instance(V__D1,s__DayFn(V__N1,s__MonthFn(V__M,s__YearFn(V__Y))))
&
s__instance(V__D2,s__DayFn(V__N2,s__MonthFn(V__M,s__YearFn(V__Y))))
&
(V__T1 = s__BeginFn(V__D1))
&
(V__T2 = s__BeginFn(V__D2))
&
s__greaterThan(V__N2,V__N1))
=>
(s__before(V__T1,V__T2)))))
)
)
|
Merge.kif 8332-8339 |
|
( ! [V__N1,V__N2,V__Y,V__D1,V__D2,V__M] :
(((s__instance(V__N1,s__PositiveInteger) &
s__instance(V__N2,s__PositiveInteger) &
s__instance(V__Y,s__Integer) &
s__instance(V__D1,s__TimeInterval) &
s__instance(V__D2,s__TimeInterval) &
s__subclass(V__M,s__Month))
=>
(((s__instance(V__D1,s__DayFn(V__N1,s__MonthFn(V__M,s__YearFn(V__Y))))
&
s__instance(V__D2,s__DayFn(V__N2,s__MonthFn(V__M,s__YearFn(V__Y))))
&
s__greaterThan(V__N2,V__N1))
=>
(s__earlier(V__D1,V__D2)))))
)
)
|
Merge.kif 8341-8346 |
|
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 320-326 |
|
( ! [V__HARBOR,V__NUM] :
((s__instance(V__NUM,s__Quantity) =>
(((s__instance(V__HARBOR,s__Harbor) &
s__equipmentCount(V__HARBOR,s__ShipBerth,V__NUM)
&
s__greaterThan(V__NUM,n__0))
=>
(s__capability(s__ShipBerthing,s__path__m,V__HARBOR)))))
)
)
|
Transportation.kif 2949-2954 |
|
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13199-13214 |
|
( ! [V__SZ,V__X] :
(((s__instance(V__SZ,s__SurfZone) &
s__instance(V__X,s__LengthMeasure) &
s__significantWaveHeight(V__SZ,s__WhenFn(V__SZ)
,s__MeasureFn(V__X,s__FootLength))
&
s__greaterThan(V__X,n__8))
=>
(s__attribute(V__SZ,s__RedFlagSwimmingCondition)))
)
)
|
Weather.kif 1396-1404 |
|
( ! [V__PRES,V__X,V__BOIL,V__Y,V__TEMP] :
(((s__instance(V__PRES,s__RealNumber) &
s__instance(V__X,s__Object) &
s__instance(V__BOIL,s__RealNumber) &
s__instance(V__Y,s__Class) &
s__subclass(V__Y,s__PureSubstance) &
s__instance(V__TEMP,s__RealNumber))
=>
(((s__instance(V__X,V__Y)
&
s__subclass(V__Y,s__PureSubstance) &
s__barometricPressure(V__X,s__MeasureFn(V__PRES,s__InchMercury))
&
s__greaterThan(n__29_92,V__PRES)
&
s__boilingPoint(V__Y,s__MeasureFn(V__BOIL,s__KelvinDegree))
&
s__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
&
s__greaterThan(V__TEMP,V__BOIL))
=>
(s__attribute(V__X,s__Gas)))))
)
)
|
Merge.kif 13134-13143 |
|
( ! [V__MELT,V__X,V__BOIL,V__Y,V__TEMP] :
(((s__instance(V__MELT,s__RealNumber) &
s__instance(V__X,s__Object) &
s__instance(V__BOIL,s__RealNumber) &
s__instance(V__Y,s__Class) &
s__subclass(V__Y,s__PureSubstance) &
s__instance(V__TEMP,s__RealNumber))
=>
(((s__instance(V__X,V__Y)
&
s__subclass(V__Y,s__PureSubstance) &
s__boilingPoint(V__Y,s__MeasureFn(V__BOIL,s__KelvinDegree))
&
s__meltingPoint(V__Y,s__MeasureFn(V__MELT,s__KelvinDegree))
&
s__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
&
s__greaterThan(V__TEMP,V__MELT)
&
s__lessThan(V__TEMP,V__BOIL))
=>
(s__attribute(V__X,s__Liquid)))))
)
)
|
Merge.kif 13145-13154 |
|
( ! [V__PRES,V__MELT,V__X,V__Y,V__TEMP] :
(((s__instance(V__PRES,s__RealNumber) &
s__instance(V__MELT,s__RealNumber) &
s__instance(V__X,s__Object) &
s__instance(V__Y,s__Class) &
s__subclass(V__Y,s__PureSubstance) &
s__instance(V__TEMP,s__RealNumber))
=>
(((s__instance(V__X,V__Y)
&
s__subclass(V__Y,s__PureSubstance) &
s__meltingPoint(V__Y,s__MeasureFn(V__MELT,s__KelvinDegree))
&
s__barometricPressure(V__X,s__MeasureFn(V__PRES,s__InchMercury))
&
s__greaterThan(V__PRES,n__29_92)
&
s__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
&
s__lessThan(V__TEMP,V__MELT))
=>
(s__attribute(V__X,s__Solid)))))
)
)
|
Merge.kif 13156-13165 |
|
( ! [V__N1,V__N2,V__Y1,V__Y2,V__T1,V__T2] :
(((s__instance(V__N1,s__Integer) &
s__instance(V__N2,s__Integer) &
s__instance(V__Y1,s__TimeInterval) &
s__instance(V__Y2,s__TimeInterval) &
s__instance(V__T1,s__TimePoint) &
s__instance(V__T2,s__TimePoint))
=>
(((s__instance(V__Y1,s__YearFn(V__N1))
&
s__instance(V__Y2,s__YearFn(V__N2))
&
(V__T1 = s__BeginFn(V__Y1))
&
(V__T2 = s__BeginFn(V__Y2))
&
s__greaterThan(V__N2,V__N1))
=>
(s__before(V__T1,V__T2)))))
)
)
|
Merge.kif 8300-8307 |
|
( ! [V__N1,V__N2,V__Y1,V__Y2] :
(((s__instance(V__N1,s__Integer) &
s__instance(V__N2,s__Integer) &
s__instance(V__Y1,s__TimeInterval) &
s__instance(V__Y2,s__TimeInterval))
=>
(((s__instance(V__Y1,s__YearFn(V__N1))
&
s__instance(V__Y2,s__YearFn(V__N2))
&
s__greaterThan(V__N2,V__N1))
=>
(s__earlier(V__Y1,V__Y2)))))
)
)
|
Merge.kif 8309-8314 |
|
|
| Display limited to 25 items. Show next 25 |
|
| Display limited to 25 items. Show next 25 |
