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

Formal Language: 



KB Term:  Term intersection
English Word: 

  lessThan

Sigma KEE - lessThan
lessThan

appearance as argument number 1
-------------------------


s__documentation(s__lessThan__m,s__ChineseLanguage,'"(lessThan ?NUMBER1 ?NUMBER2) 是真的 以防 ?NUMBER1 的 Quantity 比 ?NUMBER2 的 Quantity 要少。"')

chinese_format.kif 1729-1730
s__documentation(s__lessThan__m,s__EnglishLanguage,'"(lessThan ?NUMBER1 ?NUMBER2) is true just in case the Quantity ?NUMBER1 is less than the Quantity ?NUMBER2."')

Merge.kif 1786-1787
s__domain(s__lessThan__m,n__1,s__Quantity)

Merge.kif 1783-1783 The number 1 argument of less than is an instance of quantity
s__domain(s__lessThan__m,n__2,s__Quantity)

Merge.kif 1784-1784 The number 2 argument of less than is an instance of quantity
s__instance(s__BinaryPredicate,s__Class)

s__instance(s__lessThan__m,s__BinaryPredicate)

Merge.kif 1778-1778 less than is an instance of binary predicate
s__instance(s__IrreflexiveRelation,s__Class)

s__instance(s__lessThan__m,s__IrreflexiveRelation)

Merge.kif 1780-1780 less than is an instance of irreflexive relation
s__instance(s__lessThan__m,s__RelationExtendedToQuantities)

s__instance(s__RelationExtendedToQuantities,s__Class)

Merge.kif 1781-1781 less than is an instance of relation extended to quantities
s__instance(s__lessThan__m,s__TransitiveRelation)

s__instance(s__TransitiveRelation,s__Class)

Merge.kif 1779-1779 less than is an instance of transitive relation
s__trichotomizingOn(s__lessThan__m,s__RealNumber)

Merge.kif 1782-1782 less than is trichotomizing on real number

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


s__format(s__ChineseLanguage,s__lessThan__m,'"%1 %n 是 lessThan %2"')

chinese_format.kif 141-141
s__format(s__EnglishLanguage,s__lessThan__m,'"%1 is %n less than %2"')

english_format.kif 142-142
s__inverse(s__greaterThan__m,s__lessThan__m)

Merge.kif 1797-1797 greater than is an inverse of less than
s__termFormat(s__ChineseLanguage,s__lessThan__m,'"少于"')

chinese_format.kif 142-142
s__termFormat(s__ChineseTraditionalLanguage,s__lessThan__m,'"少於"')

domainEnglishFormat.kif 34127-34127
s__termFormat(s__EnglishLanguage,s__lessThan__m,'"less than"')

domainEnglishFormat.kif 34126-34126

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


( ! [V__S,V__LD] :
   ((s__instance(V__S,s__RealNumber) =>
       ((((s__instance(V__LD,s__LiquidDrop) &
               s__approximateDiameter(V__LD,s__MeasureFn(V__S,s__Micrometer))
             &
             s__lessThan(n__500,V__S))
         =>
         s__instance(V__LD,s__Droplet))
       &
       (s__instance(V__LD,s__Droplet) =>
         (s__instance(V__LD,s__LiquidDrop) &
           s__approximateDiameter(V__LD,s__MeasureFn(V__S,s__Micrometer))
         &
         s__lessThan(n__500,V__S))))))
)
)

