(define-theory Mereology (Structuring-Concepts))
(in-theory 'Mereology)


(DEFINE-RELATION COMMON-PART (?A ?B) :IFF-DEF
 (AND (MEREOLOGICAL-RELATION ?A ?B)
      (EXISTS (?C) (AND (PART ?A ?C) (PART-OF ?C ?B)))))
(DEFINE-RELATION PART-OVERLAPS (?A ?B) :IFF-DEF (COMMON-PART ?A ?B))
(DEFINE-RELATION MEREO-DISJOINT (?A ?B)
 "This is Tarski's definition for disjointness; 
this is actually the converse of common-part-with: 
   disjoint(x,y) <=> not(common-part-with(x,y)).
Leonard-Goodman prefer disjoint as primitive and they define part from it.
Consider that there exist distributed wholes having non-connected parts 
-societies with members, collections, etc.-
but this is not to say that this definition of disjoint does not hold;
in fact, distributed wholes are characterized by some particular meronymic
notion of part (see theory:'meronymy')."
 :IFF-DEF (AND (NOT (COMMON-PART ?A ?B)) (MEREOLOGICAL-RELATION ?A ?B)))
(DEFINE-FUNCTION MEREO-SUM (?A ?B) :-> ?C :DEF
 (AND (PROPER-PART-OF ?A ?C)
      (PROPER-PART-OF ?B ?C)
      (STRUCTURING-TERNARY ?A ?B ?C))
 :AXIOM-DEF (AND (FUNCTION MEREO-SUM) (ARITY MEREO-SUM 3)))
(DEFINE-RELATION MEREO-UNION (?A ?B))
(DEFINE-RELATION PART (?A ?B) :IFF-DEF
 (AND (= (INVERSE PART-OF) PART) (ENTITY ?A) (ENTITY ?B))
 :CONSTRAINTS (AND (ENTITY ?A) (ENTITY ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE PART ENTITY)
      (DOMAIN PART ENTITY)))
(DEFINE-RELATION PART-OF (?A ?B)
 "Many doubts have been cast on the transitivity 
of part; though, it seems that these doubts are based on 'local' problems, due 
to the various identity criteria an individual may assume. On the other hand,
transitivity is not inherited from part to regional parts (see theory 'meronymy').
   In general, regional part notions should be used; but when the axiom is 
sufficiently general, or when arguments lie in heterogeneous concepts, or
when are regions, 'part' must be used. As far as regions are concerned, one
could wonder which is the difference between located and part between regions.
Thus, figure it out a geographic area A1 which is part of another area A2 without
A1 being located at A2, for example so-called 'enclaves'."
 :DEF
 (AND (=> (AND (PART-OF ?A ?B) (PART-OF ?B ?A)) (IDENTITY ?A ?B))
      (MEREOLOGICAL-RELATION ?A ?B)))
(DEFINE-RELATION PROPER-PART (?A ?B) :IFF-DEF
 (= (INVERSE PROPER-PART-OF) PROPER-PART))
(DEFINE-RELATION PROPER-PART-OF (?A ?B) :DEF
 (AND (PART-OF ?A ?B) (NOT (PART-OF ?B ?A)) (MEREOLOGICAL-RELATION ?A ?B)))
(DEFINE-FUNCTION REMAINDER (?A ?B) :-> ?C :DEF
 (AND (PROPER-PART-OF ?A ?B)
      (PROPER-PART-OF ?C ?B)
      (DIFFERENT ?C ?A)
      (NOT (EXISTS ?W
            (AND (PROPER-PART-OF ?W ?B)
                 (OR (DIFFERENT ?W ?A) (DIFFERENT ?W ?C)))))
      (STRUCTURING-TERNARY ?A ?B ?C))
 :AXIOM-DEF (AND (FUNCTION REMAINDER) (ARITY REMAINDER 3)))
(DEFINE-RELATION _ATOM (?A ?B) :DEF
 (AND (NOT (EXISTS ?Y (PROPER-PART ?Y ?A))) (MEREOLOGICAL-PROPERTY ?A ?B)))
(DEFINE-RELATION _CONTINUOUS (?A ?B)
 "An aggregate is continuous if it has only smaller 
parts which are continuous as well; in other words, no proper parts are atoms."
 :DEF
 (AND (NOT (EXISTS ?Y (AND (_ATOM ?Y TRUE) (PROPER-PART-OF ?Y ?A))))
      (MEREOLOGICAL-PROPERTY ?A ?B)))
(DEFINE-RELATION _DISCRETE (?A ?B)
 "An aggregate is discrete if it has at least one 
atom as part."
 :DEF
 (AND (EXISTS ?Y (AND (_ATOM ?Y TRUE) (PART-OF ?Y ?A)))
      (MEREOLOGICAL-PROPERTY ?A ?B)))
(DEFINE-RELATION _LUMPY (?A ?B)
 "An aggregate is lumpy when some parts are atoms, 
and some parts are continuous aggregates, ie, x has some part y, all of whose parts z
have at least one proper part w."
 :IFF-DEF
 (AND (EXISTS ?X (AND (_ATOM ?X TRUE) (PART-OF ?X ?A)))
      (EXISTS ?Y
       (AND (PART-OF ?Y ?A)
            (FORALL ?Z
             (=> (PART-OF ?B ?Y) (EXISTS ?W (PROPER-PART-OF ?W ?B))))))
      (MEREOLOGICAL-PROPERTY ?A ?B)))