| TransitiveRelation(transitive relation) |
| appearance as argument number 1 |
|
|
| (disjoint TransitiveRelation IntransitiveRelation) | Merge.kif 2370-2370 | Transitive relation is disjoint from intransitive relation |
| (documentation TransitiveRelation ChineseLanguage "一个 BinaryRelation ?REL 是传递关系 如果所有的 ?INST1, ?INST2和 ?INST3 是(?REL ?INST1 ?INST2) 和 (?REL ?INST2 ?INST3) 意味着 (?REL ?INST1 ?INST3)。") | chinese_format.kif 1848-1850 | 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 2372-2374 | Transitive relation is disjoint from intransitive relation |
| (documentation TransitiveRelation JapaneseLanguage "BinaryRelation ?REL は、すべての ?INST1, ?INST2, および ?INST3 に対して (?REL ?INST1 ?INST2) および (?REL ?INST2 ?INST3) が (?REL ?INST1 ?INST3) を意味する場合、推移的である。") | japanese_format.kif 469-471 | Transitive relation is disjoint from intransitive relation |
| (subclass TransitiveRelation BinaryRelation) | Merge.kif 2369-2369 | Transitive relation is a subclass of binary 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 2376-2383 |
|
| consequent |
|
|
| (=> (equivalenceRelationOn ?RELATION ?CLASS) (and (instance ?RELATION TransitiveRelation) (instance ?RELATION SymmetricRelation) (reflexiveOn ?RELATION ?CLASS))) |
Merge.kif 3753-3758 |
|
| (=> (partialOrderingOn ?RELATION ?CLASS) (and (reflexiveOn ?RELATION ?CLASS) (instance ?RELATION TransitiveRelation) (instance ?RELATION AntisymmetricRelation))) |
Merge.kif 3690-3695 |
|
|
|