library Ontology/Dolce/DolceSimpl_Dummy

%%------------------------
%% Taxonomy
%%------------------------

spec Taxonomy =  
     sorts s
end


%%------------------------
%% Partial_Order (po)
%%------------------------

spec Partial_Order =
     sorts s
end

%%---------------------------
%% Strict_Partial_Order (spo)
%%---------------------------

%[
spec Strict_Partial_Order =

esort s
pred Rel: s * s
forall x,y,z: s
. Rel(x,y) => not Rel(y,x) 
. Rel(x,y) /\ Rel(y,z) => Rel(x,z) %(transitivity)%
end
]%
%%-----------------------------------
%% Classical_Extensional_Parhood (p)
%%----------------------------------

spec Classical_Extensional_Parthood =
     Partial_Order
end


%%---------------
%% Time_Mereology
%%---------------
%% Time_Mereology is needed in oder to specify the properties of perdurants

spec Time_Mereology =
     Classical_Extensional_Parthood
end

%%-------------------
%% Being_Present
%%-------------------

spec Being_Present =
     Time_Mereology
end


%%-----------
%% Mereology
%%-----------

spec Mereology =
     Time_Mereology
and  Classical_Extensional_Parthood
and  Classical_Extensional_Parthood
and  Classical_Extensional_Parthood
end

%%----------------------------
%% Mereology_and_TemporalPart
%%----------------------------

spec Mereology_and_TemporalPart =
     Mereology
and  Being_Present
end

%%---------------------
%% Binary_Present (bpre)
%%---------------------

spec Binary_Present =
     Being_Present
and
     Being_Present
end 


%%---------------------------------
%% Binary_Temporal_Dissective (btd)
%%---------------------------------

spec Binary_Temporal_Dissective = 
     Time_Mereology
end

%%-------------------------------------
%% Temporary_Strict_Partial_Order (tspo)
%%-------------------------------------

spec Temporary_Strict_Partial_Order =
     sorts s
end 


%%-----------------------
%% Temporary_Parthood (tp)
%%-----------------------

spec Temporary_Parthood =
     Being_Present
and  Binary_Temporal_Dissective
and  Binary_Present
end  


%%---------------------
%% Temporary_Mereology
%%---------------------

spec Temporary_Mereology =
     Temporary_Parthood
and  Temporary_Parthood
end


%%-----------------------
%% Constitution_Spec (k)
%%----------------------

spec Constitution_Spec =
     Binary_Temporal_Dissective
and  Binary_Present
and  Temporary_Strict_Partial_Order
and  Temporary_Parthood 
end

%%--------------
%% Constitution
%%--------------

spec Constitution =
     Constitution_Spec
and  Constitution_Spec
and  Constitution_Spec
and  Constitution_Spec
and  Constitution_Spec
and  Constitution_Spec
end


%%----------------
%% Participation
%%----------------

spec Participation =
     Binary_Temporal_Dissective
and  Binary_Present
end     

%%----------------
%% Direct_Quality
%%----------------

spec Direct_Quality =
     sorts s
end

%%-----------------
%% Immediate_Quale
%%-----------------

spec Immediate_Quale =
     sorts s
end 


%%-------------------
%% Temporary_Quale
%%-------------------

spec Temporary_Quale =
     Being_Present
and  Being_Present
and  Being_Present
end

%%------------
%% Dependence
%%------------

spec Dependence =
     Being_Present
and  Being_Present
and  Being_Present
and  Being_Present
and  Being_Present
and  Being_Present
and  Being_Present
end 

%%-------
%% Dolce
%%-------

spec PreDolce =
     Mereology_and_TemporalPart
and  Temporary_Mereology
and  Participation
and  Constitution
and  Dependence
and  Direct_Quality
and  Temporary_Quale
and  Immediate_Quale
end

spec Dolce =
     PreDolce
and
     Taxonomy
end