TreeView Knowledge Base Browser

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	If a financial account current account balance a day for a real number united states dollar(s) and the real number is less than 0 and another real number is equal to (0 and the real number), then the financial account is overdraft the other real number united states dollar(s) for the day
( ! [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	If a symbolic string is equal to the reverse of another symbolic string and a nonnegative integer is equal to the length of the other symbolic string and the nonnegative integer is greater than 1 and another nonnegative integer is greater than 0 and the other nonnegative integer is less than the nonnegative integer and an integer is equal to the ceiling of (the nonnegative integer and 1) and 2 and the other nonnegative integerEW is equal to ((the integer and the other nonnegative integer) and the integer) and a third symbolic string is equal to the sub-string of the other symbolic string from the other nonnegative integer to (1 and the other nonnegative integer), then the third symbolic string is equal to the sub-string of the symbolic string from the other nonnegative integerEW to (1 and the other nonnegative integerEW)
( ! [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	If a financial account is an instance of financial account and the financial account is minimum balance using an account for a real number an unit of measure(s) and the unit of measure is an instance of UnitOfCurrency and the financial account current account balance a day for another real number the unit of measure(s) and the other real number is less than the real number, then there exists a process such that the process is an instance of penalty and date of the process is the day and the process ends up at the currency of the financial account
( ! [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	If a liability account is an instance of liability account and the liability account is minimum payment a real number an unit of measure(s) for month duration and the unit of measure is an instance of UnitOfCurrency and there exist a process and a time interval such that the time interval is an instance of month and the process ends up at the currency of the liability account and the liability account payments per period another real number the unit of measure(s) for the time interval and the other real number is less than the real number, then there exists another process such that the other process is an instance of penalty and the other process ends up at the currency of the liability account
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 320-326	If an entity is an instance of human and the age of the entity is a quantity year duration(s) holds during a time position and the quantity is greater than 12 and the quantity is less than 20, then the entity is an instance of teenager holds during the time position
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 255-260	If an entity is an instance of human and the age of the entity is a quantity year duration(s) holds during a time position and the quantity is less than 18, then the entity is an instance of human youth holds during the time position
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13232-13247	If an entity is an instance of a kind of pure substance and a real number an unit of measure(s) is a boiling point of a kind of pure substance and another real number the unit of measure(s) is a melting point of the kind of pure substance and the unit of measure is an instance of UnitOfTemperature and the measure of the entity is a quantity the unit of measure(s) holds during a time interval and the quantity is greater than the other real number and the quantity is less than the real number, then liquid is an attribute of the entity holds during the time interval or there exists a process such that the time interval overlaps the time of existence of the process and the process is an instance of melting and the entity is a patient of the process
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13249-13262	If an entity is an instance of a kind of pure substance and a real number an unit of measure(s) is a melting point of a kind of pure substance and the measure of the entity is a quantity the unit of measure(s) holds during a time interval and the unit of measure is an instance of UnitOfTemperature and the quantity is less than the real number, then solid is an attribute of the entity holds during the time interval or there exists a process such that the time interval overlaps the time of existence of the process and the process is an instance of freezing and the entity is a patient of the process
( ! [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	If a water area is an instance of waterway and the depth from a physical to the water area is a real number an unit of measure(s) and the unit of measure is an instance of UnitOfLength and another real number is less than the real number, then the other real number the unit of measure(s) is a navigable for draft of the water area
( ! [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	If an object is an instance of a kind of pure substance and a kind of pure substance is a subclass of pure substance and a real number kelvin degree(s) is a boiling point of the kind of pure substance and another real number kelvin degree(s) is a melting point of the kind of pure substance and the measure of the object is a third real number kelvin degree(s) and the third real number is greater than the other real number and the third real number is less than the real number, then liquid is an attribute of the object
( ! [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	If an object is an instance of a kind of pure substance and a kind of pure substance is a subclass of pure substance and a real number kelvin degree(s) is a melting point of the kind of pure substance and another real number inch mercury(s) is a barometric pressure of the object and the other real number is greater than 29.92 and the measure of the object is a third real number kelvin degree(s) and the third real number is less than the real number, then solid is an attribute of the object
( ! [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	If the list of processes @ROW and a physical is a member of (@ROW) and another physical is a member of (@ROW) and another entity element of (@ROW) is equal to the physical and a third entity element of (@ROW) is equal to the other physical and a positive integer is less than another positive integer, then the time of existence of the physical happens earlier than the time of existence of the other physical
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 421-436	If a cognitive agent sells a kind of entity for a real number an unit of measure(s) and the unit of measure is an instance of UnitOfCurrency and the price of a kind of entity from the cognitive agent according to a pricing scheme is another real number the unit of measure(s) and the pricing scheme is valid for a kind of agent and another entity is an instance of the kind of entity and a process is an instance of buying and another agent is an immediate instance of a kind of agent and the other agent is an agent of the process and the process originates at the cognitive agent and the other real number is less than the real number, then the statement the real number is a transaction amount of the process has the modal force of likely
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 3653-3666	If minimum device operating temperature of an entity is another entity a third entity(s) and the third entity is an instance of UnitOfTemperature and the entity is located at a fourth entity and device on is an attribute of the entity and a fifth entity the third entity(s) is an air temperature of the fourth entity and the fifth entity is less than the other entity holds during a time position, then the statement DeviceDamaged is an attribute of the entity holds during immediately after the time position has the modal force of likely
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 3679-3692	If minimum device storagqqqe temperature of an entity is another entity a third entity(s) and the third entity is an instance of UnitOfTemperature and the entity is located at a fourth entity and device off is an attribute of the entity and a fifth entity the third entity(s) is an air temperature of the fourth entity and the fifth entity is less than the other entity holds during a time position, then the statement DeviceDamaged is an attribute of the entity holds during immediately after the time position has the modal force of likely

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	If college freshman is an attribute of a position and a human holds the position of the position in an organization, then there exists a real number such that the human is a student of the organization holds during the real number year duration(s) and the real number is less than 1
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 17776-17786	If college junior is an attribute of a position and a human holds the position of the position in an organization, then there exists a real number such that the human is a student of the organization holds during the real number year duration(s) and the real number is greater than or equal to 2 and the real number is less than 3
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 17792-17802	If college senior is an attribute of a position and a human holds the position of the position in an organization, then there exists a real number such that the human is a student of the organization holds during the real number year duration(s) and the real number is greater than or equal to 3 and the real number is less than 4
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 17808-17818	If college sophomore is an attribute of a position and a human holds the position of the position in an organization, then there exists a real number such that the human is a student of the organization holds during the real number year duration(s) and the real number is greater than or equal to 1 and the real number is less than 2
No TPTP formula. May not be expressible in strict first order.	Dining.kif 1101-1109	If probability of comfort food is an attribute of an entity provided that heart-healthy food is an attribute of the entity holds is a real number and probability of comfort food is an attribute of the entity provided that heart-healthy food is not an attribute of the entity holds is another real number, then the real number is less than the other real number
No TPTP formula. May not be expressible in strict first order.	FinancialOntology.kif 3653-3661	If an agent is a day phone of a symbolic string and a kind of day is an instance of day, then there exists a telephone such that the telephone is a phone number of the symbolic string and the agent possesses the telephone holds during the hour the symbolic string and the symbolic string is less than 18
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2564-2569	If a formula decreases likelihood of another formula and the probability of the other formula is equal to a real number and probability of the formula provided that the other formula holds is another real number, then the other real number is less than the real number
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 12780-12789	If the expected value of a kind of object is a real number an unit of measure(s) and the unit of measure is an instance of CompositeUnitOfMeasure, then the statement there exist an entity and the real numberUANTITY such that the entity is an instance of a kind of object and the measure of the entity is the real numberUANTITY the unit of measure(s) and the real numberUANTITY is less than the real number and .5 has the modal force of unlikely
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 12708-12717	If the minimum expected value of a kind of object is a real number an unit of measure(s) and the unit of measure is an instance of CompositeUnitOfMeasure, then the statement there exist an entity and the real numberUANTITY such that the entity is an instance of a kind of object and the measure of the entity is the real numberUANTITY the unit of measure(s) and the real numberUANTITY is less than the real number has the modal force of unlikely
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 12719-12730	If the minimum expected value of a kind of object is a real number an unit of measure(s) and a class is a subclass of NonCompositeUnitOfMeasure and the unit of measure is an instance of the class, then the statement there exist an entity, the real numberUANTITY and a third entity such that the entity is an instance of a kind of object and the measure of the entity is the real numberUANTITY the third entity(s) and the third entity is an instance of the class and the real numberUANTITY is less than the real number has the modal force of unlikely
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 12670-12679	If the minimum expected radius of a kind of object is a real number an unit of measure(s) and another object is an instance of a kind of object and sphere is an attribute of the other object, then the statement the radius of the other object is the real numberADIUS the unit of measure(s) and the real numberADIUS is less than the real number has the modal force of unlikely
( ! [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	If a two dimensional angle is an instance of acute angle and a real number angular degree(s) is an angular measure of the two dimensional angle, then the real number is less than 90
No TPTP formula. May not be expressible in strict first order.	Dining.kif 725-748	If an agent is an instance of agent and a cognitive agent is a potential customer for the agent and the statement an entity is an instance of reserving and the entity ends up at the agent has the modal force of necessity and probability of there exists the entityES1 such that the entityES1 is an instance of reservation and the cognitive agent reserves the entityES1 and the agent fulfills the entityES1 provided that the agent is a customer of the cognitive agent holds is a real number and probability of there doesn't exist the entityES2 such that the entityES2 is an instance of reservation and the cognitive agent reserves the entityES2 and the agent fulfills the entityES2 provided that the agent is a customer of the cognitive agent holds is another real number, then the other real number is less than the real number
( ! [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	If an object is an instance of airport and very short runway airport is an attribute of the object, then there exist another object and a real number such that the other object is an instance of runway and the other object is a part of the object and the length of the other object is the real number meter(s) and the real number is less than 914
( ! [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	If a geographic area is an instance of geographic area and the elevation low point of the geographic area is a geographic subregion of the geographic area and an unit of measure is an instance of UnitOfLength and a real number the unit of measure(s) is an elevation of the elevation low point of the geographic area, then there don't exist another geographic area and another real number such that the other geographic area is a geographic subregion of the geographic area and the other geographic area is not equal to the elevation low point of the geographic area and the other real number the unit of measure(s) is an elevation of the other geographic area and the other real number is less than the real number
( ! [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	If a region is an instance of geographic area and a process is an instance of clear weather and the process is located at 2 and a nonnegative real number is a cloud cover fraction of the region, then the nonnegative real number is less than 0.3
( ! [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	If a region is an instance of geographic area and a process is an instance of clear weather and the process is located at 2, then there exists a nonnegative real number such that the nonnegative real number is a cloud cover fraction of the region and the nonnegative real number is less than 0.3
( ! [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	If a self connected object is an instance of bottle and the bottom of the self connected object is another self connected object and the top of the self connected object is a third self connected object and an unit of measure is an instance of UnitOfLength and the width of the other self connected object is a real number the unit of measure(s) and the width of the third self connected object is another real number the unit of measure(s), then the other real number is less than the real number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 10517-10530	If a process is an instance of cooling and an entity is a patient of the process, then there exist another entity, a quantity and another quantity such that the other entity is an instance of temperature measure and the entity the other entity(s) is equal to the quantity holds during the beginning of the time of existence of the process and the entity the other entity(s) is equal to the other quantity holds during the end of the time of existence of the process and the other quantity is less than the quantity
No TPTP formula. May not be expressible in strict first order.	QoSontology.kif 1932-1946	If a computer process is an instance of data compression and a digital data is processed by the computer process and the digital data requires a quantity an entity(s) holds during immediately before the time of existence of the computer process and the digital data requires another quantity the entity(s) holds during immediately after the time of existence of the computer process, then the other quantity is less than the quantity
No TPTP formula. May not be expressible in strict first order.	Dining.kif 507-516	If a process is an instance of delivery service and the process ends up at an entity and a geographic area is the delivery area of an agent and probability of the entity is located at the geographic area provided that the agent is an agent of the process holds is a real number and probability of the entity is not located at the geographic area provided that the agent is an agent of the process holds is another real number, then the other real number is less than the real number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 10497-10510	If a process is an instance of decreasing and an entity is a patient of the process, then there exist another entity, a quantity and another quantity such that the entity the other entity(s) is equal to the quantity holds during the beginning of the time of existence of the process and the entity the other entity(s) is equal to the other quantity holds during the end of the time of existence of the process and the other quantity is less than the quantity

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)

KB Term:			Term intersection

English Word: