%%  %prefix( :      <http://www.example.org/mereology#>
%%          owl:   <http://www.w3.org/2002/07/owl#>
%%          log:   <http://purl.net/dol/@logic@/>    %% descriptions of logics ...
%%          trans: <http://purl.net/dol/translations/> )%  %% ... and translations

distributed-ontology Mereology

logic Propositional
%% logic log:Propositional syntax ser:Prop/Hets       %% non-standard serialization built into Hets
ontology Taxonomy = %mcons      %% basic taxonomic information about mereology reused from DOLCE
  props PT, T, S, AR, PD
  . S \/ T \/ AR \/ PD => PT                                                    %% PT is the top concept
  . S /\  T  => false                                               %% PD, S, T, AR are pairwise disjoint
  . T /\ AR => false                                                                         %% and so on
end

logic OWL
%% language lang:OWL2 logic log:SROIQ syntax ser:OWL2/Manchester           %% OWL Manchester syntax
ontology BasicParthood =                             %% Parthood in SROIQ, as far as easily expressible
  Class: Particular
  Class: ParticularCategory SubClassOf: Particular
  Class: SpaceRegion
  Class: TimeInterval
  Class: AbstractRegion
  Class: Perdurant
    DisjointUnionOf: SpaceRegion, TimeInterval, AbstractRegion, Perdurant
                                 %% pairwise disjointness more compact thanks to an OWL built-in
  ObjectProperty: isPartOf        Characteristics: Transitive
  ObjectProperty: isProperPartOf  Characteristics: Asymmetric  SubPropertyOf: isPartOf 
  Class: Atom EquivalentTo: inverse isProperPartOf only owl:Nothing
end                                          %% an atom has no proper parts

%[
interpretation TaxonomyToParthood : Taxonomy to BasicParthood =
  PT |-> Particular, S |-> SpaceRegion, T |-> TimeInterval, A |-> AbstractRegion %[ and so on ]%
%%  logic Propositional2OWL2 %% translation trans:PropositionalToSROIQ    %% translate the logic, then rename the entities
end


logic CommonLogic
%% logic log:CommonLogic syntax ser:CommonLogic/CLIF
                      %% syntax: the Lisp-like CLIF dialect of Common Logic
ontology ClassicalExtensionalParthood =
  BasicParthood with OWL2CommonLogic  %% translation trans:SROIQtoCL
then
      %% import the OWL ontology from above, translate it to Common Logic, then extend it there:
  . (forall (X) (if (or (= X S) (= X T) (= X AR) (= X PD))
                    (forall (x y z) (if (and (X x) (X y) (X z))
                                        (and                          
      (if (and (isPartOf x y) (isPartOf y x)) (= x y))                           
      (if (and (isProperPartOf x y) (isProperPartOf y z)) (isProperPartOf x z))

      (iff (overlaps x y) (exists (pt) (and (isPartOf pt x) (isPartOf pt y))))
      (iff (isAtomicPartOf x y) (and (isPartOf x y) (Atom x)))
      (iff (sum z x y)
           (forall (w) (iff (overlaps w z) (and (overlaps w x) (overlaps w y)))))
      (exists (s) (sum s x y))                                           
      )))))
  . (forall (Set a) (iff (fusion Set a)                                  
            (forall (b) (iff (overlaps b a)
                             (exists (c) (and (Set c) (overlaps c a)))))))
end
]%