antisymmetric relation (AntisymmetricRelation)

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.

Ontology

SUMO / BASE-ONTOLOGY

Superclass(es)

entity

abstract

relation

binary relation

antisymmetric relation

Subclass(es)

asymmetric relation partial ordering relation

Coordinate term(s)

binary predicate intransitive relation irreflexive relation reflexive relation symmetric relation transitive relation trichotomizing relation unary function

Axioms (2)

if rel is an instance of antisymmetric relation,
then for all inst1,inst2 holds: if rel(inst1,inst2) holds and rel(inst2,inst1) holds, then inst1 is equal to inst2

(=>
      (instance ?REL AntisymmetricRelation)
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (holds ?REL ?INST1 ?INST2)
                        (holds ?REL ?INST2 ?INST1))
                  (equal ?INST1 ?INST2))))

If relation is partial ordering on class, then relation is reflexive on class and relation is an instance of transitive relation and relation is an instance of antisymmetric relation.

(=>
      (partialOrderingOn ?RELATION ?CLASS)
      (and
            (reflexiveOn ?RELATION ?CLASS)
            (instance ?RELATION TransitiveRelation)
            (instance ?RELATION AntisymmetricRelation)))