Geography.kif 7082-7088 A self connected object is an instance of liquid drop and the approximate diameter of the self connected object is a real number micrometer(s) and 500 is less than the real number if and only if the self connected object is an instance of droplet
( ! [V__Time,V__U,V__Option] :
   (((s__instance(V__Time,s__Agent) &
         s__instance(V__Time,s__TimePosition))
       =>
       (((( ? [V__Stock, V__StockPrice, V__StrikePrice] :
               ((s__instance(V__Stock,s__FinancialInstrument) &
                   s__instance(V__StockPrice,s__RealNumber) &
                   s__instance(V__StrikePrice,s__RealNumber) &
                   (s__instance(V__Option,s__CallOption) &
                     s__underlier(V__Option,V__Stock)
                   &
                   s__price(V__Stock,s__MeasureFn(V__StockPrice,V__U)
                ,V__Time)
               &
               s__instance(V__U,s__UnitOfCurrency) &
               s__strikePrice(V__Option,s__MeasureFn(V__StrikePrice,V__U))
           &
           s__lessThan(V__StockPrice,V__StrikePrice)))))
=>
s__outOfTheMoney(V__Option,V__Time))
&
(s__outOfTheMoney(V__Option,V__Time)
=>
( ? [V__Stock, V__StockPrice, V__StrikePrice] :
((s__instance(V__Stock,s__FinancialInstrument) &
   s__instance(V__StockPrice,s__RealNumber) &
   s__instance(V__StrikePrice,s__RealNumber) &
   (s__instance(V__Option,s__CallOption) &
     s__underlier(V__Option,V__Stock)
   &
   s__price(V__Stock,s__MeasureFn(V__StockPrice,V__U)
,V__Time)
&
s__instance(V__U,s__UnitOfCurrency) &
s__strikePrice(V__Option,s__MeasureFn(V__StrikePrice,V__U))
&
s__lessThan(V__StockPrice,V__StrikePrice)))))))))
)
)

FinancialOntology.kif 3012-3023 There exist a financial instrument, the financial instrumentPrice and another real number such that an agreement is an instance of call option and the financial instrument is an underlier of the agreement and the financial instrument is price the financial instrumentPrice an unit of measure(s) for an agent and the unit of measure is an instance of UnitOfCurrency and the other real number the unit of measure(s) is a strike price of the agreement and the financial instrumentPrice is less than the other real number if and only if the agent is an out of the money of the agreement
( ! [V__Time,V__U,V__Option] :
   (((s__instance(V__Time,s__Agent) &
         s__instance(V__Time,s__TimePosition))
       =>
       (((( ? [V__Stock, V__StockPrice, V__StrikePrice] :
               ((s__instance(V__Stock,s__FinancialInstrument) &
                   s__instance(V__StockPrice,s__RealNumber) &
                   s__instance(V__StrikePrice,s__RealNumber) &
                   (s__instance(V__Option,s__CallOption) &
                     s__underlier(V__Option,V__Stock)
                   &
                   s__price(V__Stock,s__MeasureFn(V__StockPrice,V__U)
                ,V__Time)
               &
               s__instance(V__U,s__UnitOfCurrency) &
               s__strikePrice(V__Option,s__MeasureFn(V__StrikePrice,V__U))
           &
           s__lessThan(V__StrikePrice,V__StockPrice)))))
=>
s__inTheMoney(V__Option,V__Time))
&
(s__inTheMoney(V__Option,V__Time)
=>
( ? [V__Stock, V__StockPrice, V__StrikePrice] :
((s__instance(V__Stock,s__FinancialInstrument) &
   s__instance(V__StockPrice,s__RealNumber) &
   s__instance(V__StrikePrice,s__RealNumber) &
   (s__instance(V__Option,s__CallOption) &
     s__underlier(V__Option,V__Stock)
   &
   s__price(V__Stock,s__MeasureFn(V__StockPrice,V__U)
,V__Time)
&
s__instance(V__U,s__UnitOfCurrency) &
s__strikePrice(V__Option,s__MeasureFn(V__StrikePrice,V__U))
&
s__lessThan(V__StrikePrice,V__StockPrice)))))))))
)
)

