Relation PAIRWISE-DISJOINT

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

Slots on this relation:

Documentation:

Sets are pairwise-disjoint if and only if every set is disjoint from every other set.

Instance-Of: Relation

Equivalence Axioms:

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

Axioms:

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

(Undefined (Arity Pairwise-Disjoint))

Other Related Axioms:

(Instance-Of (Arity Pairwise-Disjoint) Undefined)

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

(<=> (Set-Partition ?S @Sets)
     (And (= ?S (Union @Sets)) (Pairwise-Disjoint @Sets)))

Notes:

• Source: KIF Version 3.0 Specification