Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| appearance as argument number 1 |
|
| appearance as argument number 2 |
|
|
| appearance as argument number 3 |
|
|
| 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(n__0_0,V__NUMBER1))))) & (((s__instance(V__NUMBER1,s__NonnegativeRealNumber) & (V__NUMBER1 = V__NUMBER2)) | (s__instance(V__NUMBER1,s__NegativeRealNumber) & (V__NUMBER2 = s__SubtractionFn(n__0_0,V__NUMBER1)))) => ((s__AbsoluteValueFn(V__NUMBER1) = V__NUMBER2) & s__instance(V__NUMBER1,s__RealNumber) & s__instance(V__NUMBER2,s__RealNumber)))) )
|
Merge.kif 4880-4891 | equal the absolute value of X and Y and X is an instance of real number and Y is an instance of real number if and only if X is an instance of nonnegative real number and equal X and Y or X is an instance of negative real number and equal Y and (0.0 and X) |
| ! [V__DEGREE] : ((s__instance(V__DEGREE,s__RealNumber) => (s__TangentFn(V__DEGREE) = s__DivisionFn(s__SineFn(V__DEGREE) ,s__CosineFn(V__DEGREE)))) )
|
Merge.kif 5362-5368 | If X is an instance of real number, then equal the tangent of X, the sine of X, and the cosine of X |
| ! [V__N] : ((s__instance(V__N,s__RealNumber) => (s__MeasureFn(V__N,s__Horsepower) = s__MeasureFn(s__MultiplicationFn(V__N,n__746) ,s__Watt))) )
|
Merge.kif 7021-7025 | If X is an instance of real number, then equal X horsepower(s) and X and 746 watt(s) |
| ! [V__B : $i,V__T : $real] : (((s__roastedToTemperature(V__B, V__T) & s__instance(V__B, s__CoffeeBean)) => s__modalAttribute(( ? [V__R:$i] : ((s__instance(V__R, s__DryRoasting) & s__patient(V__R, V__B)))), s__Likely))) | Food.kif 455-464 | If X is the temperature at which Y is roasted to, Y is an instance of coffee bean, and X is an instance of real number, then the statement there exists Z such that Z is an instance of dry roasting and Y is a patient of Z has the modal force of likely |
| ! [V__BUYINGS : $i,V__GMB : $i,V__ITEM : $i,V__TOTAL : $int] : (((s__instance(V__BUYINGS, s__Collection) & s__instance(V__GMB, s__CurrencyMeasure) & V__GMB = s__GMBFn(V__BUYINGS) & V__TOTAL = s__CardinalityFn(s__KappaFn(V__ITEM, (s__instance(V__ITEM, s__Object) & ( ? [V__BUYING:$i] : ((s__member(V__BUYING, V__BUYINGS) & s__patient(V__BUYING, V__ITEM)))))))) => s__ABPFn(V__BUYINGS) = s__DivisionFn(V__GMB, V__TOTAL))) | UXExperimentalTerms.kif 3238-3258 | If X is an instance of collection, Y is an instance of currency measure, Z is an instance of real number, equal Y and the value of X, and equal Z and the number of instances in the class described by W, then equal the average price of X, Y, and Z |
| ! [V__GMV : $i,V__ITEM : $i,V__SELLINGS : $i,V__TOTAL : $int] : (((s__instance(V__SELLINGS, s__Collection) & s__instance(V__GMV, s__CurrencyMeasure) & V__GMV = s__GMVFn(V__SELLINGS) & V__TOTAL = s__CardinalityFn(s__KappaFn(V__ITEM, (s__instance(V__ITEM, s__Object) & ( ? [V__SELLING:$i] : ((s__member(V__SELLING, V__SELLINGS) & s__patient(V__SELLING, V__ITEM)))))))) => s__ASPFn(V__SELLINGS) = s__DivisionFn(V__GMV, V__TOTAL))) | UXExperimentalTerms.kif 3281-3301 | If X is an instance of collection, Y is an instance of currency measure, Z is an instance of real number, equal Y and the value of X, and equal Z and the number of instances in the class described by W, then equal the average selling price of X, Y, and Z |
| consequent |
|
|
| ! [V__NUMBER] : (((s__instance(V__NUMBER,s__NonnegativeRealNumber) => (s__greaterThanOrEqualTo(V__NUMBER,n__0) & s__instance(V__NUMBER,s__RealNumber))) & ((s__greaterThanOrEqualTo(V__NUMBER,n__0) & s__instance(V__NUMBER,s__RealNumber)) => s__instance(V__NUMBER,s__NonnegativeRealNumber))) )
|
Merge.kif 2030-2034 | X is an instance of nonnegative real number if, only if X is greater than or equal to 0, and X is an instance of real number |
| ! [V__NUMBER] : (((s__instance(V__NUMBER,s__PositiveRealNumber) => (s__greaterThan(V__NUMBER,n__0) & s__instance(V__NUMBER,s__RealNumber))) & ((s__greaterThan(V__NUMBER,n__0) & s__instance(V__NUMBER,s__RealNumber)) => s__instance(V__NUMBER,s__PositiveRealNumber))) )
|
Merge.kif 2041-2045 | X is an instance of positive real number if, only if X is greater than 0, and X is an instance of 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 2052-2056 | X is an instance of negative real number if, only if X is less than 0, and X is an instance of real number |
| ! [V__LIST,V__AVERAGE] : (((s__instance(V__LIST,s__List) & s__instance(V__AVERAGE,s__RealNumber)) => (s__average(V__LIST,V__AVERAGE) => (! [V__LISTITEM] : ((s__inList(V__LISTITEM,V__LIST) => s__instance(V__LISTITEM,s__RealNumber)))))) )
|
Merge.kif 5492-5497 | If X is an average of Y, then For all Entity Z: if Z is a member of Y, then Z is an instance of real number |
| ! [V__SQUAREUNIT,V__UNIT] : ((s__instance(V__SQUAREUNIT,s__UnitOfMeasure) => ((s__instance(V__UNIT,s__UnitOfMeasure) & (V__SQUAREUNIT = s__SquareUnitFn(V__UNIT))) => (? [V__NUM] : ((s__instance(V__NUM,s__RealNumber) & (s__MeasureFn(V__NUM,V__SQUAREUNIT) = s__MeasureFn(s__MultiplicationFn(V__NUM,V__NUM) ,V__UNIT))))))) )
|
Mid-level-ontology.kif 15195-15206 | If X is an instance of unit of measure and equal Y and the square unit of X, then there exists Z such that Z is an instance of real number and equal Z Y(s) and Z and Z X(s) |
| ! [V__MAF : $i,V__REFERENCEOBJECT : $i,V__RELATIVEOBJECT : $i] : (((s__instance(V__MAF, s__MovingAwayFrom) & s__instance(V__RELATIVEOBJECT, s__Object) & s__instance(V__REFERENCEOBJECT, s__Object) & s__patient(V__MAF, V__RELATIVEOBJECT) & s__patient(V__MAF, V__REFERENCEOBJECT)) => ( ? [V__BEFOREDISTANCE:$real, V__AFTERDISTANCE:$real, V__U:$i] : ((s__moves(V__MAF, V__RELATIVEOBJECT) & s__holdsDuring(s__BeginFn(s__WhenFn(V__MAF)), s__distance(V__RELATIVEOBJECT, V__REFERENCEOBJECT, s__MeasureFn(V__BEFOREDISTANCE, V__U))) & s__holdsDuring(s__EndFn(s__WhenFn(V__MAF)), s__distance(V__RELATIVEOBJECT, V__REFERENCEOBJECT, s__MeasureFn(V__AFTERDISTANCE, V__U))) & ($greater(V__AFTERDISTANCE,V__BEFOREDISTANCE))))))) | Mid-level-ontology.kif 34214-34234 | If X is an instance of moving away from, Y is an instance of object, Z is an instance of object, Y is a patient of X, and Z is a patient of X, then there exist W, V and U such that W is an instance of real number and V is an instance of real number and Y moves during X and the distance between Y and Z is W U(s) holds during the beginning of the time of existence of X and the distance between Y and Z is V U(s) holds during the end of the time of existence of X and V is greater than W |
| ! [V__MT : $i,V__REFERENCEOBJECT : $i,V__RELATIVEOBJECT : $i] : (((s__instance(V__MT, s__MovingTowards) & s__instance(V__RELATIVEOBJECT, s__Object) & s__instance(V__REFERENCEOBJECT, s__Object) & s__patient(V__MT, V__REFERENCEOBJECT) & s__patient(V__MT, V__RELATIVEOBJECT)) => ( ? [V__BEFOREDISTANCE:$real, V__AFTERDISTANCE:$real, V__U:$i] : ((s__instance(V__U, s__UnitOfLength) & s__moves(V__MT, V__RELATIVEOBJECT) & s__holdsDuring(s__BeginFn(s__WhenFn(V__MT)), s__distance(V__RELATIVEOBJECT, V__REFERENCEOBJECT, s__MeasureFn(V__BEFOREDISTANCE, V__U))) & s__holdsDuring(s__EndFn(s__WhenFn(V__MT)), s__distance(V__RELATIVEOBJECT, V__REFERENCEOBJECT, s__MeasureFn(V__AFTERDISTANCE, V__U))) & ($greater(V__BEFOREDISTANCE,V__AFTERDISTANCE))))))) | Mid-level-ontology.kif 34241-34262 | If X is an instance of moving towards, Y is an instance of object, Z is an instance of object, Z is a patient of X, and Y is a patient of X, then there exist W, V and U such that W is an instance of real number and V is an instance of real number and U is an instance of unit of length and Y moves during X and the distance between Y and Z is W U(s) holds during the beginning of the time of existence of X and the distance between Y and Z is V U(s) holds during the end of the time of existence of X and W is greater than V |
| ! [V__L] : ((s__instance(V__L,s__Lungo) => (? [V__E,V__V] : ((s__instance(V__E,s__Espresso) & s__part(V__E,V__L) & s__measure(V__E,s__MeasureFn(V__V,s__Liter)) & s__instance(V__V,s__RealNumber) & s__measure(V__L,s__MeasureFn(s__MultiplicationFn(V__V,n__2) ,s__Liter)))))) )
|
Food.kif 747-758 | If X is an instance of lungo, then there exist Y and Z such that Y is an instance of espresso and Y is a part of X and the measure of Y is Z liter(s) and Z is an instance of real number and the measure of X is Z and 2 liter(s) |
|
