  forall
|
|
Sigma KEE - forall
|
antecedent
|
|
|
(=>
(and
(equal
(PathWeightFn ?PATH) ?SUM)
(subGraph ?SUBPATH ?PATH)
(graphPart ?ARC1 ?PATH)
(arcWeight ?ARC1 ?NUMBER1)
(forall (?ARC2)
(=>
(graphPart ?ARC2 ?PATH)
(or
(graphPart ?ARC2 ?SUBPATH)
(equal ?ARC2 ?ARC1)))))
(equal ?SUM
(AdditionFn
(PathWeightFn ?SUBPATH) ?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) |
(=>
(and
(equal
(PathWeightFn ?PATH) ?SUM)
(graphPart ?ARC1 ?PATH)
(graphPart ?ARC2 ?PATH)
(arcWeight ?ARC1 ?NUMBER1)
(arcWeight ?ARC2 ?NUMBER2)
(forall (?ARC3)
(=>
(graphPart ?ARC3 ?PATH)
(or
(equal ?ARC3 ?ARC1)
(equal ?ARC3 ?ARC2)))))
(equal
(PathWeightFn ?PATH)
(AdditionFn ?NUMBER1 ?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) |
(<=>
(holdsDuring ?T
(and
(instance ?PERSON Human)
(forall (?ORG)
(not
(employs ?ORG ?PERSON)))))
(holdsDuring ?T
(attribute ?PERSON Unemployed))) |
Merge.kif 17604-17612 |
X is an instance of human, Y Y doesn't employ X holds during Z if, and only if unemployed person is an attribute of X holds during Z |
(=>
(and
(climateTypeInArea ?AREA ColdClimateZone)
(forall (?MO)
(and
(instance ?MO Month)
(averageTemperatureForPeriod ?AREA ?MO
(MeasureFn ?TEMP CelsiusDegree)))))
(greaterThan 10.0 ?TEMP)) |
Geography.kif 2979-2987 |
If cold climate zone is a climate type in area of X and For all TimeInterval Y: Y is an instance of month and X average temperature for period Y for Z celsius degree(s), then 10.0 is greater than Z |
(=>
(and
(instance ?COLL Collection)
(instance ?SITE WebSite)
(instance ?AGENT AutonomousAgent)
(instance ?LISTING WebListing)
(instance ?TIME TimePoint)
(listingSeller ?LISTING ?AGENT)
(not
(member ?LISTING ?COLL))
(forall (?ITEM ?MEMBER)
(and
(=>
(and
(instance ?ITEM WebListing)
(member ?ITEM
(SellersItemsFn ?AGENT ?SITE))
(temporalPart ?TIME
(WhenFn ?ITEM))
(not
(equal ?ITEM ?LISTING)))
(member ?ITEM ?COLL))
(=>
(member ?MEMBER ?COLL)
(and
(temporalPart ?TIME
(WhenFn ?ITEM))
(instance ?MEMBER WebListing))))))
(equal
(SellersOtherItemsFn ?AGENT ?SITE ?LISTING ?TIME) ?COLL)) |
UXExperimentalTerms.kif 1033-1060 |
If All of the following hold: (1) X is an instance of collection (2) Y is an instance of web site (3) Z is an instance of agent (4) W is an instance of web listing (5) V is an instance of time point (6) Z sells W (7) W is not a member of X (8) For all Physicals U and T: if U is an instance of web listing, U is a member of items for sale by Z at Y, V is a part of the time of existence of U, and equal U and W, then U is a member of X and if T is a member of X, then V is a part of the time of existence of U and T is an instance of web listing, then equal things for sale by Z not listed in W at Y during V and X |
(=>
(and
(instance ?COLL Collection)
(forall (?MEMBER)
(=>
(member ?MEMBER ?COLL)
(instance ?MEMBER WebListing))))
(exists (?LISTING ?SITE ?ITEM)
(equal
(DivisionFn
(CardinalityFn
(KappaFn ?LISTING
(and
(instance ?LISTING WebListing)
(instance ?SITE WebSite)
(instance ?ITEM Physical)
(member ?LISTING ?COLL)
(patient ?LISTING ?ITEM)
(hostedOn ?LISTING ?SITE)
(exists (?BUYING)
(and
(instance ?BUYING Buying)
(patient ?BUYING ?ITEM)
(eCommerceSite ?BUYING ?SITE))))))
(CardinalityFn ?COLL))
(BidCountFn ?COLL)))) |
UXExperimentalTerms.kif 2846-2871 |
If X is an instance of collection and For all Physical Y: if Y is a member of X, then Y is an instance of web listing, then there exist Z, W, V such that equal the number of instances in the class described by Z, the number of instances in X, and number of bids in X |
(=>
(and
(instance ?COLL Collection)
(forall (?MEMBER)
(=>
(member ?MEMBER ?COLL)
(instance ?MEMBER FinancialTransaction))))
(exists (?ITEM ?BUYING)
(equal
(CardinalityFn
(KappaFn ?ITEM
(and
(instance ?ITEM Physical)
(instance ?BUYING Buying)
(member ?BUYING ?COLL)
(patient ?BUYING ?ITEM))))
(BoughtItemsFn ?COLL)))) |
UXExperimentalTerms.kif 2887-2903 |
If X is an instance of collection and For all Physical Y: if Y is a member of X, then Y is an instance of financial transaction, then there exist Z, W such that equal the number of instances in the class described by Z, and number of items purchased in X |
(=>
(and
(instance ?COLL Collection)
(forall (?MEMBER)
(=>
(member ?MEMBER ?COLL)
(instance ?MEMBER WebListing))))
(exists (?BIDDING ?ITEM ?LISTING ?BIDDING)
(equal
(CardinalityFn
(KappaFn ?BIDDING
(and
(instance ?ITEM Physical)
(instance ?LISTING WebListing)
(instance ?BIDDING Bidding)
(member ?LISTING ?COLL)
(objectOfBid ?BIDDING ?ITEM)
(patient ?LISTING ?ITEM))))
(BidCountFn ?COLL)))) |
UXExperimentalTerms.kif 2922-2940 |
If X is an instance of collection and For all Physical Y: if Y is a member of X, then Y is an instance of web listing, then there exist Z, W,, , V, Z such that equal the number of instances in the class described by Z, and number of bids in X |
(=>
(and
(instance ?PURCHASES Collection)
(forall (?MEMBER)
(=>
(member ?MEMBER ?PURCHASES)
(instance ?MEMBER Buying)))
(exists (?REGION)
(and
(instance ?REGION GeopoliticalArea)
(forall (?BUYER ?BUYING)
(=>
(and
(instance ?BUYER AutonomousAgent)
(instance ?BUYING Buying)
(member ?BUYING ?PURCHASES)
(agent ?BUYING ?BUYER))
(located ?BUYER ?REGION))))))
(exists (?AMOUNT ?PURCHASE ?TOTAL_PURCHASE_AMOUNT)
(and
(total
(KappaFn ?AMOUNT
(and
(instance ?PURCHASE Buying)
(member ?PURCHASE ?PURCHASES)
(transactionAmount ?PURCHASE ?AMOUNT))) ?TOTAL_PURCHASE_AMOUNT)
(equal
(GMBFn ?PURCHASES) ?TOTAL_PURCHASE_AMOUNT)))) |
UXExperimentalTerms.kif 2956-2983 |
If X is an instance of collection, For all Physical Y: if Y is a member of X, then Y is an instance of buying, and there exists Z such that Z is an instance of geopolitical area, W, V W is an instance of agent, V is an instance of buying, V is a member of X, and W is an agent of VW is located at Z, then there exist U, T, ?TOTAL_PURCHASE_AMOUNT such that the total of values in the class described by U is ?TOTAL_PURCHASE_AMOUNT, equal the value of X, and ?TOTAL_PURCHASE_AMOUNT |
(=>
(and
(instance ?SALES Collection)
(forall (?MEMBER)
(=>
(member ?MEMBER ?SALES)
(instance ?MEMBER Selling)))
(exists (?REGION)
(and
(instance ?REGION GeopoliticalArea)
(forall (?SELLER ?SELLING)
(=>
(and
(instance ?SELLER AutonomousAgent)
(instance ?SELLING Buying)
(member ?SELLING ?SALES)
(agent ?SELLING ?SELLER))
(located ?SELLER ?REGION))))))
(exists (?AMOUNT ?SALE ?TOTAL_SALE_AMOUNT)
(and
(total
(KappaFn ?AMOUNT
(and
(instance ?SALE Selling)
(member ?SALE ?SALES)
(transactionAmount ?SALE ?AMOUNT))) ?TOTAL_SALE_AMOUNT)
(equal
(GMVFn ?SALES) ?TOTAL_SALE_AMOUNT)))) |
UXExperimentalTerms.kif 2999-3026 |
If X is an instance of collection, For all Physical Y: if Y is a member of X, then Y is an instance of selling, and there exists Z such that Z is an instance of geopolitical area, W, V W is an instance of agent, V is an instance of buying, V is a member of X, and W is an agent of VW is located at Z, then there exist U, T, ?TOTAL_SALE_AMOUNT such that the total of values in the class described by U is ?TOTAL_SALE_AMOUNT, equal the value of X, and ?TOTAL_SALE_AMOUNT |
(=>
(and
(instance ?VISITS Collection)
(instance ?HYPERLINK HypertextLink)
(forall (?ACCESSING)
(and
(member ?ACCESSING ?PAGE)
(and
(instance ?ACCESSING AccessingWebPage)
(component ?PAGE ?HYPERLINK)))))
(exists (?CLICKS)
(and
(instance ?CLICKS Collection)
(forall (?CLICK)
(=>
(and
(instance ?CLICK RequestingHyperlink)
(patient ?CLICK ?HYPERLINK))
(member ?CLICK ?CLICKS)))
(equal
(ClickThroughRateFn ?VISITS ?HYPERLINK)
(DivisionFn
(CardinalityFn ?CLICKS)
(CardinalityFn ?VISITS)))))) |
UXExperimentalTerms.kif 3332-3355 |
If X is an instance of collection, Y is an instance of hyperlink, and For all Physical Z: Z is a member of W and Z is an instance of accessing web page and W is a component of Y, then there exists V such that V is an instance of collection, U U is an instance of requesting hyperlink, Y is a patient of UU is a member of V, equal the rate of clicking through Y in X, the number of instances in V, and the number of instances in X |
(=>
(and
(instance ?VISITS Collection)
(instance ?PURCHASES Collection)
(subCollection ?PURCHASES ?VISITS)
(forall (?MEMBER)
(=>
(member ?MEMBER ?VISITS)
(instance ?MEMBER AccessingWebPage)))
(forall (?BUYING ?VISITOR ?ACCESSING ?BUYING ?PAGE)
(=>
(and
(instance ?VISITOR Human)
(instance ?BUYING Buying)
(instance ?ACCESSING AccessingWebPage)
(instance ?PAGE WebPage)
(member ?ACCESSING ?VISITS)
(destination ?ACCESSING ?PAGE)
(agent ?BUYING ?VISITOR)
(agent ?ACCESSING ?VISITOR)
(during
(WhenFn ?BUYING)
(WhenFn ?ACCESSING))
(instrument ?BUYING ?PAGE))
(member ?BUYING ?PURCHASES))))
(exists (?INTERVAL ?PURCHASE_IN_INTERVAL ?VISIT_IN_INTERVAL)
(equal
(SCRFn ?VISITS ?INTERVAL)
(DivisionFn
(CardinalityFn
(KappaFn ?PURCHASE_IN_INTERVAL
(and
(member ?PURCHASE_IN_INTERVAL ?PURCHASES)
(during
(WhenFn ?PURCHASE_IN_INTERVAL) ?INTERVAL))))
(CardinalityFn
(KappaFn ?VISIT_IN_INTERVAL
(and
(member ?VISIT_IN_INTERVAL ?VISITS)
(during
(WhenFn ?PURCHASE_IN_INTERVAL) ?INTERVAL)))))))) |
UXExperimentalTerms.kif 3665-3701 |
If X is an instance of collection, Y is an instance of collection, Y is a proper sub-collection of X, For all Physical Z: if Z is a member of X, then Z is an instance of accessing web page, and For all Processes W, U, and W, AutonomousAgent V, and Object T: if All of the following hold: (1) V is an instance of human (2) W is an instance of buying (3) U is an instance of accessing web page (4) T is an instance of web page (5) U is a member of X (6) U ends up at T (7) V is an agent of W (8) V is an agent of U (9) the time of existence of W takes place during the time of existence of U (10) T is an instrument for W, then W is a member of Y, then there exist S, ?PURCHASE_IN_INTERVAL, ?VISIT_IN_INTERVAL such that equal purchases made in X during S, the number of instances in the class described by ?PURCHASE_IN_INTERVAL, and the number of instances in the class described by ?VISIT_IN_INTERVAL |
(=>
(and
(instance ?VISITOR Human)
(instance ?QPVIEWS Collection)
(forall (?PAGE ?ACCESSING ?EXPERIMENT)
(=>
(and
(instance ?PAGE WebPage)
(instance ?ACCESSING AccessingWebPage)
(instance ?EXPERIMENT Experimenting)
(agent ?ACCESSING ?VISITOR)
(patient ?ACCESSING ?PAGE)
(treatedPage ?PAGE ?EXPERIMENT))
(member ?ACCESSING ?QPVIEWS))))
(equal ?QPVIEWS
(QPViewsFn ?VISITOR))) |
UXExperimentalTerms.kif 4172-4187 |
If X is an instance of human, Y is an instance of collection, and For all WebPage Z, Process W, and Experimenting V: if W is an instance of accessing web page, X is an agent of W, Z is a patient of W, and Z is the object of study of V, then W is a member of Y, then equal Y and all the treated web page views from X |
(=>
(and
(instance ?VISITOR Human)
(instance ?COLL Collection)
(forall (?EXPERIMENT ?EVENT)
(=>
(exists (?CLASS)
(and
(instance ?EXPERIMENT Experimenting)
(instance ?EVENT Process)
(member ?EVENT
(QualifyingEventsFn ?EXPERIMENT))
(instance ?EVENT ?CLASS)
(capability ?CLASS experiencer ?VISITOR)))
(member ?EVENT ?COLL)))
(=>
(member ?PROC ?COLL)
(and
(instance ?PROC Process)
(exists (?EXP ?PROCESS)
(and
(instance ?EXP Experimenting)
(member ?PROC
(QualifyingEventsFn ?EXP))
(instance ?PROC ?PROCESS)
(capability ?PROCESS experiencer ?VISITOR))))))
(equal
(QualifiedTreatmentsFn ?VISITOR) ?COLL)) |
UXExperimentalTerms.kif 4238-4264 |
If X is an instance of human, Y is an instance of collection, For all Experimenting Z and Physical W: if there exists V such that Z is an instance of experimenting, W is an instance of process, W is a member of events in Z, W is an instance of V, and X is capable of doing V as a experiencer, then W is a member of Y, and if U is a member of Y, then U is an instance of process and there exist T, S such that T is an instance of experimenting, U is a member of events in T, U is an instance of S, and X is capable of doing S as a experiencer, then equal all the processes X is qualified for and Y |
|
consequent
|
|
|
(=>
(equal ?THING1 ?THING2)
(forall (?ATTR)
(<=>
(property ?THING1 ?ATTR)
(property ?THING2 ?ATTR)))) |
Merge.kif 254-259 |
If equal X and Y, then For all Attribute Z: X the attribute Z if and only if Y the attribute Z |
(=>
(equal ?ATTR1 ?ATTR2)
(forall (?THING)
(<=>
(property ?THING ?ATTR1)
(property ?THING ?ATTR2)))) |
Merge.kif 261-266 |
If equal X and Y, then For all Entity Z: Z the attribute X if and only if Z the attribute Y |
(=>
(equal ?THING1 ?THING2)
(forall (?CLASS)
(<=>
(instance ?THING1 ?CLASS)
(instance ?THING2 ?CLASS)))) |
Merge.kif 268-273 |
If equal X and Y, then For all Class Z: X is an instance of Z if and only if Y is an instance of Z |
(=>
(equal ?CLASS1 ?CLASS2)
(forall (?THING)
(<=>
(instance ?THING ?CLASS1)
(instance ?THING ?CLASS2)))) |
Merge.kif 275-280 |
If equal X and Y, then For all Entity Z: Z is an instance of X if and only if Z is an instance of Y |
(=>
(exhaustiveAttribute ?CLASS @ROW)
(forall (?ATTR1)
(=>
(instance ?ATTR1 ?CLASS)
(exists (?ATTR2)
(and
(inList ?ATTR2
(ListFn @ROW))
(equal ?ATTR1 ?ATTR2)))))) |
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 |
(=>
(subAttribute ?ATTR1 ?ATTR2)
(forall (?OBJ)
(=>
(property ?OBJ ?ATTR1)
(property ?OBJ ?ATTR2)))) |
Merge.kif 681-686 |
If X is a subattribute of Y, then For all Entity Z: if Z the attribute X, then Z the attribute Y |
(=>
(piece ?SUBSTANCE1 ?SUBSTANCE2)
(forall (?CLASS)
(=>
(instance ?SUBSTANCE1 ?CLASS)
(instance ?SUBSTANCE2 ?CLASS)))) |
Merge.kif 967-972 |
If X is a piece of Y, then For all Class Z: if X is an instance of Z, then Y is an instance of Z |
(=>
(instance ?ATOM Atom)
(forall (?NUCLEUS1 ?NUCLEUS2)
(=>
(and
(part ?NUCLEUS1 ?ATOM)
(part ?NUCLEUS2 ?ATOM)
(instance ?NUCLEUS1 AtomicNucleus)
(instance ?NUCLEUS2 AtomicNucleus))
(equal ?NUCLEUS1 ?NUCLEUS2)))) |
Merge.kif 1195-1204 |
If X is an instance of atom, then For all Objects Y and Z: if Y is a part of X, Z is a part of X, Y is an instance of atomic nucleus, and Z is an instance of atomic nucleus, then equal Y and Z |
(<=>
(subCollection ?COLL1 ?COLL2)
(forall (?MEMBER)
(=>
(member ?MEMBER ?COLL1)
(member ?MEMBER ?COLL2)))) |
Merge.kif 1370-1375 |
X is a proper sub-collection of Y if and only if Z Z is a member of XZ is a member of Y |
(=>
(instance ?REL IrreflexiveRelation)
(forall (?INST)
(not
(?REL ?INST ?INST)))) |
Merge.kif 2364-2368 |
If X is an instance of irreflexive relation, then For all Entity Y: X Y and Y |
(=>
(instance ?REL SymmetricRelation)
(forall (?INST1 ?INST2)
(=>
(?REL ?INST1 ?INST2)
(?REL ?INST2 ?INST1)))) |
Merge.kif 2377-2382 |
If X is an instance of symmetric relation, then For all Entities Y and Z: if X Y and Z, then X Z and Y |
(=>
(instance ?REL AntisymmetricRelation)
(forall (?INST1 ?INST2)
(=>
(and
(?REL ?INST1 ?INST2)
(?REL ?INST2 ?INST1))
(equal ?INST1 ?INST2)))) |
Merge.kif 2411-2418 |
If X is an instance of antisymmetric relation, then For all Entities Y and Z: if X Y and Z and X Z and Y, then equal Y and Z |
(=>
(instance ?REL TrichotomizingRelation)
(forall (?INST1 ?INST2)
(or
(and
(?REL ?INST1 ?INST2)
(not
(equal ?INST1 ?INST2))
(not
(?REL ?INST2 ?INST1)))
(and
(not
(?REL ?INST1 ?INST2))
(equal ?INST1 ?INST2)
(not
(?REL ?INST2 ?INST1)))
(and
(not
(?REL ?INST1 ?INST2))
(not
(equal ?INST1 ?INST2))
(?REL ?INST2 ?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 |
(=>
(instance ?REL TransitiveRelation)
(forall (?INST1 ?INST2 ?INST3)
(=>
(and
(?REL ?INST1 ?INST2)
(?REL ?INST2 ?INST3))
(?REL ?INST1 ?INST3)))) |
Merge.kif 2450-2457 |
If X is an instance of transitive relation, then For all Entities Y, Z, and W: if X Y and Z and X Z and W, then X Y and W |
(=>
(instance ?REL IntransitiveRelation)
(forall (?INST1 ?INST2 ?INST3)
(=>
(and
(?REL ?INST1 ?INST2)
(?REL ?INST2 ?INST3))
(not
(?REL ?INST1 ?INST3))))) |
Merge.kif 2465-2473 |
If X is an instance of intransitive relation, then For all Entities Y, Z, and W: if X Y and Z and X Z and W, then X Y and W |
(=>
(instance ?REL TotalOrderingRelation)
(forall (?INST1 ?INST2)
(and
(or
(?REL ?INST1 ?INST2)
(?REL ?INST2 ?INST1))
(or
(not
(?REL ?INST1 ?INST2))
(not
(?REL ?INST2 ?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 |
(=>
(instance ?LIST UniqueList)
(forall (?NUMBER1 ?NUMBER2)
(=>
(equal
(ListOrderFn ?LIST ?NUMBER1)
(ListOrderFn ?LIST ?NUMBER2))
(equal ?NUMBER1 ?NUMBER2)))) |
Merge.kif 3021-3026 |
If X is an instance of unique list, then For all PositiveIntegers Y and Z: if equal W element of X and V element of X, then equal Y and Z |
(=>
(exhaustiveDecomposition ?CLASS @ROW)
(forall (?OBJ)
(=>
(instance ?OBJ ?CLASS)
(exists (?ITEM)
(and
(inList ?ITEM
(ListFn @ROW))
(instance ?OBJ ?ITEM)))))) |
Merge.kif 3051-3059 |
If X is covered by @ROW, then For all Entity Z: if Z is an instance of X, then there exists W such that W is a member of (@ROW) and Z is an instance of W |
(=>
(disjointDecomposition ?CLASS @ROW)
(forall (?ITEM)
(=>
(inList ?ITEM
(ListFn @ROW))
(subclass ?ITEM ?CLASS)))) |
Merge.kif 3061-3066 |
If X is disjointly decomposed into @ROW, then For all Class Z: if Z is a member of (@ROW), then Z is a subclass of X |
(=>
(disjointDecomposition ?CLASS @ROW)
(forall (?ITEM1 ?ITEM2)
(=>
(and
(inList ?ITEM1
(ListFn @ROW))
(inList ?ITEM2
(ListFn @ROW))
(not
(equal ?ITEM1 ?ITEM2)))
(disjoint ?ITEM1 ?ITEM2)))) |
Merge.kif 3068-3077 |
If X is disjointly decomposed into @ROW, then For all Classes Z and W: if Z is a member of (@ROW), W is a member of (@ROW), and equal Z and W, then Z is disjoint from W |
(=>
(and
(valence ?REL ?NUMBER)
(instance ?REL Predicate))
(forall (@ROW)
(=>
(?REL @ROW)
(equal
(ListLengthFn
(ListFn @ROW)) ?NUMBER)))) |
Merge.kif 3159-3166 |
If X has Y argument(s) and X is an instance of predicate, then for all : if X @ROW, then equal length of (@ROW) and Y |
(=>
(instance ?FUN OneToOneFunction)
(forall (?ARG1 ?ARG2)
(=>
(exists (?CLASS)
(and
(domain ?FUN 1 ?CLASS)
(instance ?ARG1 ?CLASS)
(instance ?ARG2 ?CLASS)
(not
(equal ?ARG1 ?ARG2))))
(not
(equal
(AssignmentFn ?FUN ?ARG1)
(AssignmentFn ?FUN ?ARG2)))))) |
Merge.kif 3488-3498 |
If X is an instance of one to one function, then For all Entities Y and Z: if there exists W such that the number 1 argument of X is an instance of W, Y is an instance of W, Z is an instance of W, equal Y, and Z, then equal X(Y) and X(Z) |
(=>
(instance ?FUNCTION AssociativeFunction)
(forall (?INST1 ?INST2 ?INST3 ?CLASS)
(=>
(and
(domain ?FUNCTION 1 ?CLASS)
(instance ?INST1 ?CLASS)
(instance ?INST2 ?CLASS)
(instance ?INST3 ?CLASS))
(equal
(AssignmentFn ?FUNCTION ?INST1
(AssignmentFn ?FUNCTION ?INST2 ?INST3))
(AssignmentFn ?FUNCTION
(AssignmentFn ?FUNCTION ?INST1 ?INST2) ?INST3))))) |
Merge.kif 3531-3541 |
If X is an instance of associative function, then For all Entities Y, Z, and W and Class V: if the number 1 argument of X is an instance of V, Y is an instance of V, Z is an instance of V, and W is an instance of V, then equal X(Y and X(Z and W)) and X(X(Y and Z) and W) |
(=>
(instance ?FUNCTION CommutativeFunction)
(forall (?INST1 ?INST2 ?CLASS)
(=>
(and
(domain ?FUNCTION 1 ?CLASS)
(instance ?INST1 ?CLASS)
(instance ?INST2 ?CLASS))
(equal
(AssignmentFn ?FUNCTION ?INST1 ?INST2)
(AssignmentFn ?FUNCTION ?INST2 ?INST1))))) |
Merge.kif 3551-3561 |
If X is an instance of commutative function, then For all Entities Y and Z and Class W: if the number 1 argument of X is an instance of W, Y is an instance of W, and Z is an instance of W, then equal X(Y and Z) and X(Z and Y) |
(=>
(and
(instance ?RELATION ReflexiveRelation)
(reflexiveOn ?RELATION ?CLASS)
(instance ?RELATION Predicate))
(forall (?INST)
(=>
(instance ?INST ?CLASS)
(?RELATION ?INST ?INST)))) |
Merge.kif 3721-3729 |
If X is an instance of reflexive relation, X is reflexive on Y, and X is an instance of predicate, then For all Entity Z: if Z is an instance of Y, then X Z and Z |
| | Display limited to 25 items. Show next 25 |
| | Display limited to 25 items. Show next 25 |
|
statement
|
|
|
|
