|
|
   TransitiveRelation
|
|
|
| appearance as argument number 1 |
|
|
| (disjoint TransitiveRelation IntransitiveRelation) | Merge.kif 2345-2345 | 传递关系 和 % 2 是 disjoint |
| (documentation TransitiveRelation ChineseLanguage "一个 BinaryRelation ?REL 是传递关系 如果所有的 ?INST1， ?INST2和 ?INST3 是(?REL ?INST1 ?INST2) 和 (?REL ?INST2 ?INST3) 意味着 (?REL ?INST1 ?INST3)。") | chinese_format.kif 1848-1850 | 传递关系 和 % 2 是 disjoint |
| (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 2347-2349 | 传递关系 和 % 2 是 disjoint |
| (documentation TransitiveRelation JapaneseLanguage "BinaryRelation ?REL は、すべての ?INST1, ?INST2, および ?INST3 に対して (?REL ?INST1 ?INST2) および (?REL ?INST2 ?INST3) が (?REL ?INST1 ?INST3) を意味する場合、推移的である。") | japanese_format.kif 469-471 | 传递关系 和 % 2 是 disjoint |
| (subclass TransitiveRelation BinaryRelation) | Merge.kif 2344-2344 | 传递关系 是 二元关系 的 subclass |
| 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 2351-2358 |
| consequent |
|
|
| (=> (equivalenceRelationOn ?RELATION ?CLASS) (and (instance ?RELATION TransitiveRelation) (instance ?RELATION SymmetricRelation) (reflexiveOn ?RELATION ?CLASS))) |
Merge.kif 3728-3733 | |
| (=> (partialOrderingOn ?RELATION ?CLASS) (and (reflexiveOn ?RELATION ?CLASS) (instance ?RELATION TransitiveRelation) (instance ?RELATION AntisymmetricRelation))) |
Merge.kif 3665-3670 |
|
|
|