| AntisymmetricRelation(antisymmetric relation) |
| appearance as argument number 1 |
|
|
| (subclass AntisymmetricRelation BinaryRelation) | Merge.kif 2327-2327 | Antisymmetric relation is a subclass of binary relation |
| (documentation AntisymmetricRelation EnglishLanguage "BinaryRelation ?REL is an AntisymmetricRelation if for distinct ?INST1 and ?INST2, (?REL ?INST1 ?INST2) implies not (?REL ?INST2 ?INST1). In other words, for all ?INST1 and ?INST2, (?REL ?INST1 ?INST2) and (?REL ?INST2 ?INST1) imply that ?INST1 and ?INST2 are identical. Note that it is possible for an AntisymmetricRelation to be a ReflexiveRelation.") | Merge.kif 2329-2334 | Antisymmetric relation is a subclass of binary relation |
| appearance as argument number 2 |
|
|
| antecedent |
|
|
| (=> (and (instance ?REL AntisymmetricRelation) (instance ?REL IrreflexiveRelation)) (instance ?REL AsymmetricRelation)) |
Merge.kif 2321-2325 | If X is an instance of antisymmetric relation and X is an instance of irreflexive relation, then X is an instance of asymmetric relation |
| (=> (instance ?REL AntisymmetricRelation) (forall (?INST1 ?INST2) (=> (and (?REL ?INST1 ?INST2) (?REL ?INST2 ?INST1)) (equal ?INST1 ?INST2)))) |
Merge.kif 2336-2343 | If X is an instance of antisymmetric relation, then For all Entities Y and Z: if X Y and Z and X Z and Y, then equal Y and Z |
| consequent |
|
|
| (=> (instance ?REL AsymmetricRelation) (and (instance ?REL AntisymmetricRelation) (instance ?REL IrreflexiveRelation))) |
Merge.kif 2315-2319 | If X is an instance of asymmetric relation, then X is an instance of antisymmetric relation and X is an instance of irreflexive relation |
| (=> (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 |
|
|