FinancialOntology.kif 2963-2974 There exist a financial instrument, the financial instrumentPrice and another real number such that an agreement is an instance of call option and the financial instrument is an underlier of the agreement and the financial instrument is price the financial instrumentPrice an unit of measure(s) for an agent and the unit of measure is an instance of UnitOfCurrency and the other real number the unit of measure(s) is a strike price of the agreement and the other real number is less than the financial instrumentPrice if and only if the agent is an in the money of the agreement
( ! [V__Time,V__U,V__Option] :
   (((s__instance(V__Time,s__Agent) &
         s__instance(V__Time,s__TimePosition))
       =>
       (((( ? [V__Stock, V__StockPrice, V__StrikePrice] :
               ((s__instance(V__Stock,s__FinancialInstrument) &
                   s__instance(V__StockPrice,s__RealNumber) &
                   s__instance(V__StrikePrice,s__RealNumber) &
                   (s__instance(V__Option,s__PutOption) &
                     s__underlier(V__Option,V__Stock)
                   &
                   s__price(V__Stock,s__MeasureFn(V__StockPrice,V__U)
                ,V__Time)
               &
               s__instance(V__U,s__UnitOfCurrency) &
               s__strikePrice(V__Option,s__MeasureFn(V__StrikePrice,V__U))
           &
           s__lessThan(V__StockPrice,V__StrikePrice)))))
=>
s__inTheMoney(V__Option,V__Time))
&
(s__inTheMoney(V__Option,V__Time)
=>
( ? [V__Stock, V__StockPrice, V__StrikePrice] :
((s__instance(V__Stock,s__FinancialInstrument) &
   s__instance(V__StockPrice,s__RealNumber) &
   s__instance(V__StrikePrice,s__RealNumber) &
   (s__instance(V__Option,s__PutOption) &
     s__underlier(V__Option,V__Stock)
   &
   s__price(V__Stock,s__MeasureFn(V__StockPrice,V__U)
,V__Time)
&
s__instance(V__U,s__UnitOfCurrency) &
s__strikePrice(V__Option,s__MeasureFn(V__StrikePrice,V__U))
&
s__lessThan(V__StockPrice,V__StrikePrice)))))))))
)
)

FinancialOntology.kif 2976-2987 There exist a financial instrument, the financial instrumentPrice and another real number such that an agreement is an instance of put option and the financial instrument is an underlier of the agreement and the financial instrument is price the financial instrumentPrice an unit of measure(s) for an agent and the unit of measure is an instance of UnitOfCurrency and the other real number the unit of measure(s) is a strike price of the agreement and the financial instrumentPrice is less than the other real number if and only if the agent is an in the money of the agreement
( ! [V__Time,V__U,V__Option] :
   (((s__instance(V__Time,s__Agent) &
         s__instance(V__Time,s__TimePosition))
       =>
       (((( ? [V__Stock, V__StockPrice, V__StrikePrice] :
               ((s__instance(V__Stock,s__FinancialInstrument) &
                   s__instance(V__StockPrice,s__RealNumber) &
                   s__instance(V__StrikePrice,s__RealNumber) &
                   (s__instance(V__Option,s__PutOption) &
                     s__underlier(V__Option,V__Stock)
                   &
                   s__price(V__Stock,s__MeasureFn(V__StockPrice,V__U)
                ,V__Time)
               &
               s__instance(V__U,s__UnitOfCurrency) &
               s__strikePrice(V__Option,s__MeasureFn(V__StrikePrice,V__U))
           &
           s__lessThan(V__StrikePrice,V__StockPrice)))))
=>
s__outOfTheMoney(V__Option,V__Time))
&
(s__outOfTheMoney(V__Option,V__Time)
=>
( ? [V__Stock, V__StockPrice, V__StrikePrice] :
((s__instance(V__Stock,s__FinancialInstrument) &
   s__instance(V__StockPrice,s__RealNumber) &
   s__instance(V__StrikePrice,s__RealNumber) &
   (s__instance(V__Option,s__PutOption) &
     s__underlier(V__Option,V__Stock)
   &
   s__price(V__Stock,s__MeasureFn(V__StockPrice,V__U)
,V__Time)
&
s__instance(V__U,s__UnitOfCurrency) &
s__strikePrice(V__Option,s__MeasureFn(V__StrikePrice,V__U))
&
s__lessThan(V__StrikePrice,V__StockPrice)))))))))
)
)

