Relation TRANSITIVE

• Defined in theory: Abstract-algebra
• Source code: abstract-algebra.lisp

Slots on this relation:

Instance-Of: Relation

Arity: 2

Domain: Binary-relation

Equivalence Axioms:

(<=> (Transitive ?Rel ?Domain)
     (And (Binary-Relation ?Rel)
          (Forall (?X ?Y ?Z)
                  (=> (And (Instance-Of ?X ?Domain)
                           (Instance-Of ?Y ?Domain)
                           (Instance-Of ?Z ?Domain)
                           (Holds ?Rel ?X ?Y)
                           (Holds ?Rel ?Y ?Z))
                      (Holds ?Rel ?X ?Z)))))

Other Related Axioms:

(=> (Transitive $X $Y) (Binary-Relation $X))

(<=> (Transitive ?Rel ?Domain)
     (And (Binary-Relation ?Rel)
          (Forall (?X ?Y ?Z)
                  (=> (And (Instance-Of ?X ?Domain)
                           (Instance-Of ?Y ?Domain)
                           (Instance-Of ?Z ?Domain)
                           (Holds ?Rel ?X ?Y)
                           (Holds ?Rel ?Y ?Z))
                      (Holds ?Rel ?X ?Z)))))

(<=> (Partial-Order ?Domain ?Rel)
     (And (Irreflexive ?Rel ?Domain)
          (Asymmetric ?Rel ?Domain)
          (Transitive ?Rel ?Domain)))

(<=> (Linear-Order ?Domain ?Rel)
     (And (Irreflexive ?Rel ?Domain)
          (Asymmetric ?Rel ?Domain)
          (Transitive ?Rel ?Domain)
          (Trichotomizes ?Rel ?Domain)))