|
|
   TransitiveRelation
|
|
|
| appearance as argument number 1 |
|
|
| (disjoint TransitiveRelation IntransitiveRelation) | Merge.kif 2334-2334 | RelazioneTransitiva è disgiunto da RelazioneIntransitiva |
| (documentation TransitiveRelation ChineseLanguage "一个 BinaryRelation ?REL 是传递关系 如果所有的 ?INST1， ?INST2和 ?INST3 是(?REL ?INST1 ?INST2) 和 (?REL ?INST2 ?INST3) 意味着 (?REL ?INST1 ?INST3)。") | chinese_format.kif 1848-1850 | |
| (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 | |
| (documentation TransitiveRelation JapaneseLanguage "BinaryRelation ?REL は、すべての ?INST1, ?INST2, および ?INST3 に対して (?REL ?INST1 ?INST2) および (?REL ?INST2 ?INST3) が (?REL ?INST1 ?INST3) を意味する場合、推移的である。") | japanese_format.kif 469-471 | |
| (subclass TransitiveRelation BinaryRelation) | Merge.kif 2333-2333 | RelazioneTransitiva è una sottoclasse di RelazioneBinaria |
| 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 3713-3718 |
|
| (=> (partialOrderingOn ?RELATION ?CLASS) (and (reflexiveOn ?RELATION ?CLASS) (instance ?RELATION TransitiveRelation) (instance ?RELATION AntisymmetricRelation))) |
Merge.kif 3650-3655 |
|
|
|
|