FinancialOntology.kif 3025-3036 There exist a financial instrument, the financial instrumentPrice and another real number such that an agreement is an instance of put option and the financial instrument is an underlier of the agreement and the financial instrument is price the financial instrumentPrice an unit of measure(s) for an agent and the unit of measure is an instance of UnitOfCurrency and the other real number the unit of measure(s) is a strike price of the agreement and the other real number is less than the financial instrumentPrice if and only if the agent is an out of the money of the agreement
( ! [V__Date,V__Balance,V__Account,V__Overdraft] :
   (((s__instance(V__Date,s__Day) &
         s__instance(V__Balance,s__RealNumber) &
         s__instance(V__Account,s__FinancialAccount) &
         s__instance(V__Overdraft,s__RealNumber))
       =>
       (((s__currentAccountBalance(V__Account,V__Date,s__MeasureFn(V__Balance,s__UnitedStatesDollar))
           &
           s__lessThan(V__Balance,n__0)
         &
         (V__Overdraft = s__SubtractionFn(n__0,V__Balance)))
     =>
     (s__overdraft(V__Account,s__MeasureFn(V__Overdraft,s__UnitedStatesDollar),V__Date)))))
)
)

FinancialOntology.kif 742-747
( ! [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__Amount,V__Date,V__Balance,V__U,V__Account] :
   (((s__instance(V__Amount,s__RealNumber) &
         s__instance(V__Date,s__Day) &
         s__instance(V__Balance,s__RealNumber))
       =>
       (((s__instance(V__Account,s__FinancialAccount) &
             s__minimumBalance(V__Account,s__UsingAnAccount,s__MeasureFn(V__Balance,V__U))
         &
         s__instance(V__U,s__UnitOfCurrency) &
         s__currentAccountBalance(V__Account,V__Date,s__MeasureFn(V__Amount,V__U))
     &
     s__lessThan(V__Amount,V__Balance))
=>
(( ? [V__Penalty] :
     ((s__instance(V__Penalty,s__Penalty) &
         s__date(V__Penalty,V__Date)
       &
       s__destination(V__Penalty,s__CurrencyFn(V__Account)))))))))
)
)

FinancialOntology.kif 661-674
( ! [V__Amount,V__MinPayment,V__U,V__Account] :
   (((s__instance(V__Amount,s__RealNumber) &
         s__instance(V__MinPayment,s__RealNumber))
       =>
       (((s__instance(V__Account,s__LiabilityAccount) &
             s__minimumPayment(V__Account,s__MeasureFn(V__MinPayment,V__U)
          ,s__MonthDuration) &
           s__instance(V__U,s__UnitOfCurrency) &
           ( ? [V__Payment, V__Month] :
             ((s__instance(V__Payment,s__Process) &
                 (s__instance(V__Month,s__Month) &
                   s__destination(V__Payment,s__CurrencyFn(V__Account))
               &
               s__paymentsPerPeriod(V__Account,s__MeasureFn(V__Amount,V__U)
            ,V__Month)
           &
           s__lessThan(V__Amount,V__MinPayment))))))
=>
(( ? [V__Penalty] :
   ((s__instance(V__Penalty,s__Penalty) &
       s__destination(V__Penalty,s__CurrencyFn(V__Account)))))))))
)
)

FinancialOntology.kif 718-734
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 320-326
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 255-260
No TPTP formula. May not be expressible in strict first order. Merge.kif 13232-13247
No TPTP formula. May not be expressible in strict first order. Merge.kif 13249-13262
( ! [V__DEPTH,V__OBJ,V__DRAFT,V__WATERWAY,V__UNIT] :
   (((s__instance(V__DEPTH,s__RealNumber) &
         s__instance(V__OBJ,s__Physical) &
         s__instance(V__DRAFT,s__RealNumber))
       =>
       (((s__instance(V__WATERWAY,s__Waterway) &
             s__depth(V__OBJ,V__WATERWAY,s__MeasureFn(V__DEPTH,V__UNIT))
         &
         s__instance(V__UNIT,s__UnitOfLength) &
         s__lessThan(V__DRAFT,V__DEPTH))
     =>
     (s__navigableForDraft(V__WATERWAY,s__MeasureFn(V__DRAFT,V__UNIT))))))
)
)

