TransitiveRelation(transitive relation) |
appearance as argument number 1 |
(disjoint TransitiveRelation IntransitiveRelation) | Merge.kif 2334-2334 | 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 2336-2338 | 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 2333-2333 | 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 2340-2347 |
|
consequent |
(=> (equivalenceRelationOn ?RELATION ?CLASS) (and (instance ?RELATION TransitiveRelation) (instance ?RELATION SymmetricRelation) (reflexiveOn ?RELATION ?CLASS))) |
Merge.kif 3714-3719 |
|
(=> (partialOrderingOn ?RELATION ?CLASS) (and (reflexiveOn ?RELATION ?CLASS) (instance ?RELATION TransitiveRelation) (instance ?RELATION AntisymmetricRelation))) |
Merge.kif 3651-3656 |
|