| TransitiveRelation(transitive relation) |
| appearance as argument number 1 |
|
|
| (subclass TransitiveRelation BinaryRelation) | Merge.kif 2368-2368 | Transitive relation is a subclass of binary relation |
| (disjoint TransitiveRelation IntransitiveRelation) | Merge.kif 2369-2369 | Transitive relation is disjoint from intransitive relation |
| (documentation TransitiveRelation EnglishLanguage "A BinaryRelation ?REL is transitive if (?REL ?INST1 ?INST2) and (?REL ?INST2 ?INST3) imply (?REL ?INST1 ?INST3), for all ?INST1, ?INST2, and ?INST3.") | Merge.kif 2371-2373 | Transitive relation is disjoint from intransitive relation |
| appearance as argument number 2 |
|
|
| antecedent |
|
|
| (=> (instance ?REL TransitiveRelation) (forall (?INST1 ?INST2 ?INST3) (=> (and (?REL ?INST1 ?INST2) (?REL ?INST2 ?INST3)) (?REL ?INST1 ?INST3)))) |
Merge.kif 2375-2382 | 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 |
| consequent |
|
|
| (=> (partialOrderingOn ?RELATION ?CLASS) (and (reflexiveOn ?RELATION ?CLASS) (instance ?RELATION TransitiveRelation) (instance ?RELATION AntisymmetricRelation))) |
Merge.kif 3689-3694 | If X is partial ordering on Y, then X is reflexive on Y, X is an instance of transitive relation, and X is an instance of antisymmetric relation |
| (=> (equivalenceRelationOn ?RELATION ?CLASS) (and (instance ?RELATION TransitiveRelation) (instance ?RELATION SymmetricRelation) (reflexiveOn ?RELATION ?CLASS))) |
Merge.kif 3752-3757 | If X is an equivalence relation on Y, then X is an instance of transitive relation, X is an instance of symmetric relation, and X is reflexive on Y |
|
|