Transportation.kif 2674-2680
( ! [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 13178-13187
( ! [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 13189-13198
( ! [V__ROW7,V__ROW8,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   (((s__instance(V__Process1,s__Physical) &
         s__instance(V__Process2,s__Physical) &
         s__instance(V__Number1,s__PositiveInteger) &
         s__instance(V__Number2,s__PositiveInteger))
       =>
       (((s__processList__7(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
           &
           s__inList(V__Process1,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
       &
       s__inList(V__Process2,s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8))
   &
   (s__ListOrderFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
  ,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__7Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7,V__ROW8)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
(s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))))
)
)

( ! [V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   (((s__instance(V__Process1,s__Physical) &
         s__instance(V__Process2,s__Physical) &
         s__instance(V__Number1,s__PositiveInteger) &
         s__instance(V__Number2,s__PositiveInteger))
       =>
       (((s__processList__5(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
           &
           s__inList(V__Process1,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
       &
       s__inList(V__Process2,s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6))
   &
   (s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
  ,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__5Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
(s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))))
)
)

( ! [V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   (((s__instance(V__Process1,s__Physical) &
         s__instance(V__Process2,s__Physical) &
         s__instance(V__Number1,s__PositiveInteger) &
         s__instance(V__Number2,s__PositiveInteger))
       =>
       (((s__processList__1(V__ROW2)
           &
           s__inList(V__Process1,s__ListFn__1Fn(V__ROW2))
       &
       s__inList(V__Process2,s__ListFn__1Fn(V__ROW2))
   &
   (s__ListOrderFn(s__ListFn__1Fn(V__ROW2)
  ,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__1Fn(V__ROW2)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
(s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))))
)
)

( ! [V__ROW3,V__ROW4,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   (((s__instance(V__Process1,s__Physical) &
         s__instance(V__Process2,s__Physical) &
         s__instance(V__Number1,s__PositiveInteger) &
         s__instance(V__Number2,s__PositiveInteger))
       =>
       (((s__processList__3(V__ROW2,V__ROW3,V__ROW4)
           &
           s__inList(V__Process1,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
       &
       s__inList(V__Process2,s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4))
   &
   (s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
  ,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__3Fn(V__ROW2,V__ROW3,V__ROW4)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
(s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))))
)
)

( ! [V__ROW7,V__ROW5,V__ROW6,V__ROW3,V__ROW4,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   (((s__instance(V__Process1,s__Physical) &
         s__instance(V__Process2,s__Physical) &
         s__instance(V__Number1,s__PositiveInteger) &
         s__instance(V__Number2,s__PositiveInteger))
       =>
       (((s__processList__6(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
           &
           s__inList(V__Process1,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
       &
       s__inList(V__Process2,s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7))
   &
   (s__ListOrderFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
  ,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__6Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
(s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))))
)
)

( ! [V__ROW3,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   (((s__instance(V__Process1,s__Physical) &
         s__instance(V__Process2,s__Physical) &
         s__instance(V__Number1,s__PositiveInteger) &
         s__instance(V__Number2,s__PositiveInteger))
       =>
       (((s__processList__2(V__ROW2,V__ROW3)
           &
           s__inList(V__Process1,s__ListFn__2Fn(V__ROW2,V__ROW3))
       &
       s__inList(V__Process2,s__ListFn__2Fn(V__ROW2,V__ROW3))
   &
   (s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
  ,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__2Fn(V__ROW2,V__ROW3)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
(s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))))
)
)

( ! [V__ROW5,V__ROW3,V__ROW4,V__Process1,V__ROW2,V__Process2,V__Number1,V__Number2] :
   (((s__instance(V__Process1,s__Physical) &
         s__instance(V__Process2,s__Physical) &
         s__instance(V__Number1,s__PositiveInteger) &
         s__instance(V__Number2,s__PositiveInteger))
       =>
       (((s__processList__4(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
           &
           s__inList(V__Process1,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
       &
       s__inList(V__Process2,s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5))
   &
   (s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
  ,V__Number1)
= V__Process1)
&
(s__ListOrderFn(s__ListFn__4Fn(V__ROW2,V__ROW3,V__ROW4,V__ROW5)
,V__Number2)
= V__Process2)
&
s__lessThan(V__Number1,V__Number2))
=>
(s__earlier(s__WhenFn(V__Process1)
,s__WhenFn(V__Process2))))))
)
)

QoSontology.kif 692-708
No TPTP formula. May not be expressible in strict first order. Catalog.kif 421-436
No TPTP formula. May not be expressible in strict first order. ComputingBrands.kif 3653-3666
No TPTP formula. May not be expressible in strict first order. ComputingBrands.kif 3679-3692

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


No TPTP formula. May not be expressible in strict first order. People.kif 253-277 The deaths per thousand live births of a geopolitical area and the year an integer is equal to a real number if and only if another integer is equal to the number of instances in the class described by a symbolic string and the other integer and 1000 is equal to a number and a third integer is equal to the number of instances in the class described by another symbolic string and the third integer and the number is equal to the real number
( ! [V__NUMBER] :
   (((s__instance(V__NUMBER,s__NegativeRealNumber) =>
         (s__lessThan(V__NUMBER,n__0)
         &
         s__instance(V__NUMBER,s__RealNumber)))
     &
     ((s__lessThan(V__NUMBER,n__0)
       &
       s__instance(V__NUMBER,s__RealNumber))
     =>
     s__instance(V__NUMBER,s__NegativeRealNumber)))
)
)

Merge.kif 1895-1899 A quantity is an instance of negative real number if and only if the quantity is less than 0 and the quantity is an instance of real number
( ! [V__NUMBER1,V__NUMBER2] :
   (((s__instance(V__NUMBER1,s__Quantity) &
         s__instance(V__NUMBER2,s__Quantity))
       =>
       (((s__lessThanOrEqualTo(V__NUMBER1,V__NUMBER2)
           =>
           ((V__NUMBER1 = V__NUMBER2)
             |
             s__lessThan(V__NUMBER1,V__NUMBER2)))
       &
       (((V__NUMBER1 = V__NUMBER2)
           |
           s__lessThan(V__NUMBER1,V__NUMBER2))
       =>
       s__lessThanOrEqualTo(V__NUMBER1,V__NUMBER2)))))
)
)

Merge.kif 1814-1818 A quantity is less than or equal to another quantity if and only if the quantity is equal to the other quantity or the quantity is less than the other quantity
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 17761-17770
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 17776-17786
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 17792-17802
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 17808-17818
No TPTP formula. May not be expressible in strict first order. Dining.kif 1101-1109
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 3653-3661
No TPTP formula. May not be expressible in strict first order. Merge.kif 2564-2569
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 12780-12789
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 12708-12717
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 12719-12730
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 12670-12679
( ! [V__A,V__N] :
   ((s__instance(V__N,s__RealNumber) =>
       (((s__instance(V__A,s__AcuteAngle) &
             s__angularMeasure(V__A,s__MeasureFn(V__N,s__AngularDegree)))
         =>
         (s__lessThan(V__N,n__90)))))
)
)

Mid-level-ontology.kif 4578-4582
No TPTP formula. May not be expressible in strict first order. Dining.kif 725-748
( ! [V__AIRPORT] :
   (((s__instance(V__AIRPORT,s__Airport) &
         s__attribute(V__AIRPORT,s__VeryShortRunwayAirport))
       =>
       (( ? [V__RUNWAY, V__LENGTH] :
           ((s__instance(V__LENGTH,s__RealNumber) &
               (s__instance(V__RUNWAY,s__Runway) &
                 s__part(V__RUNWAY,V__AIRPORT)
               &
               s__length(V__RUNWAY,s__MeasureFn(V__LENGTH,s__Meter))
             &
             s__lessThan(V__LENGTH,n__914)))))))
)
)

Transportation.kif 1391-1400
( ! [V__U,V__AREA,V__ELEV1] :
   ((s__instance(V__ELEV1,s__RealNumber) =>
       (((s__instance(V__AREA,s__GeographicArea) &
             s__geographicSubregion(s__ElevationLowPointFn(V__AREA)
          ,V__AREA)
         &
         s__instance(V__U,s__UnitOfLength) &
         s__elevation(s__ElevationLowPointFn(V__AREA)
      ,s__MeasureFn(V__ELEV1,V__U)))
=>
(~(( ? [V__OTHER, V__ELEV2] :
       ((s__instance(V__OTHER,s__GeographicArea) &
           s__instance(V__ELEV2,s__RealNumber) &
           (s__geographicSubregion(V__OTHER,V__AREA)
           &
           ~((V__OTHER = s__ElevationLowPointFn(V__AREA)))
         &
         s__elevation(V__OTHER,s__MeasureFn(V__ELEV2,V__U))
     &
     s__lessThan(V__ELEV2,V__ELEV1))))))))))
)
)

Geography.kif 1911-1925
( ! [V__WEATHER,V__FRACTION,V__AREA] :
   ((s__instance(V__FRACTION,s__NonnegativeRealNumber) =>
       (((s__instance(V__AREA,s__GeographicArea) &
             s__instance(V__WEATHER,s__ClearWeather) &
             s__eventLocated(V__WEATHER,V__AREA)
           &
           s__cloudCoverFraction(V__AREA,V__FRACTION))
       =>
       (s__lessThan(V__FRACTION,n__0_3)))))
)
)

Weather.kif 892-898
( ! [V__WEATHER,V__AREA] :
   (((s__instance(V__AREA,s__GeographicArea) &
         s__instance(V__WEATHER,s__ClearWeather) &
         s__eventLocated(V__WEATHER,V__AREA))
     =>
     (( ? [V__FRACTION] :
         ((s__instance(V__FRACTION,s__NonnegativeRealNumber) &
             (s__cloudCoverFraction(V__AREA,V__FRACTION)
             &
             s__lessThan(V__FRACTION,n__0_3)))))))
)
)

Weather.kif 882-890
( ! [V__BOTTOM,V__U,V__WIDTH2,V__WIDTH1,V__TOP,V__BOTTLE] :
   (((s__instance(V__BOTTOM,s__SelfConnectedObject) &
         s__instance(V__WIDTH2,s__RealNumber) &
         s__instance(V__WIDTH1,s__RealNumber) &
         s__instance(V__TOP,s__SelfConnectedObject))
       =>
       (((s__instance(V__BOTTLE,s__Bottle) &
             s__bottom(V__BOTTOM,V__BOTTLE)
           &
           s__top(V__TOP,V__BOTTLE)
         &
         s__instance(V__U,s__UnitOfLength) &
         s__width(V__BOTTOM,s__MeasureFn(V__WIDTH1,V__U))
     &
     s__width(V__TOP,s__MeasureFn(V__WIDTH2,V__U)))
=>
(s__lessThan(V__WIDTH2,V__WIDTH1)))))
)
)

Mid-level-ontology.kif 4415-4425
No TPTP formula. May not be expressible in strict first order. Merge.kif 10517-10530
No TPTP formula. May not be expressible in strict first order. QoSontology.kif 1932-1946
No TPTP formula. May not be expressible in strict first order. Dining.kif 507-516
No TPTP formula. May not be expressible in strict first order. Merge.kif 10497-10510

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


( ! [V__NUMBER1,V__NUMBER2,V__GRAPH] :
   (((s__instance(V__NUMBER1,s__PositiveInteger) &
         s__instance(V__NUMBER2,s__PositiveInteger) &
         s__instance(V__GRAPH,s__Graph))
       =>
       (~(( ? [V__PATH1, V__PATH2] :
             ((s__instance(V__PATH1,s__GraphPath) &
                 s__instance(V__PATH2,s__GraphPath) &
                 (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 5872-5879 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


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 3.0 is open source software produced by Articulate Software and its partners