Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| or |
| antecedent |
|
| ! [V__PATH,V__SUM,V__SUBPATH,V__ARC1,V__NUMBER1] : (((s__instance(V__PATH,s__GraphPath) & s__instance(V__SUM,s__RealNumber) & s__instance(V__SUBPATH,s__GraphPath) & s__instance(V__ARC1,s__GraphArc) & s__instance(V__NUMBER1,s__RealNumber)) => (((s__PathWeightFn(V__PATH) = V__SUM) & s__subGraph(V__SUBPATH,V__PATH) & s__graphPart(V__ARC1,V__PATH) & s__arcWeight(V__ARC1,V__NUMBER1) & (! [V__ARC2] : ((s__instance(V__ARC2,s__GraphElement) => (s__graphPart(V__ARC2,V__PATH) => (s__graphPart(V__ARC2,V__SUBPATH) | (V__ARC2 = V__ARC1))))))) => (V__SUM = s__AdditionFn(s__PathWeightFn(V__SUBPATH) ,V__NUMBER1)))) )
|
Merge.kif 6098-6110 | If equal the value of X and Y, Z is a subgraph of X, W is a part of X, the value of W is V, and For all GraphElement U: if U is a part of X, then U is a part of Z or equal U and W, then equal Y and (the value of Z and V) |
| ! [V__PATH,V__SUM,V__ARC1,V__ARC2,V__NUMBER1,V__NUMBER2] : (((s__instance(V__PATH,s__GraphPath) & s__instance(V__SUM,s__RealNumber) & s__instance(V__ARC1,s__GraphArc) & s__instance(V__ARC2,s__GraphArc) & s__instance(V__NUMBER1,s__RealNumber) & s__instance(V__NUMBER2,s__RealNumber)) => (((s__PathWeightFn(V__PATH) = V__SUM) & s__graphPart(V__ARC1,V__PATH) & s__graphPart(V__ARC2,V__PATH) & s__arcWeight(V__ARC1,V__NUMBER1) & s__arcWeight(V__ARC2,V__NUMBER2) & (! [V__ARC3] : ((s__instance(V__ARC3,s__GraphElement) => (s__graphPart(V__ARC3,V__PATH) => ((V__ARC3 = V__ARC1) | (V__ARC3 = V__ARC2))))))) => (s__PathWeightFn(V__PATH) = s__AdditionFn(V__NUMBER1,V__NUMBER2)))) )
|
Merge.kif 6112-6125 | If All of the following hold: (1) equal the value of X and Y (2) Z is a part of X (3) W is a part of X (4) the value of Z is V (5) the value of W is U (6) For all GraphElement T: if T is a part of X, then equal T and Z or equal T and W, then equal the value of X and (V and U) |
| ! [V__POINT1,V__POINT2] : (((s__instance(V__POINT1,s__TimePoint) & s__instance(V__POINT2,s__TimePoint)) => ((s__before(V__POINT1,V__POINT2) | (V__POINT1 = V__POINT2)) => s__beforeOrEqual(V__POINT1,V__POINT2))) )
|
Merge.kif 8353-8357 | If X happens before Y or equal X and Y, then X happens before or at Y |
| ! [V__STUFF,V__PROC] : ((s__instance(V__STUFF,s__Object) => ((s__instance(V__PROC,s__ChemicalProcess) & (s__resource(V__PROC,V__STUFF) | s__result(V__PROC,V__STUFF))) => s__instance(V__STUFF,s__PureSubstance))) )
|
Merge.kif 12804-12810 | If X is an instance of chemical process and Y is a resource for X or Y is a result of X, then Y is an instance of pure substance |
| ! [V__X] : (((s__instance(V__X,s__Substance) & (s__attribute(V__X,s__Gas) | s__attribute(V__X,s__Liquid) | s__attribute(V__X,s__Plasma))) => s__attribute(V__X,s__Fluid)) )
|
Merge.kif 17951-17958 | If X is an instance of substance and At least one of the following holds: (1) gas is an attribute of X (2) liquid is an attribute of X (3) plasma is an attribute of X, then fluid is an attribute of X |
| ! [V__AGENT] : ((s__instance(V__AGENT,s__Object) => ((s__attribute(V__AGENT,s__Asleep) | s__attribute(V__AGENT,s__Awake)) => s__attribute(V__AGENT,s__Living))) )
|
Merge.kif 18692-18696 | If asleep is an attribute of X or awake is an attribute of X, then living is an attribute of X |
| ! [V__S1START,V__S2START,V__A,V__S1,V__S2] : (((s__instance(V__S1START,s__TimePoint) & s__instance(V__S2START,s__TimePoint)) => ((s__instance(V__A,s__Ambulating) & s__subProcess(V__S1,V__A) & s__instance(V__S1,s__Stepping) & s__subProcess(V__S2,V__A) & s__instance(V__S2,s__Stepping) & (V__S1START = s__BeginFn(s__WhenFn(V__S1))) & (V__S2START = s__BeginFn(s__WhenFn(V__S2))) & ~((s__before(V__S1START,V__S2START) | s__before(V__S2START,V__S1START)))) => (V__S1 = V__S2))) )
|
Mid-level-ontology.kif 484-497 | If All of the following hold: (1) X is an instance of ambulating (2) Y is a subprocess of X (3) Y is an instance of stepping (4) Z is a subprocess of X (5) Z is an instance of stepping (6) equal W and the beginning of the time of existence of Y (7) equal V and the beginning of the time of existence of Z (8) ~{ W happens before V } and ~{ V happens before W }, then equal Y and Z |
| ! [V__HUMAN : $i,V__ROLE : $i,V__T1 : $i] : ((((s__instance(V__ROLE, s__OccupationalTrade) | s__instance(V__ROLE, s__Profession)) & s__holdsDuring(V__T1, s__attribute(V__HUMAN, V__ROLE))) => ( ? [V__FIELD:$i] : ((s__subclass(V__FIELD, s__FieldOfStudy) & s__holdsDuring(V__T1, s__hasExpertise(V__HUMAN, V__FIELD))))))) | Mid-level-ontology.kif 9653-9662 | If X is an instance of occupational trade or X is an instance of profession and X is an attribute of Y holds during Z, then there exists W such that W is a subclass of field of study and W has an expertise in Y holds during Z |
| ! [V__AGENT : $i,V__AGREEMENT : $i,V__ATTR : $i,V__PROP : $i] : (((s__agreementClause(V__PROP, V__ATTR, V__AGREEMENT, V__AGENT) & (V__ATTR = s__Obligation | V__ATTR = s__Promise)) => s__modalAttribute(( ? [V__PROC:$i] : ((s__realization(V__PROC, V__PROP) & s__agent(V__PROC, V__AGENT)))), s__Likely))) | Mid-level-ontology.kif 15680-15690 | If X has the responsibility to make Y Z in W and equal Z and obligation or equal Z and promise, then the statement there exists V such that V expresses the content of Y and X is an agent of V has the modal force of likely |
| ! [V__ATOM : $i,V__NUMBER : $int,V__SUBSTANCE : $i] : (((s__protonNumber(V__SUBSTANCE,V__NUMBER) & s__part(V__ATOM, V__SUBSTANCE) & (s__instance(V__ATOM, s__Atom) | s__instance(V__ATOM, s__Molecule))) => ( ? [V__PROTON:$i] : (V__NUMBER = s__CardinalityFn(s__KappaFn(V__PROTON, (s__part(V__PROTON, V__ATOM) & s__instance(V__PROTON, s__Proton)))))))) | Mid-level-ontology.kif 23961-23974 | If X is a proton number of Y, Z is a part of Y, and Z is an instance of atom or Z is an instance of molecule, then there exists W such that equal X and the number of instances in the class described by W |
| ! [V__ATOM : $i,V__NUMBER : $int,V__SUBSTANCE : $i] : (((s__electronNumber(V__SUBSTANCE,V__NUMBER) & s__part(V__ATOM, V__SUBSTANCE) & (s__instance(V__ATOM, s__Atom) | s__instance(V__ATOM, s__Molecule))) => ( ? [V__ELECTRON:$i] : (V__NUMBER = s__CardinalityFn(s__KappaFn(V__ELECTRON, (s__part(V__ELECTRON, V__ATOM) & s__instance(V__ELECTRON, s__Electron)))))))) | Mid-level-ontology.kif 23984-23997 | If X is an electron number of Y, Z is a part of Y, and Z is an instance of atom or Z is an instance of molecule, then there exists W such that equal X and the number of instances in the class described by W |
| ! [V__PLACE,V__GEO] : ((((s__located(V__PLACE,V__GEO) & s__instance(V__PLACE,s__PostalPlace) & (s__instance(V__GEO,s__Nation) | s__instance(V__GEO,s__DependencyOrSpecialSovereigntyArea))) => s__postCountry(V__PLACE,V__GEO)) & (s__postCountry(V__PLACE,V__GEO) => (s__located(V__PLACE,V__GEO) & s__instance(V__PLACE,s__PostalPlace) & (s__instance(V__GEO,s__Nation) | s__instance(V__GEO,s__DependencyOrSpecialSovereigntyArea))))) )
|
Mid-level-ontology.kif 26995-27002 | X is located at Y, X is an instance of postal place, Y is an instance of nation or Y is an instance of dependency or special sovereignty area if, and only if X is in Y |
| ! [V__PLACE,V__CITY,V__AREA] : (((s__instance(V__PLACE,s__PostalPlace) & s__instance(V__CITY,s__City)) => ((s__postCity(V__PLACE,V__CITY) & s__geographicSubregion(V__CITY,V__AREA) & (s__instance(V__AREA,s__Nation) | s__instance(V__AREA,s__DependencyOrSpecialSovereigntyArea))) => s__postCountry(V__PLACE,V__AREA))) )
|
Mid-level-ontology.kif 27011-27018 | If X is in Y, Y is a geographic subregion of Z, and Z is an instance of nation or Z is an instance of dependency or special sovereignty area, then X is in Z |
| ! [V__X : $i] : (((s__attribute(V__X, s__WheelchairAccessible) & (s__instance(V__X, s__Building) | s__instance(V__X, s__Room))) => s__modalAttribute(( ? [V__MOTION:$i, V__WHEELCHAIR:$i] : ((s__instance(V__MOTION, s__Motion) & s__instrument(V__MOTION, V__WHEELCHAIR) & s__instance(V__WHEELCHAIR, s__Wheelchair) & s__eventLocated(V__MOTION, V__X)))), s__Possibility))) | Mid-level-ontology.kif 28729-28741 | If wheelchair accessible is an attribute of X and X is an instance of building or X is an instance of room, then the statement there exist Y, Z such that Y is an instance of motion, Z is an instrument for Y, Z is an instance of wheelchair, and Y is located at X has the modal force of possibility |
| ! [V__H : $i,V__LA : $i,V__LL : $i,V__O : $i,V__RA : $i,V__RL : $i,V__T : $i] : (((s__holdsDuring(V__T, (s__attribute(V__H, s__LateralRecumbant) & s__orientation(V__H, V__O, s__On))) & s__instance(V__LA, s__LeftArm) & s__part(V__LA, V__H) & s__instance(V__RA, s__RightArm) & s__part(V__RA, V__H) & s__instance(V__LL, s__LeftLeg) & s__part(V__LL, V__H) & s__instance(V__RL, s__RightLeg) & s__part(V__RL, V__H) & (s__meetsSpatially(V__LA, V__O) | s__meetsSpatially(V__LL, V__O))) => s__holdsDuring(V__T, (~(s__meetsSpatially(V__RA, V__O)) & ~(s__meetsSpatially(V__RL, V__O)))))) | Anatomy.kif 1860-1882 | If All of the following hold: (1) lateral recumbant is an attribute of X and X is on to Y holds during Z (2) W is an instance of left arm (3) W is a part of X (4) V is an instance of right arm (5) V is a part of X (6) U is an instance of left leg (7) U is a part of X (8) T is an instance of right leg (9) T is a part of X (10) W meets Y or U meets Y, then V doesn't meet Y and T doesn't meet Y holds during Z |
| ! [V__H : $i,V__LA : $i,V__LL : $i,V__O : $i,V__RA : $i,V__RL : $i,V__T : $i] : (((s__holdsDuring(V__T, (s__attribute(V__H, s__LateralRecumbant) & s__orientation(V__H, V__O, s__On))) & s__instance(V__LA, s__LeftArm) & s__part(V__LA, V__H) & s__instance(V__RA, s__RightArm) & s__part(V__RA, V__H) & s__instance(V__LL, s__LeftLeg) & s__part(V__LL, V__H) & s__instance(V__RL, s__RightLeg) & s__part(V__RL, V__H) & (s__meetsSpatially(V__RA, V__O) | s__meetsSpatially(V__RL, V__O))) => s__holdsDuring(V__T, (~(s__meetsSpatially(V__LA, V__O)) & ~(s__meetsSpatially(V__LL, V__O)))))) | Anatomy.kif 1884-1906 | If All of the following hold: (1) lateral recumbant is an attribute of X and X is on to Y holds during Z (2) W is an instance of left arm (3) W is a part of X (4) V is an instance of right arm (5) V is a part of X (6) U is an instance of left leg (7) U is a part of X (8) T is an instance of right leg (9) T is a part of X (10) V meets Y or T meets Y, then W doesn't meet Y and U doesn't meet Y holds during Z |
| ! [V__X,V__CLASS,V__TEXT,V__WRITE] : (((s__instance(V__X,s__AutonomousAgent) & s__instance(V__CLASS,s__Class) & s__subclass(V__CLASS,s__ContentBearingObject)) => ((s__attribute(V__X,s__Writer) & s__instance(V__TEXT,V__CLASS) & (s__subclass(V__CLASS,s__Text) | s__subclass(V__CLASS,s__Document)) & s__instance(V__WRITE,s__Writing) & s__agent(V__WRITE,V__X) & s__result(V__WRITE,V__TEXT)) => s__authors(V__X,V__CLASS))) )
|
Biography.kif 733-743 | If All of the following hold: (1) writer is an attribute of X (2) Y is an instance of Z (3) Z is a subclass of text or Z is a subclass of document (4) W is an instance of writing (5) X is an agent of W (6) Y is a result of W, then X is the author of Z |
| ! [V__PERSON,V__WRITE,V__TEXT] : (((s__instance(V__PERSON,s__Human) & s__instance(V__WRITE,s__Writing) & (s__instance(V__TEXT,s__Text) | s__instance(V__TEXT,s__Document)) & s__result(V__WRITE,V__TEXT) & s__agent(V__WRITE,V__PERSON)) => s__attribute(V__PERSON,s__Writer)) )
|
Biography.kif 745-754 | If X is an instance of human, Y is an instance of writing, Z is an instance of text or Z is an instance of document, Z is a result of Y, and X is an agent of Y, then writer is an attribute of X |
| ! [V__AGENT : $i,V__B : $i,V__ENT : $i,V__ITEM : $i,V__PAY : $i,V__PRICE : $i,V__PS : $i,V__QUANT : $i] : (((s__instance(V__B, s__Buying) & s__patient(V__B, V__ITEM) & s__origin(V__B, V__AGENT) & (s__publishedPrice(V__ENT, V__PRICE, V__AGENT, V__PS) | s__unitPrice(V__ENT, V__QUANT, V__AGENT, V__PS)) & s__subclass(V__ENT, s__Physical) & s__immediateInstance(V__ITEM, V__ENT) & s__validPaymentType(V__PS, V__PAY)) => s__modalAttribute(( ? [V__PAYMENT:$i] : ((s__instance(V__PAYMENT, V__PAY) & s__subProcess(V__PAYMENT, V__B)))), s__Likely))) | Catalog.kif 337-352 | If All of the following hold: (1) X is an instance of buying (2) Y is a patient of X (3) X originates at Z (4) the price of W from Z according to V is U or the unit price charged Z under V for T is W (5) W is a subclass of physical (6) Y is an immediate instance of W (7) S is a valid payment under V, then the statement there exists R such that R is an instance of S and R is a subprocess of X has the modal force of likely |
| ! [V__AGENT : $i,V__B : $i,V__CUSTCLASS : $i,V__CUSTOMER : $i,V__ENT : $i,V__ITEM : $i,V__PRICE : $i,V__PS : $i,V__QUANT : $i] : ((((s__publishedPrice(V__ENT, V__PRICE, V__AGENT, V__PS) | s__unitPrice(V__ENT, V__QUANT, V__AGENT, V__PS)) & s__subclass(V__ENT, s__Physical) & s__immediateInstance(V__ITEM, V__ENT) & s__validFor(V__PS, V__CUSTCLASS) & s__instance(V__CUSTOMER, V__CUSTCLASS)) => s__modalAttribute(((s__instance(V__B, s__Buying) & s__agent(V__B, V__CUSTOMER) & s__origin(V__B, V__AGENT) & s__patient(V__B, V__ITEM)) => s__transactionAmount(V__B, V__PRICE)), s__Likely))) | Catalog.kif 354-370 | If the price of X from Y according to Z is W or the unit price charged Y under Z for V is X, X is a subclass of physical, U is an immediate instance of X, Z is valid for T, and S is an instance of T, then the statement R is an instance of buying, S is an agent of R, R originates at Y, and U is a patient of RW is a transaction amount of R has the modal force of likely |
| ! [V__AGENT : $i,V__ENT : $i,V__ITEM : $i,V__PRICE : $i,V__PS : $i,V__QUANT : $i,V__S : $i,V__TIMEINT : $i] : ((((s__publishedPrice(V__ENT, V__PRICE, V__AGENT, V__PS) | s__unitPrice(V__ENT, V__QUANT, V__AGENT, V__PS)) & s__subclass(V__ENT, s__Physical) & s__immediateInstance(V__ITEM, V__ENT) & s__validityPeriod(V__PS, V__TIMEINT)) => s__holdsDuring(V__TIMEINT, s__modalAttribute(((s__instance(V__S, s__Selling) & s__agent(V__S, V__AGENT) & s__patient(V__S, V__ITEM)) => s__transactionAmount(V__S, V__PRICE)), s__Likely)))) | Catalog.kif 372-387 | If the price of X from Y according to Z is W or the unit price charged Y under Z for V is X, X is a subclass of physical, U is an immediate instance of X, and Z is valid during T, then the statement S is an instance of selling, Y is an agent of S, and U is a patient of SW is a transaction amount of S has the modal force of likely holds during T |
| ! [V__AMOUNT : $i,V__AREA : $i,V__PERIOD : $i] : (((s__electricityProductionInPeriod(V__AREA, V__AMOUNT, V__PERIOD) & (s__subclass(V__PERIOD, s__Year) | s__subclass(V__PERIOD, s__FiscalYearFn(V__AREA)))) => ( ? [V__YEAR:$i] : ((s__instance(V__YEAR, V__PERIOD) & s__holdsDuring(V__YEAR, s__annualElectricityProduction(V__AREA, V__AMOUNT))))))) | Economy.kif 2215-2224 | If X is electricity production in period Y for Z and Z is a subclass of year or Z is a subclass of the fiscal year of X, then there exists W such that W is an instance of Z and Y is an annual electricity production of X holds during W |
| ! [V__AMOUNT : $i,V__AREA : $i,V__PERIOD : $i,V__YEAR : $i] : (((s__holdsDuring(V__YEAR, s__annualElectricityProduction(V__AREA, V__AMOUNT)) & s__instance(V__YEAR, V__PERIOD) & (s__subclass(V__PERIOD, s__Year) | s__subclass(V__PERIOD, s__FiscalYearFn(V__AREA)))) => s__electricityProductionInPeriod(V__AREA, V__AMOUNT, V__PERIOD))) | Economy.kif 2226-2233 | If X is an annual electricity production of Y holds during Z, Z is an instance of W, and W is a subclass of year or W is a subclass of the fiscal year of Y, then Y is electricity production in period X for W |
| ! [V__AMOUNT : $i,V__AREA : $i,V__PERIOD : $i] : (((s__electricityConsumptionInPeriod(V__AREA, V__AMOUNT, V__PERIOD) & (s__subclass(V__PERIOD, s__Year) | s__subclass(V__PERIOD, s__FiscalYearFn(V__AREA)))) => ( ? [V__YEAR:$i] : ((s__instance(V__YEAR, V__PERIOD) & s__holdsDuring(V__YEAR, s__annualElectricityConsumption(V__AREA, V__AMOUNT))))))) | Economy.kif 2347-2356 | If X is electricity consumption in period Y for Z and Z is a subclass of year or Z is a subclass of the fiscal year of X, then there exists W such that W is an instance of Z and Y is an annual electricity consumption of X holds during W |
| ! [V__AMOUNT : $i,V__AREA : $i,V__PERIOD : $i,V__YEAR : $i] : (((s__holdsDuring(V__YEAR, s__annualElectricityConsumption(V__AREA, V__AMOUNT)) & s__instance(V__YEAR, V__PERIOD) & (s__subclass(V__PERIOD, s__Year) | s__subclass(V__PERIOD, s__FiscalYearFn(V__AREA)))) => s__electricityConsumptionInPeriod(V__AREA, V__AMOUNT, V__PERIOD))) | Economy.kif 2358-2365 | If X is an annual electricity consumption of Y holds during Z, Z is an instance of W, and W is a subclass of year or W is a subclass of the fiscal year of Y, then Y is electricity consumption in period X for W |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| consequent |
|
|
| ! [V__REL,V__NUMBER,V__CLASS1,V__CLASS2] : (((s__instance(V__REL,s__Relation) & s__instance(V__NUMBER,s__PositiveInteger) & s__instance(V__CLASS1,s__Class) & s__instance(V__CLASS2,s__Class)) => ((s__domain(V__REL,V__NUMBER,V__CLASS1) & s__domain(V__REL,V__NUMBER,V__CLASS2)) => (s__subclass(V__CLASS1,V__CLASS2) | s__subclass(V__CLASS2,V__CLASS1)))) )
|
Merge.kif 215-221 | If the number X argument of Y is an instance of Z and the number X argument of Y is an instance of W, then Z is a subclass of W or W is a subclass of Z |
| ! [V__REL,V__NUMBER,V__CLASS1,V__CLASS2] : (((s__instance(V__REL,s__Relation) & s__instance(V__NUMBER,s__PositiveInteger) & s__instance(V__CLASS1,s__Class) & s__instance(V__CLASS2,s__Class)) => ((s__domainSubclass(V__REL,V__NUMBER,V__CLASS1) & s__domainSubclass(V__REL,V__NUMBER,V__CLASS2)) => (s__subclass(V__CLASS1,V__CLASS2) | s__subclass(V__CLASS2,V__CLASS1)))) )
|
Merge.kif 238-244 | If the number X argument of Y is a subclass of Z and the number X argument of Y is a subclass of W, then Z is a subclass of W or W is a subclass of Z |
| ! [V__REL,V__CLASS1,V__CLASS2] : (((s__instance(V__REL,s__Function) & s__instance(V__CLASS1,s__Class) & s__instance(V__CLASS2,s__Class)) => ((s__range(V__REL,V__CLASS1) & s__range(V__REL,V__CLASS2)) => (s__subclass(V__CLASS1,V__CLASS2) | s__subclass(V__CLASS2,V__CLASS1)))) )
|
Merge.kif 317-323 | If the range of X is an instance of Y and the range of X is an instance of Z, then Y is a subclass of Z or Z is a subclass of Y |
| ! [V__REL,V__CLASS1,V__CLASS2] : (((s__instance(V__REL,s__Function) & s__instance(V__CLASS1,s__Class) & s__subclass(V__CLASS1,s__Class) & s__instance(V__CLASS2,s__Class) & s__subclass(V__CLASS2,s__Class)) => ((s__rangeSubclass(V__REL,V__CLASS1) & s__rangeSubclass(V__REL,V__CLASS2)) => (s__subclass(V__CLASS1,V__CLASS2) | s__subclass(V__CLASS2,V__CLASS1)))) )
|
Merge.kif 343-349 | If the values returned by X are subclasses of Y and the values returned by X are subclasses of Z, then Y is a subclass of Z or Z is a subclass of Y |
| ! [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__AGENT : $i,V__TIME : $i] : (((s__holdsDuring(V__TIME, s__attribute(V__AGENT, s__LegalPersonhood)) => s__holdsDuring(V__TIME, (s__capability(s__LegalAction, s__agent, V__AGENT) | s__capability(s__LegalAction, s__patient, V__AGENT)))) & (s__holdsDuring(V__TIME, (s__capability(s__LegalAction, s__agent, V__AGENT) | s__capability(s__LegalAction, s__patient, V__AGENT))) => s__holdsDuring(V__TIME, s__attribute(V__AGENT, s__LegalPersonhood))))) | Merge.kif 1695-1701 | Legal personhood is an attribute of X holds during Y if and only if X is capable of doing legal action as a agent or X is capable of doing legal action as a patient holds during Y |
| ! [V__NUMBER1,V__NUMBER2] : (((s__instance(V__NUMBER1,s__RealNumber) & s__instance(V__NUMBER2,s__RealNumber)) => ((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 1970-1974 | X is less than, equal to Y if, only if equal X, and Y, or X is less than Y |
| ! [V__NUM] : ((s__instance(V__NUM,s__BinaryNumber) => ((V__NUM = n__1) | (V__NUM = n__0))) )
|
Merge.kif 2112-2116 | If X is an instance of binary number, then equal X and 1 or equal X and 0 |
| ! [V__REL : $i] : ((s__instance(V__REL, s__TrichotomizingRelation) => ( ! [V__INST1:$i, V__INST2:$i] : (((s__?REL(V__INST1, V__INST2) & ~(V__INST1 = V__INST2) & ~(s__?REL(V__INST2, V__INST1))) | (~(s__?REL(V__INST1, V__INST2)) & V__INST1 = V__INST2 & ~(s__?REL(V__INST2, V__INST1))) | (~(s__?REL(V__INST1, V__INST2)) & ~(V__INST1 = V__INST2) & s__?REL(V__INST2, V__INST1))))))) | Merge.kif 2426-2441 | If X is an instance of trichotomizing relation, then For all Entities Y and Z: At least one of the following holds: (1) X Y and Z, equal Y and Z, and X Z and Y (2) X Y and Z, equal Y and Z, and X Z and Y (3) X Y and Z, equal Y and Z, and X Z and Y |
| ! [V__REL : $i] : ((s__instance(V__REL, s__TotalOrderingRelation) => ( ! [V__INST1, V__INST2] : (((s__?REL(V__INST1, V__INST2) | s__?REL(V__INST2, V__INST1)) & (~(s__?REL(V__INST1, V__INST2)) | ~(s__?REL(V__INST2, V__INST1)))))))) | Merge.kif 2491-2500 | If X is an instance of total ordering relation, then For all Entities Y and Z: X Y and Z or X Z and Y and X Y and Z or X Z and Y |
| ! [V__FORMULA1 : $i,V__FORMULA2 : $i] : (((s__instance(V__FORMULA1, s__Formula) & s__instance(V__FORMULA2, s__Formula)) => (s__increasesLikelihood(V__FORMULA1, V__FORMULA2) | s__decreasesLikelihood(V__FORMULA1, V__FORMULA2) | s__independentProbability(V__FORMULA1, V__FORMULA2)))) | Merge.kif 2756-2763 | If X is an instance of formula and Y is an instance of formula, then At least one of the following holds: (1) X increases likelihood of Y (2) X decreases likelihood of Y (3) probability of X and Y is independent |
| ! [V__CLASS] : ((s__instance(V__CLASS,s__Class) => ((s__trichotomizingOn(s__greaterThanOrEqualTo,V__CLASS) & s__instance(s__greaterThanOrEqualTo,s__RelationExtendedToQuantities)) => (! [V__INST1,V__INST2] : (((s__instance(V__INST1,s__RealNumber) & s__instance(V__INST2,s__RealNumber)) => ((s__instance(V__INST1,V__CLASS) & s__instance(V__INST2,V__CLASS)) => (s__greaterThanOrEqualTo(V__INST1,V__INST2) | s__greaterThanOrEqualTo(V__INST2,V__INST1) | (V__INST1 = V__INST2)))))))) )
! [V__CLASS] :
! [V__CLASS] :
! [V__CLASS] :
|
Merge.kif 3796-3808 | If X is trichotomizing on Y and X is an instance of relation extended to quantities, then For all Entities Z and W: if Z is an instance of Y and W is an instance of Y, then At least one of the following holds: (1) X Z and W (2) X W and Z (3) equal Z and W |
| ! [V__OBJ1,V__OBJ2] : (((s__instance(V__OBJ1,s__Object) & s__instance(V__OBJ2,s__Object)) => (s__traverses(V__OBJ1,V__OBJ2) => (s__crosses(V__OBJ1,V__OBJ2) | s__penetrates(V__OBJ1,V__OBJ2)))) )
|
Merge.kif 4301-4305 | If X traverses Y, then X crosses Y or X penetrates Y |
| ! [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__NUMBER1,V__NUMBER2,V__NUMBER] : (((s__instance(V__NUMBER1,s__RealNumber) & s__instance(V__NUMBER2,s__RealNumber) & s__instance(V__NUMBER,s__Number)) => ((s__MaxFn(V__NUMBER1,V__NUMBER2) = V__NUMBER) => (((V__NUMBER = V__NUMBER1) & s__greaterThan(V__NUMBER1,V__NUMBER2)) | ((V__NUMBER = V__NUMBER2) & s__greaterThan(V__NUMBER2,V__NUMBER1)) | ((V__NUMBER = V__NUMBER1) & (V__NUMBER = V__NUMBER2))))) )
|
Merge.kif 5107-5118 | If equal the larger of X, Y, and Z, then At least one of the following holds: (1) equal Z and X and X is greater than Y (2) equal Z and Y and Y is greater than X (3) equal Z and X and equal Z and Y |
| ! [V__NUMBER1,V__NUMBER2,V__NUMBER] : (((s__instance(V__NUMBER1,s__RealNumber) & s__instance(V__NUMBER2,s__RealNumber) & s__instance(V__NUMBER,s__Number)) => ((s__MinFn(V__NUMBER1,V__NUMBER2) = V__NUMBER) => (((V__NUMBER = V__NUMBER1) & s__lessThan(V__NUMBER1,V__NUMBER2)) | ((V__NUMBER = V__NUMBER2) & s__lessThan(V__NUMBER2,V__NUMBER1)) | ((V__NUMBER = V__NUMBER1) & (V__NUMBER = V__NUMBER2))))) )
|
Merge.kif 5133-5144 | If equal the smaller of X, Y, and Z, then At least one of the following holds: (1) equal Z and X and X is less than Y (2) equal Z and Y and Y is less than X (3) equal Z and X and equal Z and Y |
| ! [V__PRIME] : ((s__instance(V__PRIME,s__PrimeNumber) => (! [V__NUMBER] : ((s__instance(V__NUMBER,s__Integer) => (((s__RemainderFn(V__PRIME,V__NUMBER) = n__0) & ~((V__NUMBER = n__0))) => ((V__NUMBER = n__1) | (V__NUMBER = V__PRIME))))))) )
|
Merge.kif 5266-5277 | If X is an instance of prime number, then For all Integer Y: if equal X mod Y and 0 and equal Y and 0, then equal Y and 1 or equal Y and X |
| ! [V__NUMBER] : ((s__instance(V__NUMBER,s__NonnegativeRealNumber) => ((s__SignumFn(V__NUMBER) = n__1) | (s__SignumFn(V__NUMBER) = n__0))) )
|
Merge.kif 5307-5311 | If X is an instance of nonnegative real number, then equal the sign of X and 1 or equal the sign of X and 0 |
| ! [V__GRAPH,V__NODE1,V__NODE2] : (((s__instance(V__GRAPH,s__Graph) & s__instance(V__NODE1,s__GraphNode) & s__instance(V__NODE2,s__GraphNode) & s__graphPart(V__NODE1,V__GRAPH) & s__graphPart(V__NODE2,V__GRAPH) & ~((V__NODE1 = V__NODE2))) => (? [V__ARC,V__PATH] : ((s__instance(V__ARC,s__GraphArc) & (s__links(V__NODE1,V__NODE2,V__ARC) | (s__subGraph(V__PATH,V__GRAPH) & s__instance(V__PATH,s__GraphPath) & (((s__BeginNodeFn(V__PATH) = V__NODE1) & (s__EndNodeFn(V__PATH) = V__NODE2)) | ((s__BeginNodeFn(V__PATH) = V__NODE2) & (s__EndNodeFn(V__PATH) = V__NODE1))))))))) )
|
Merge.kif 5750-5770 | If All of the following hold: (1) X is an instance of graph (2) Y is an instance of graph node (3) Z is an instance of graph node (4) Y is a part of X (5) Z is a part of X (6) equal Y and Z, then All of the following hold: (1) there exist W (2) V such that W links Y (3) Z, V is a subgraph of X (4) V is an instance of graph path (5) equal the beginning of V (6) Y (7) equal the end of V (8) Z, or equal the beginning of V (9) Z (10) equal the end of V (11) Y |
| ! [V__POINT1,V__POINT2] : (((s__instance(V__POINT1,s__TimePoint) & s__instance(V__POINT2,s__TimePoint)) => (s__beforeOrEqual(V__POINT1,V__POINT2) => (s__before(V__POINT1,V__POINT2) | (V__POINT1 = V__POINT2)))) )
|
Merge.kif 8347-8351 | If X happens before or at Y, then X happens before Y or equal X and Y |
| ! [V__NUMBER,V__LEAP] : ((s__instance(V__NUMBER,s__Integer) => ((s__instance(V__LEAP,s__LeapYear) & s__instance(V__LEAP,s__YearFn(V__NUMBER))) => (((s__RemainderFn(V__NUMBER,n__4) = n__0) & ~((s__RemainderFn(V__NUMBER,n__100) = n__0))) | (s__RemainderFn(V__NUMBER,n__400) = n__0)))) )
|
Merge.kif 9203-9211 | If X is an instance of leap year and X is an instance of the year Y, then equal Y mod 4 and 0 and equal Y mod 100 and 0 or equal Y mod 400 and 0 |
| ! [V__INTERVAL,V__INTERVALTYPE,V__CLASS] : (((s__instance(V__INTERVAL,s__TimeInterval) & s__subclass(V__INTERVALTYPE,s__TimeInterval) & s__instance(V__CLASS,s__Class) & s__subclass(V__CLASS,s__TimeInterval)) => ((s__TemporalCompositionFn(V__INTERVAL,V__INTERVALTYPE) = V__CLASS) => (! [V__TIME1,V__TIME2] : (((s__instance(V__TIME1,s__TimeInterval) & s__instance(V__TIME2,s__TimeInterval)) => ((s__instance(V__TIME1,V__CLASS) & s__instance(V__TIME2,V__CLASS) & ~((V__TIME1 = V__TIME2))) => (s__meetsTemporally(V__TIME1,V__TIME2) | s__meetsTemporally(V__TIME2,V__TIME1) | s__earlier(V__TIME1,V__TIME2) | s__earlier(V__TIME2,V__TIME1)))))))) )
|
Merge.kif 9620-9632 | If equal decomposition of X into Y and Z, then For all TimeIntervals W and V: if equal W and V, then At least one of the following holds: (1) W meets V (2) V meets W (3) W happens earlier than V (4) V happens earlier than W |
| ! [V__OBJ1,V__OBJ2] : (((s__instance(V__OBJ1,s__Object) & s__instance(V__OBJ2,s__Object)) => (s__connected(V__OBJ1,V__OBJ2) => (s__meetsSpatially(V__OBJ1,V__OBJ2) | s__overlapsSpatially(V__OBJ1,V__OBJ2)))) )
|
Merge.kif 9734-9738 | If X is connected to Y, then X meets Y or X and Y overlapsSpatially |
| ! [V__OBJ3,V__OBJ1,V__OBJ2] : (((s__instance(V__OBJ3,s__Object) & s__instance(V__OBJ1,s__Object) & s__instance(V__OBJ2,s__Object)) => ((V__OBJ3 = s__MereologicalSumFn(V__OBJ1,V__OBJ2)) => (! [V__PART] : ((s__instance(V__PART,s__Object) => ((s__part(V__PART,V__OBJ3) => (s__part(V__PART,V__OBJ1) | s__part(V__PART,V__OBJ2))) & ((s__part(V__PART,V__OBJ1) | s__part(V__PART,V__OBJ2)) => s__part(V__PART,V__OBJ3)))))))) )
|
Merge.kif 10023-10030 | If equal X, the union of the parts of Y, and Z, then For all Object W: W is a part of X if and only if W is a part of Y or W is a part of Z |
| ! [V__HOLE,V__OBJ1,V__OBJ2] : (((s__instance(V__HOLE,s__HoleRegion) & s__instance(V__OBJ1,s__SelfConnectedObject) & s__instance(V__OBJ2,s__SelfConnectedObject)) => ((s__hole(V__HOLE,V__OBJ1) & s__part(V__OBJ1,V__OBJ2)) => (s__overlapsSpatially(V__HOLE,V__OBJ2) | s__hole(V__HOLE,V__OBJ2)))) )
|
Merge.kif 10130-10136 | If X is a hole in Y and Y is a part of Z, then X and Z overlapsSpatially or X is a hole in Z |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| statement |
|
|
| ! [V__AGE : $i,V__AGEMINUSONE : $i,V__AREA : $i,V__MILITARYAGE : $i,V__PERSON : $i,V__YEAR : $i] : (s__ReachingMilitaryAgeAnnuallyMaleFn(V__AREA, V__YEAR) = s__CardinalityFn(s__KappaFn(V__PERSON, (s__instance(V__PERSON, s__Human) & s__attribute(V__PERSON, s__Male) & s__militaryAge(V__AREA, V__MILITARYAGE) & V__AGEMINUSONE = $difference(V__AGE ,1) & s__holdsDuring(V__YEAR, (s__age(V__PERSON, V__AGEMINUSONE) | s__age(V__PERSON, V__AGE))) & V__AGE = V__MILITARYAGE & s__inhabits(V__PERSON, V__AREA))))) | Military.kif 1197-1210 | equal the reaching military age annually male of X, Y, and the number of instances in the class described by Z |
|