Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| exists |
| antecedent |
|
| ! [V__GUN : $i,V__LM : $real,V__LM1 : $real,V__O : $i,V__U : $i] : (((s__instance(V__GUN, s__Gun) & s__instance(V__U, s__UnitOfLength) & s__effectiveRange(V__GUN, s__MeasureFn(V__LM, V__U)) & s__distance(V__GUN, V__O, s__MeasureFn(V__LM1, V__U)) & ~(( ? [V__O2:$i] : (s__between(V__O, V__O2, V__GUN)))) & ($lesseq(V__LM1,V__LM))) => ( ? [V__DAMAGING:$i] : (s__capability(s__KappaFn(V__DAMAGING, (s__instance(V__DAMAGING, s__Damaging) & s__patient(V__DAMAGING, V__O))), s__instrument, V__GUN))))) | Mid-level-ontology.kif 1662-1680 | If All of the following hold: (1) X is an instance of gun (2) Y is an instance of unit of length (3) Z Y(s) is an effective range of X (4) the distance between X and W is V Y(s) (5) there doesn't exist U such that U is between W and X (6) V is less than or equal to Z, then there exists T such that X is capable of doing the class described by T as a instrument |
| ! [V__GUN : $i,V__LM : $real,V__LM1 : $real,V__O : $i,V__U : $i] : (((s__instance(V__GUN, s__Gun) & s__instance(V__U, s__UnitOfLength) & s__effectiveRange(V__GUN, s__MeasureFn(V__LM, V__U)) & s__distance(V__GUN, V__O, s__MeasureFn(V__LM1, V__U)) & s__instance(V__O, s__Organism) & ~(( ? [V__O2:$i] : (s__between(V__O, V__O2, V__GUN)))) & ($lesseq(V__LM1,V__LM))) => ( ? [V__KILLING:$i] : (s__capability(s__KappaFn(V__KILLING, (s__instance(V__KILLING, s__Killing) & s__patient(V__KILLING, V__O))), s__instrument, V__GUN))))) | Mid-level-ontology.kif 1684-1703 | If All of the following hold: (1) X is an instance of gun (2) Y is an instance of unit of length (3) Z Y(s) is an effective range of X (4) the distance between X and W is V Y(s) (5) W is an instance of organism (6) there doesn't exist U such that U is between W and X (7) V is less than or equal to Z, then there exists T such that X is capable of doing the class described by T as a instrument |
| ! [V__B] : (((s__instance(V__B,s__Bubble) & ~((? [V__X,V__S] : ((s__instance(V__X,s__Object) & s__instance(V__S,s__Attribute) & (s__attribute(V__X,V__S) & ~((V__X = s__Gas)) & s__meetsSpatially(V__X,V__B))))))) => s__attribute(V__B,s__ConvexRoundShape)) )
|
Mid-level-ontology.kif 6111-6120 | If X is an instance of bubble and there don't exist Y, Z such that Z is an attribute of Y, equal Y, gas, and Y meets X, then convex round shape is an attribute of X |
| ! [V__NOTPARTPROB : $real,V__PART : $i,V__PARTPROB : $real,V__WHOLE : $i,V__Y : $i] : (((s__typicallyContainsTemporalPart(V__PART, V__WHOLE) & s__instance(V__Y, V__WHOLE) & V__PARTPROB = s__ProbabilityFn(( ? [V__X1:$i] : ((s__instance(V__X1, V__PART) & s__temporalPart(V__X1, V__Y))))) & V__NOTPARTPROB = s__ProbabilityFn(~(( ? [V__X2:$i] : ((s__instance(V__X2, V__PART) & s__temporalPart(V__X2, V__Y))))))) => ($greater(V__PARTPROB,V__NOTPARTPROB)))) | Mid-level-ontology.kif 25115-25132 | If a X typically contains a Y, Z is an instance of X, equal W, the probability of there exists V such that V is an instance of Y, and V is a part of Z, and equal U, the probability of there doesn't exist T such that T is an instance of Y, and T is a part of Z, then W is greater than U |
| ! [V__A : $i,V__AGENT : $i,V__NOTPPROB : $real,V__PPROB : $real,V__PROCESS : $i] : (((s__typicalAction(V__PROCESS, V__AGENT) & s__instance(V__A, V__AGENT) & V__PPROB = s__ProbabilityFn(( ? [V__X:$i] : ((s__instance(V__X, V__PROCESS) & s__agent(V__X, V__A))))) & V__NOTPPROB = s__ProbabilityFn(~(( ? [V__Y:$i] : ((s__instance(V__Y, V__PROCESS) & s__agent(V__Y, V__A))))))) => ($greater(V__PPROB,V__NOTPPROB)))) | Mid-level-ontology.kif 25150-25167 | If X is a typical action of a Y, Z is an instance of Y, equal W, the probability of there exists V such that V is an instance of X, and Z is an agent of V, and equal U, the probability of there doesn't exist T such that T is an instance of X, and Z is an agent of T, then W is greater than U |
| ! [V__NOTPARTPROB : $real,V__PART : $i,V__PARTPROB : $real,V__WHOLE : $i,V__X : $i] : (((s__typicalPart(V__PART, V__WHOLE) & s__instance(V__X, V__PART) & V__PARTPROB = s__ProbabilityFn(( ? [V__Y:$i] : ((s__instance(V__Y, V__WHOLE) & s__part(V__X, V__Y))))) & V__NOTPARTPROB = s__ProbabilityFn(~(( ? [V__Z:$i] : ((s__instance(V__Z, V__WHOLE) & s__part(V__X, V__Z))))))) => ($greater(V__PARTPROB,V__NOTPARTPROB)))) | Mid-level-ontology.kif 25958-25975 | If a X is typically a part of a Y, Z is an instance of X, equal W, the probability of there exists V such that V is an instance of Y, and Z is a part of V, and equal U, the probability of there doesn't exist T such that T is an instance of Y, and Z is a part of T, then W is greater than U |
| ! [V__NOTPARTPROB : $real,V__PART : $i,V__PARTPROB : $real,V__WHOLE : $i,V__Y : $i] : (((s__typicallyContainsPart(V__PART, V__WHOLE) & s__instance(V__Y, V__WHOLE) & V__PARTPROB = s__ProbabilityFn(( ? [V__X1:$i] : ((s__instance(V__X1, V__PART) & s__part(V__X1, V__Y))))) & V__NOTPARTPROB = s__ProbabilityFn(~(( ? [V__X2:$i] : ((s__instance(V__X2, V__PART) & s__part(V__X2, V__Y))))))) => ($greater(V__PARTPROB,V__NOTPARTPROB)))) | Mid-level-ontology.kif 25996-26013 | If a X typically has a part Y, Z is an instance of X, equal W, the probability of there exists V such that V is an instance of Y, and V is a part of Z, and equal U, the probability of there doesn't exist T such that T is an instance of Y, and T is a part of Z, then W is greater than U |
| ! [V__UNITSTR,V__PLACE] : (((s__instance(V__UNITSTR,s__SymbolicString) & s__instance(V__PLACE,s__PostalPlace)) => ((s__unitNumber(V__UNITSTR,V__PLACE) & ~((? [V__FLR] : ((s__instance(V__FLR,s__SymbolicString) & s__floorCode(V__FLR,V__PLACE)))))) => (? [V__UNIT] : ((s__instance(V__UNIT,s__Room) & s__names(V__UNITSTR,V__UNIT) & s__located(V__UNIT,V__PLACE)))))) )
|
Mid-level-ontology.kif 26927-26937 | If the unit number of X is Y and there doesn't exist Z such that Z is the floor of X, then there exists W such that W is an instance of room, W has name Y, and W is located at X |
| ! [V__A : $i,V__F : $i,V__T : $i] : ((s__holdsDuring(V__T, (~(( ? [V__C:$i] : ((s__instance(V__C, s__Clothing) & s__covers(V__C, V__F))))) & s__instance(V__F, s__Foot) & s__part(V__F, V__A))) => s__holdsDuring(V__T, s__attribute(V__A, s__Barefoot)))) | Mid-level-ontology.kif 32753-32764 | If there doesn't exist X such that X is an instance of clothing, X covers Y, Y is an instance of foot, and Y is a part of Z holds during W, then barefoot is an attribute of Z holds during W |
| ! [V__A : $i,V__T : $i] : ((s__holdsDuring(V__T, ~(( ? [V__C:$i] : ((s__instance(V__C, s__Clothing) & s__wears(V__A, V__C)))))) => s__holdsDuring(V__T, s__attribute(V__A, s__Naked)))) | Mid-level-ontology.kif 32779-32787 | If there doesn't exist X such that X is an instance of clothing and Y wears X holds during Z, then naked is an attribute of Y holds during Z |
| ! [V__R1,V__R2,V__A1,V__A2,V__S1] : (((s__instance(V__R1,s__RealNumber) & s__instance(V__R2,s__RealNumber)) => ((s__instance(V__A1,s__Automobile) & s__instance(V__A2,s__Automobile) & s__instance(V__S1,s__AutomobileShock) & s__part(V__S1,V__A1) & ~((? [V__S2] : ((s__instance(V__S2,s__AutomobileShock) & s__part(V__S2,V__A2))))) & s__dampingRatio(V__A1,V__R1) & s__dampingRatio(V__A2,V__R2)) => s__greaterThan(V__R2,V__R1))) )
|
Cars.kif 790-803 | If All of the following hold: (1) X is an instance of automobile (2) Y is an instance of automobile (3) Z is an instance of shock (4) Z is a part of X (5) there doesn't exist W such that W is an instance of shock and W is a part of Y (6) the damping ratio of X is V (7) the damping ratio of Y is U, then U is greater than V |
| ! [V__NOTPARTPROB : $real,V__PART : $i,V__PARTPROB : $real,V__WHOLE : $i,V__X : $i] : (((s__typicalTemporalPart(V__PART, V__WHOLE) & s__instance(V__X, V__PART) & V__PARTPROB = s__ProbabilityFn(( ? [V__Y:$i] : ((s__instance(V__Y, V__WHOLE) & s__temporalPart(V__X, V__Y))))) & V__NOTPARTPROB = s__ProbabilityFn(~(( ? [V__Z:$i] : ((s__instance(V__Z, V__WHOLE) & s__temporalPart(V__X, V__Z))))))) => ($greater(V__PARTPROB,V__NOTPARTPROB)))) | Cars.kif 1367-1384 | If a X is typically a part of a Y, Z is an instance of X, equal W, the probability of there exists V such that V is an instance of Y, and Z is a part of V, and equal U, the probability of there doesn't exist T such that T is an instance of Y, and Z is a part of T, then W is greater than U |
| ! [V__EM : $i,V__T1 : $i] : (((s__instance(V__EM, s__Electromagnet) & ~(s__holdsDuring(V__T1, ( ? [V__T:$i, V__E:$i] : ((s__instance(V__T, s__Transfer) & s__instance(V__E, s__Electricity) & s__objectTransferred(V__T, V__E) & s__path(V__T, V__EM))))))) => ~(s__holdsDuring(V__T1, ( ? [V__M:$i] : ((s__instance(V__M, s__Magnetism) & s__instrument(V__M, V__EM)))))))) | Cars.kif 3775-3791 | If X is an instance of electromagnet and there don't exist Y, Z such that Y is an instance of transfer, Z is an instance of electricity, the object transferred in Y is Z, and X is path along which Y occurs doesn't hold during W, then there doesn't exist V such that V is an instance of magnetism and X is an instrument for V doesn't hold during W |
| ! [V__CUST,V__AGENT,V__AMT,V__ITEM,V__X,V__D] : (((s__instance(V__CUST,s__CognitiveAgent) & s__instance(V__AGENT,s__AutonomousAgent) & s__instance(V__AMT,s__CurrencyMeasure) & s__instance(V__ITEM,s__Class) & s__subclass(V__ITEM,s__Object) & s__instance(V__X,s__Object)) => ((s__customer(V__CUST,V__AGENT) & s__corkageFee(V__AMT,V__ITEM,V__AGENT) & s__instance(V__X,V__ITEM) & ~((? [V__B] : ((s__instance(V__B,s__Buying) & s__patient(V__B,V__X) & s__destination(V__B,V__CUST) & s__origin(V__B,V__AGENT))))) & s__instance(V__D,s__Drinking) & s__agent(V__D,V__CUST) & s__resource(V__D,V__X)) => (? [V__C] : ((s__instance(V__C,s__Corkage) & s__agent(V__C,V__CUST) & s__refers(V__C,V__X) & s__destination(V__C,V__AGENT)))))) )
|
Dining.kif 130-150 | If All of the following hold: (1) X is a customer of Y (2) X charges Z in corkage for W (3) V is an instance of W (4) there doesn't exist U such that U is an instance of buying, V is a patient of U, U ends up at Y, and U originates at X (5) T is an instance of drinking (6) Y is an agent of T (7) V is a resource for T, then there exists S such that S is an instance of corkage, Y is an agent of S, S includes a reference to V, and S ends up at X |
| ! [V__AGENT : $i,V__CUST : $i,V__OBJ : $i,V__X : $i] : (((s__facility(V__AGENT, V__OBJ) & s__customer(V__CUST, V__AGENT) & s__instance(V__X, V__OBJ) & s__desires(V__CUST, ( ? [V__PROC:$i] : ((s__instance(V__PROC, s__IntentionalProcess) & s__patient(V__PROC, V__X) & s__agent(V__PROC, V__CUST)))))) => s__modalAttribute(s__confersRight(V__AGENT, V__CUST, s__uses(V__X, V__CUST)), s__Possibility))) | Dining.kif 336-350 | If X provides Y, X is a customer of Z, W is an instance of Y, and Z desires there exists V such that V is an instance of intentional process, W is a patient of V, and Z is an agent of V, then the statement Z allows Z uses W to perform task of the type X has the modal force of possibility |
| ! [V__AGENT,V__CUST,V__LOC1,V__LOC2,V__C] : (((s__instance(V__AGENT,s__AutonomousAgent) & s__instance(V__CUST,s__CognitiveAgent) & s__instance(V__LOC1,s__Object) & s__instance(V__LOC2,s__Object)) => ((s__instance(V__C,s__CateringService) & s__agent(V__C,V__AGENT) & s__destination(V__C,V__CUST) & s__located(V__AGENT,V__LOC1) & s__customer(V__CUST,V__AGENT) & (? [V__S,V__FOOD,V__E] : ((s__instance(V__S,s__Cooking) & s__agent(V__S,V__AGENT) & s__result(V__S,V__FOOD) & s__patient(V__C,V__FOOD) & s__instance(V__E,s__Eating) & s__agent(V__E,V__CUST) & s__eventLocated(V__E,V__LOC2))))) => ~((V__LOC1 = V__LOC2)))) )
|
Dining.kif 586-602 | If All of the following hold: (1) X is an instance of catering (2) Y is an agent of X (3) X ends up at Z (4) Y is located at W (5) Y is a customer of Z (6) All of the following hold: (1) there exist V, U (2) T such that V is an instance of cooking (3) Y is an agent of V (4) U is a result of V (5) U is a patient of X (6) T is an instance of eating (7) Z is an agent of T (8) T is located at S, then equal W and S |
| ! [V__AGENT : $i,V__CUST : $i,V__NUM1 : $real,V__NUM2 : $real,V__R : $i] : (((s__instance(V__AGENT, s__AutonomousAgent) & s__potentialCustomer(V__CUST, V__AGENT) & s__modalAttribute((s__instance(V__R, s__Reserving) & s__destination(V__R, V__AGENT)), s__Necessity) & s__conditionalProbability(( ? [V__RES1:$i] : ((s__instance(V__RES1, s__Reservation) & s__reservingEntity(V__CUST, V__RES1) & s__fulfillingEntity(V__AGENT, V__RES1)))), s__customer(V__CUST, V__AGENT), V__NUM1) & s__conditionalProbability(~(( ? [V__RES2:$i] : ((s__instance(V__RES2, s__Reservation) & s__reservingEntity(V__CUST, V__RES2) & s__fulfillingEntity(V__AGENT, V__RES2))))), s__customer(V__CUST, V__AGENT), V__NUM2)) => ($less(V__NUM2,V__NUM1)))) | Dining.kif 772-795 | If X is an instance of agent, Y is a potential customer for X, the statement Z is an instance of reserving and Z ends up at X has the modal force of necessity, probability of there exists W such that W is an instance of reservation, Y reserves W, and X fulfills W provided that X is a customer of Y holds is V, and probability of there doesn't exist U such that U is an instance of reservation, Y reserves U, and X fulfills U provided that X is a customer of Y holds is T, then T is less than V |
| ! [V__Account] : ((s__instance(V__Account,s__FinancialAccount) => (((? [V__Rate] : ((s__instance(V__Rate,s__Number) & s__fixedInterestRate(V__Account,V__Rate)))) => s__instance(V__Account,s__FixedRateAccount)) & (s__instance(V__Account,s__FixedRateAccount) => (? [V__Rate] : ((s__instance(V__Rate,s__Number) & s__fixedInterestRate(V__Account,V__Rate))))))) )
|
FinancialOntology.kif 1003-1006 | There exists X such that X is a fixed interest rate of Y if and only if Y is an instance of fixed rate account |
| ! [V__Withdrawal,V__Account] : ((((s__instance(V__Withdrawal,s__Withdrawal) & s__instance(V__Account,s__FinancialAccount) & s__origin(V__Withdrawal,s__CurrencyFn(V__Account)) & ~((? [V__Penalty] : ((s__instance(V__Penalty,s__Penalty) & s__destination(V__Penalty,s__CurrencyFn(V__Account)) & s__causes(V__Withdrawal,V__Penalty)))))) => s__liquidity(V__Account,s__HighLiquidity)) & (s__liquidity(V__Account,s__HighLiquidity) => (s__instance(V__Withdrawal,s__Withdrawal) & s__instance(V__Account,s__FinancialAccount) & s__origin(V__Withdrawal,s__CurrencyFn(V__Account)) & ~((? [V__Penalty] : ((s__instance(V__Penalty,s__Penalty) & s__destination(V__Penalty,s__CurrencyFn(V__Account)) & s__causes(V__Withdrawal,V__Penalty)))))))) )
|
FinancialOntology.kif 1864-1874 | All of the following hold: (1) X is an instance of withdrawing from an account (2) Y is an instance of financial account (3) X originates at the currency of Y (4) there doesn't exist Z such that Z is an instance of penalizing (5) Z ends up at the currency of Y (6) X causes Z if (7) only if the liqudity of Y is high liquidity |
| ! [V__Amount,V__Loan] : ((s__instance(V__Amount,s__Interest) => (((? [V__Period] : ((s__instance(V__Period,s__TimeInterval) & (s__instance(V__Loan,s__Loan) & s__agreementPeriod(V__Loan,V__Period) & s__interestEarned(V__Loan,V__Amount,V__Period))))) => s__loanInterest(V__Loan,V__Amount)) & (s__loanInterest(V__Loan,V__Amount) => (? [V__Period] : ((s__instance(V__Period,s__TimeInterval) & (s__instance(V__Loan,s__Loan) & s__agreementPeriod(V__Loan,V__Period) & s__interestEarned(V__Loan,V__Amount,V__Period)))))))) )
|
FinancialOntology.kif 3978-3984 | There exists X such that Y is an instance of loan, X is an agreement period of Y, Y is interest earned Z for X if, and only if Z is a loan interest of Y |
| ! [V__X] : (((s__instance(V__X,s__Pasta) & ~((? [V__Y] : ((s__instance(V__Y,s__Pasta) & s__part(V__Y,V__X)))))) => s__attribute(V__X,s__LongAndThin)) )
|
Food.kif 2648-2656 | If X is an instance of pasta and there doesn't exist Y such that Y is an instance of pasta and Y is a part of X, then long and thin is an attribute of X |
| ! [V__X] : (((s__instance(V__X,s__Penne) & ~((? [V__Y] : ((s__instance(V__Y,s__Penne) & s__part(V__Y,V__X)))))) => ((? [V__HOLE2] : ((s__instance(V__HOLE2,s__HoleRegion) & s__part(V__X,V__HOLE2)))) & s__attribute(V__X,s__Fillable))) )
|
Food.kif 2792-2805 | If X is an instance of penne and there doesn't exist Y such that Y is an instance of penne and Y is a part of X, then there exists Z such that Z is an instance of hole and X is a part of Z and fillable is an attribute of X |
| ! [V__X] : (((s__instance(V__X,s__Spaghetti) & ~((? [V__Y] : ((s__instance(V__Y,s__Spaghetti) & s__part(V__Y,V__X)))))) => s__attribute(V__X,s__LongAndThin)) )
|
Food.kif 3500-3508 | If X is an instance of spaghetti and there doesn't exist Y such that Y is an instance of spaghetti and Y is a part of X, then long and thin is an attribute of X |
| ! [V__X,V__A,V__B] : ((s__instance(V__X,s__RealNumber) => ((s__instance(V__A,s__PointInSpace) & s__instance(V__B,s__PointInSpace) & s__located(V__A,s__RockyMountains) & s__located(V__B,s__RockyMountains) & s__orientation(V__A,V__B,s__North) & ~((? [V__A1,V__B1] : ((s__instance(V__A1,s__PointInSpace) & s__located(V__A1,s__RockyMountains) & s__orientation(V__A1,V__A,s__North) & s__instance(V__B1,s__PointInSpace) & s__located(V__B1,s__RockyMountains) & s__orientation(V__B1,V__B,s__South))))) & s__distance(V__A,V__B,s__MeasureFn(V__X,s__Mile))) => s__approximateValue(V__X,n__3000))) )
|
Geography.kif 377-395 | If All of the following hold: (1) X is an instance of point in space (2) Y is an instance of point in space (3) X is located at Rocky Mountains (4) Y is located at Rocky Mountains (5) X is north of to Y (6) All of the following hold: (1) there don't exist Z (2) W such that Z is an instance of point in space (3) Z is located at Rocky Mountains (4) Z is north of to X (5) W is an instance of point in space (6) W is located at Rocky Mountains (7) W is south of to Y (7) the distance between X and Y is V mile(s), then the approximate value of V is 3000 |
| ! [V__X,V__A,V__B] : ((s__instance(V__X,s__RealNumber) => ((s__instance(V__A,s__PointInSpace) & s__instance(V__B,s__PointInSpace) & s__located(V__A,s__RockyMountains) & s__located(V__B,s__RockyMountains) & s__orientation(V__A,V__B,s__East) & ~((? [V__A1,V__B1] : ((s__instance(V__A1,s__PointInSpace) & s__located(V__A1,s__RockyMountains) & s__orientation(V__A1,V__A,s__East) & s__instance(V__B1,s__PointInSpace) & s__located(V__B1,s__RockyMountains) & s__orientation(V__B1,V__B,s__West))))) & s__distance(V__A,V__B,s__MeasureFn(V__X,s__Mile))) => (s__greaterThan(V__X,n__70) & s__greaterThan(n__300,V__X)))) )
|
Geography.kif 397-417 | If All of the following hold: (1) X is an instance of point in space (2) Y is an instance of point in space (3) X is located at Rocky Mountains (4) Y is located at Rocky Mountains (5) X is east of to Y (6) All of the following hold: (1) there don't exist Z (2) W such that Z is an instance of point in space (3) Z is located at Rocky Mountains (4) Z is east of to X (5) W is an instance of point in space (6) W is located at Rocky Mountains (7) W is west of to Y (7) the distance between X and Y is V mile(s), then V is greater than 70 and 300 is greater than V |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| consequent |
|
|
| ! [V__CLASS,V__ENTITY] : ((s__instance(V__CLASS,s__Class) => (s__immediateInstance(V__ENTITY,V__CLASS) => ~((? [V__SUBCLASS] : ((s__instance(V__SUBCLASS,s__Class) & (s__subclass(V__SUBCLASS,V__CLASS) & ~((V__SUBCLASS = V__CLASS)) & s__instance(V__ENTITY,V__SUBCLASS)))))))) )
|
Merge.kif 98-104 | If X is an immediate instance of Y, then there doesn't exist Z such that Z is a subclass of Y, equal Z, Y, and X is an instance of Z |
| ! [V__CLASS1,V__CLASS2] : (((s__instance(V__CLASS1,s__Class) & s__instance(V__CLASS2,s__Class)) => (s__immediateSubclass(V__CLASS1,V__CLASS2) => ~((? [V__CLASS3] : ((s__instance(V__CLASS3,s__Class) & (s__subclass(V__CLASS3,V__CLASS2) & s__subclass(V__CLASS1,V__CLASS3) & ~((V__CLASS2 = V__CLASS3)) & ~((V__CLASS1 = V__CLASS3))))))))) )
|
Merge.kif 154-161 | If X is an immediate subclass of Y, then there doesn't exist Z such that Z is a subclass of Y, X is a subclass of Z, equal Y, Z, equal X, and Z |
| ! [V__CLASS1,V__CLASS2] : (((s__instance(V__CLASS1,s__Class) & s__instance(V__CLASS2,s__Class)) => (s__disjoint(V__CLASS1,V__CLASS2) => ~((? [V__INST] : ((s__instance(V__INST,V__CLASS1) & s__instance(V__INST,V__CLASS2))))))) )
|
Merge.kif 393-399 | If X is disjoint from Y, then there doesn't exist Z such that Z is an instance of X and Z is an instance of Y |
| ! [V__CLASS,V__ROW1,V__ROW2] : (((s__subclass(V__CLASS,s__Attribute) & s__instance(V__CLASS,s__Class) & s__instance(V__ROW1,s__Attribute) & s__instance(V__ROW2,s__Attribute)) => (s__exhaustiveAttribute(V__CLASS,V__ROW1,V__ROW2) => (! [V__ATTR1] : ((s__instance(V__ATTR1,V__CLASS) => (? [V__ATTR2] : ((s__inList(V__ATTR2,s__ListFn(V__ROW1,V__ROW2)) & (V__ATTR1 = V__ATTR2))))))))) )
! [V__CLASS,V__ROW1] :
! [V__CLASS,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5] :
! [V__CLASS,V__ROW1,V__ROW2,V__ROW3] :
! [V__CLASS,V__ROW1,V__ROW2,V__ROW3,V__ROW4] :
! [V__CLASS,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7] :
! [V__CLASS,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6] :
|
Merge.kif 501-509 | If @ROW are all the attributes of Y, then For all Entity Z: if Z is an instance of Y, then there exists W such that W is a member of (@ROW) and equal Z and W |
| ! [V__ATTRCLASS,V__ROW1,V__ROW2,V__ROW3,V__ROW4] : (((s__subclass(V__ATTRCLASS,s__Attribute) & s__instance(V__ATTRCLASS,s__Class) & s__instance(V__ROW1,s__Attribute) & s__instance(V__ROW2,s__Attribute) & s__instance(V__ROW3,s__Attribute) & s__instance(V__ROW4,s__Attribute)) => (s__exhaustiveAttribute(V__ATTRCLASS,V__ROW1,V__ROW2,V__ROW3,V__ROW4) => ~((? [V__EL] : ((s__instance(V__EL,V__ATTRCLASS) & ~((? [V__ATTR,V__NUMBER] : ((s__instance(V__NUMBER,s__PositiveInteger) & ((V__EL = V__ATTR) & (V__ATTR = s__ListOrderFn(s__ListFn(V__ROW1,V__ROW2,V__ROW3,V__ROW4) ,V__NUMBER))))))))))))) )
! [V__ATTRCLASS,V__ROW1,V__ROW2,V__ROW3] :
! [V__ATTRCLASS,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6] :
! [V__ATTRCLASS,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5,V__ROW6,V__ROW7] :
! [V__ATTRCLASS,V__ROW1,V__ROW2] :
! [V__ATTRCLASS,V__ROW1] :
! [V__ATTRCLASS,V__ROW1,V__ROW2,V__ROW3,V__ROW4,V__ROW5] :
|
Merge.kif 511-523 | If @ROW are all the attributes of Y, then there doesn't exist Z such that Z is an instance of Y and there don't exist W and V such that equal Z and W and equal W and U element of (@ROW) |
| ! [V__PHYS] : ((s__instance(V__PHYS,s__Physical) => (? [V__LOC,V__TIME] : ((s__instance(V__LOC,s__Object) & s__instance(V__TIME,s__TimePosition) & (s__located(V__PHYS,V__LOC) & s__time(V__PHYS,V__TIME)))))) )
|
Merge.kif 831-836 | If X is an instance of physical, then there exist Y, Z such that X is located at Y, and X exists during Z |
| ! [V__event] : ((s__instance(V__event,s__VolcanicEruption) => (? [V__volcano] : ((s__instance(V__volcano,s__Volcano) & s__agent(V__event,V__volcano))))) )
|
Merge.kif 1030-1035 | If X is an instance of volcanic eruption, then there exists Y such that Y is an instance of volcano and Y is an agent of X |
| ! [V__ERUPTING] : ((s__instance(V__ERUPTING,s__VolcanicEruption) => (? [V__VOLCANO] : ((s__instance(V__VOLCANO,s__Volcano) & s__eventLocated(V__ERUPTING,V__VOLCANO))))) )
|
Merge.kif 1041-1046 | If X is an instance of volcanic eruption, then there exists Y such that Y is an instance of volcano and X is located at Y |
| ! [V__ERUPTING] : ((s__instance(V__ERUPTING,s__VolcanicEruption) => (? [V__HEATING] : ((s__instance(V__HEATING,s__Heating) & s__subProcess(V__HEATING,V__ERUPTING))))) )
|
Merge.kif 1048-1053 | If X is an instance of volcanic eruption, then there exists Y such that Y is an instance of heating and Y is a subprocess of X |
| ! [V__SURF,V__C] : ((s__instance(V__SURF,s__Object) => (s__instance(V__C,s__Crater) => (? [V__HOST,V__EVENT,V__METEOR,V__BOMB] : ((s__instance(V__HOST,s__SelfConnectedObject) & (s__hole(V__C,V__HOST) & s__superficialPart(V__SURF,s__HoleHostFn(V__C)) & ((s__instance(V__EVENT,s__Impacting) & s__instrument(V__EVENT,V__METEOR) & s__instance(V__METEOR,s__Meteorite)) | (s__instance(V__EVENT,s__Explosion) & s__instrument(V__EVENT,V__BOMB) & s__instance(V__BOMB,s__Bomb)) | s__instance(V__EVENT,s__VolcanicEruption)) & s__result(V__EVENT,V__C))))))) )
|
Merge.kif 1059-1075 | If X is an instance of crater, then All of the following hold: (1) there exist Y, Z,, , W (2) V such that X is a hole in Y (3) U is a superficial part of the host of the hole X (4) Z is an instance of impacting (5) W is an instrument for Z (6) W is an instance of meteorite or Z is an instance of explosion (7) V is an instrument for Z (8) V is an instance of bomb or Z is an instance of volcanic eruption (9) X is a result of Z |
| ! [V__OBJ1,V__OBJ2] : (((s__instance(V__OBJ1,s__SelfConnectedObject) & s__instance(V__OBJ2,s__Object)) => (s__contains(V__OBJ1,V__OBJ2) => (? [V__HOLE] : ((s__instance(V__HOLE,s__HoleRegion) & (s__hole(V__HOLE,V__OBJ1) & s__properlyFills(V__OBJ2,V__HOLE))))))) )
|
Merge.kif 1101-1106 | If X contains Y, then there exists Z such that Z is a hole in X and Y properly fills Z |
| ! [V__SUBSTANCE] : ((s__instance(V__SUBSTANCE,s__SyntheticSubstance) => (? [V__PROCESS] : ((s__instance(V__PROCESS,s__IntentionalProcess) & s__result(V__PROCESS,V__SUBSTANCE) & s__instance(V__SUBSTANCE,s__Substance))))) )
|
Merge.kif 1145-1151 | If X is an instance of synthetic substance, then there exists Y such that Y is an instance of intentional process, X is a result of Y, and X is an instance of substance |
| ! [V__ATOM] : ((s__instance(V__ATOM,s__Atom) => (? [V__PROTON,V__ELECTRON] : ((s__part(V__PROTON,V__ATOM) & s__part(V__ELECTRON,V__ATOM) & s__instance(V__PROTON,s__Proton) & s__instance(V__ELECTRON,s__Electron))))) )
|
Merge.kif 1186-1193 | If X is an instance of atom, then there exist Y, Z such that Y is a part of X, Z is a part of X, Y is an instance of proton, and Z is an instance of electron |
| ! [V__PARTICLE] : ((s__instance(V__PARTICLE,s__SubatomicParticle) => (? [V__ATOM] : ((s__instance(V__ATOM,s__Atom) & s__component(V__PARTICLE,V__ATOM))))) )
|
Merge.kif 1211-1216 | If X is an instance of subatomic particle, then there exists Y such that Y is an instance of atom and X is a component of Y |
| ! [V__NUCLEUS] : ((s__instance(V__NUCLEUS,s__AtomicNucleus) => (? [V__NEUTRON,V__PROTON] : ((s__component(V__NEUTRON,V__NUCLEUS) & s__component(V__PROTON,V__NUCLEUS) & s__instance(V__NEUTRON,s__Neutron) & s__instance(V__PROTON,s__Proton))))) )
|
Merge.kif 1222-1229 | If X is an instance of atomic nucleus, then there exist Y, Z such that Y is a component of X, Z is a component of X, Y is an instance of neutron, and Z is an instance of proton |
| ! [V__MIXTURE] : ((s__instance(V__MIXTURE,s__Mixture) => (? [V__PURE1,V__PURE2] : ((s__instance(V__PURE1,s__PureSubstance) & s__instance(V__PURE2,s__PureSubstance) & ~((V__PURE1 = V__PURE2)) & s__piece(V__PURE1,V__MIXTURE) & s__piece(V__PURE2,V__MIXTURE))))) )
|
Merge.kif 1263-1271 | If X is an instance of mixture, then All of the following hold: (1) there exist Y (2) Z such that Y is an instance of pure substance (3) Z is an instance of pure substance (4) equal Y (5) Z (6) Y is a piece of X (7) Z is a piece of X |
| ! [V__ING,V__S] : (((s__instance(V__ING,s__Class) & s__subclass(V__ING,s__Substance) & s__instance(V__S,s__Class) & s__instance(V__S,s__CorpuscularObject)) => (s__ingredient(V__ING,V__S) => (? [V__PROC,V__X,V__Y] : ((s__instance(V__PROC,s__Process) & s__instance(V__X,V__ING) & s__patient(V__PROC,V__X) & s__instance(V__Y,V__S) & s__result(V__PROC,V__Y)))))) )
|
Merge.kif 1289-1297 | If X is an ingredient in Y, then there exist Z, W, V such that Z is an instance of process, W is an instance of X, W is a patient of Z, V is an instance of Y, and V is a result of Z |
| ! [V__OBJ] : ((s__instance(V__OBJ,s__CorpuscularObject) => (? [V__SUBSTANCE1,V__SUBSTANCE2] : ((s__instance(V__SUBSTANCE1,s__Class) & s__subclass(V__SUBSTANCE1,s__Substance) & s__instance(V__SUBSTANCE2,s__Class) & s__subclass(V__SUBSTANCE2,s__Substance) & (s__subclass(V__SUBSTANCE1,s__Substance) & s__subclass(V__SUBSTANCE2,s__Substance) & s__material(V__SUBSTANCE1,V__OBJ) & s__material(V__SUBSTANCE2,V__OBJ) & ~((V__SUBSTANCE1 = V__SUBSTANCE2))))))) )
|
Merge.kif 1304-1312 | If X is an instance of corpuscular object, then All of the following hold: (1) there exist Y (2) Z such that Y is a subclass of substance (3) Z is a subclass of substance (4) X is made of Y (5) X is made of Z (6) equal Y (7) Z |
| ! [V__COLL] : ((s__instance(V__COLL,s__Collection) => (? [V__OBJ] : ((s__instance(V__OBJ,s__Physical) & s__member(V__OBJ,V__COLL))))) )
|
Merge.kif 1345-1348 | If X is an instance of collection, then there exists Y such that Y is a member of X |
| ! [V__OBJ] : ((s__instance(V__OBJ,s__ContentBearingPhysical) => (? [V__THING] : (s__represents(V__OBJ,V__THING)))) )
|
Merge.kif 1401-1404 | If X is an instance of content bearing physical, then there exists Y such that X expresses Y |
| ! [V__STRING] : ((s__instance(V__STRING,s__SymbolicString) => (? [V__PART] : ((s__part(V__PART,V__STRING) & s__instance(V__PART,s__Character))))) )
|
Merge.kif 1437-1442 | If X is an instance of symbolic string, then there exists Y such that Y is a part of X and Y is an instance of character |
| ! [V__LANG] : ((s__instance(V__LANG,s__ConstructedLanguage) => (? [V__PLAN] : ((s__instance(V__PLAN,s__Planning) & s__result(V__PLAN,V__LANG))))) )
|
Merge.kif 1559-1564 | If X is an instance of constructed language, then there exists Y such that Y is an instance of planning and X is a result of Y |
| ! [V__W] : ((s__instance(V__W,s__Writing) => (? [V__S,V__L] : ((s__instance(V__S,s__Text) & s__instance(V__L,s__WrittenHumanLanguage) & s__language(V__S,V__L))))) )
|
Merge.kif 1603-1609 | If X is an instance of writing, then there exist Y, Z such that Y is an instance of text, Z is an instance of written human language, and Z is a Language of Y. |
| ! [V__AGENT] : ((s__instance(V__AGENT,s__AutonomousAgent) => (? [V__PROC] : ((s__subclass(V__PROC,s__Process) & s__capability(V__PROC,s__agent,V__AGENT))))) )
|
Merge.kif 1656-1659 | If X is an instance of agent, then there exists Y such that X is capable of doing Y as a agent |
| ! [V__PROCESS] : ((s__instance(V__PROCESS,s__DualObjectProcess) => (? [V__OBJ1,V__OBJ2] : ((s__patient(V__PROCESS,V__OBJ1) & s__patient(V__PROCESS,V__OBJ2) & ~((V__OBJ1 = V__OBJ2)))))) )
|
Merge.kif 1731-1737 | If X is an instance of dual object process, then there exist Y, Z such that Y is a patient of X, Z is a patient of X, equal Y, and Z |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| statement |
|
|
| ! [V__GRAPH,V__NUMBER1,V__NUMBER2] : (((s__instance(V__GRAPH,s__Graph) & s__instance(V__NUMBER1,s__PositiveInteger) & s__instance(V__NUMBER2,s__PositiveInteger)) => ~((? [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 6218-6225 | There don't exist X, Y such that X is an instance of the set of paths that partition Z into two separate graphs, Y is an instance of the set of minimal paths that partition Z into two separate graphs, the length of X is W, the length of Y is V, and W is less than V |
| ! [V__T : $i] : (s__hasPurpose(s__IBookstore, ( ? [V__D:$i] : ((s__instance(V__D, s__DownloadingOverNetwork) & s__instrument(V__D, s__IBookstore) & s__instance(V__T, s__Text) & s__objectTransferred(V__D, V__T)))))) | ComputingBrands.kif 3216-3222 | IBookstore has the purpose there exists ?D such that ?D is an instance of downloading, iBookstore is an instrument for ?D, ?T is an instance of text, and the object transferred in ?D is ?T |
| appearance as argument number 0 |
|
|
|