Relation DISJOINT

• Defined in theory: Kif-sets
• Source code: kif-sets.lisp

Slots on this relation:

Documentation:

Two sets are disjoint if and only if there is no object that is a member of both sets.

Instance-Of: Relation

Arity: 2

Equivalence Axioms:

(<=> (Disjoint ?S1 ?S2) (Empty (Intersection ?S1 ?S2)))

Other Related Axioms:

(<=> (Disjoint ?S1 ?S2) (Empty (Intersection ?S1 ?S2)))

(Forall (?S1 ?S2)
        (=> (Item ?S1 (Listof @Sets))
            (Item ?S2 (Listof @Sets))
            (Or (= ?S1 ?S2) (Disjoint ?S1 ?S2))))

(<=> (Pairwise-Disjoint @Sets)
     (Forall (?S1 ?S2)
             (=> (Item ?S1 (Listof @Sets))
                 (Item ?S2 (Listof @Sets))
                 (Or (= ?S1 ?S2) (Disjoint ?S1 ?S2)))))

(Forall (?S)
        (=> (Not (Empty ?S))
            (Exists (?U) (And (Member ?U ?S) (Disjoint ?U ?S)))))

Notes:

• Source: KIF Version 3.0 Specification