Dolce in FCG
Philippe Martin - August 2004
This file shows a translation of the KIF source of
Dolce
(D18) in the
FCG notation.
However, the syntax still need to be refined (and WebKB-2 fully upgraded to handle
the new syntactic features) before this file can be loaded in the KB of WebKB-2.
This is expected to be done in October 2004.
In order to integrate the categories of Dolce into the
multi-source ontology (MSO) of WebKB-2, these categories are prefixed by "dolce#"
(the first two commands permit this prefix to be implicit).
no storage; no "already the case" warning; //while this file is being debugged
default creator: dolce;
unprefixed identifiers allowed;
//REVIEW INFO
//CHANGES - COMMENTS
//(D13) changed WORD into WORLD - Typo
//(NA3)-(NA9) have been dropped - These occur already somewhere else
//(NA10)-(NA12) are left as comments - These are guaranteed by def. (ND5)
//(NA13) has been dropped - It follows from (NA14) and (D2)
// Basic functions and relations
// new non-rigid universals introduced in specialized
// theories or in new versions of DOLCE need to be added in
// this definition as new disjunction clauses of form (= ?f =8A)
// (ND1): universals
//(defrelation UNIVERSAL (?f) := (or (X ?f)))
universal__UNIVERSAL > rigid_universal; //'>' means "has for proper subtype"
// new rigid universals introduced in new versions of DOLCE
// (or by the user) need to be added in this definition
// (ND2) rigid universals
//(defrelation X (?f) :=
// (or (= ?f entity) (= ?f abstract)
// (= ?f region) (= ?f temporal_region) (= ?f time_interval)
// (= ?f physical_region) (= ?f space_region) (= ?f abstract_region)
// (= ?f quality) (= ?f temporal_quality) (= ?f temporal_location)
// (= ?f physical_quality) (= ?f spatial_location) (= ?f abstract_quality)
// (= ?f endurant) (= ?f amount_of_matter) (= ?f physical_endurant)
// (= ?f feature) (= ?f physical_object) (= ?f agentive_physical_object)
// (= ?f non-agentive_physical_object) (= ?f non-physical_endurant)
// (= ?f non-physical_object) (= ?f mental_object) (= ?f social_object)
// (= ?f agentive_social_object) (= ?f social_agent) (= ?f society)
// (= ?f non-agentive_social_object) (= ?f arbitrary_sum)
// (= ?f perdurant) (= ?f event) (= ?f achievement) (= ?f accomplishment)
// (= ?f stative) (= ?f state) (= ?f process))))
rigid_universal__X //':' means "has for instance"
: entity abstract region temporal_region time_interval
physical_region space_region abstract_region
quality temporal_quality temporal_location physical_quality spatial_location
abstract_quality endurant amount_of_matter physical_endurant feature
physical_object agentive_physical_object non-agentive_physical_object
non-physical_endurant non-physical_object mental_object social_object
agentive_social_object social_agent society non-agentive_social_object
arbitrary_sum perdurant event achievement accomplishment
stative state process ;
// there are no particulars in this version of DOLCE, any
// particular has to be added in this definition, the def.
// will have form : (or (= ?x =8A) (= ?x =8A))
// (ND3) particulars
//(defrelation PARTICULAR(?x) := )
particular__PARTICULAR < pm#individual;
// there are no named worlds in this version of DOLCE, any
// world has to be added in this definition, the def. Will
// have form : (or (= ?w =8A) (= ?w =8A))
// (ND4) worlds
//(defrelation WORLD(?w) := )
world__WORLD < pm#thing;
// (ND5) accessibility relation on worlds
//(defrelation WLDR(?w ?v) := (and (WORLD ?w) (WORLD ?v)))
wldr__WLDR (world, world);
//pm: new def. ND6 - ND12: Table 3 D18p20 *************************************
// (ND6) Parthood
//(defrelation P (?w ?x ?y) :=> (and (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y)))
part__P (world, particular, particular);
//A1: [part(world ?w0,particular ?x,particular ?y) =>
// AND{ OR{abstract(?w0,?x), perdurant(?w0,?x)},
// OR{abstract(?w0,?y), perdurant(?w0,?y)}];
//A2: [part(world ?w0,particular ?x,particular ?y) =>
// [perdurant(?w0,?x) <=> perdurant(?w0,?y)];
//A3: [part(world ?w0,particular ?x,particular ?y) =>
// [abstract(?w0,?x) <=> abstract(?w0,?y)];
// (ND7) Temporal Parthood //pm: Temporary Parthood, not Temporal Parthood (D54)
//(defrelation P (?w ?x ?y ?t) :=>
// (and (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)))
temporary_part__P (world, particular, particular, particular);
//A10: [temporary_part(world ?w0,particular ?x,particular ?y,particular ?t) =>
// AND{endurant(?w0,?x), endurant(?w0,?y), time_interval(?w0,?t)}];
//A11: [temporary_part(world ?w0,particular ?x,particular ?y,particular ?t) =>
// AND{physical_endurant(?w0,?x), physical_endurant(?w0,?y)}];
//A12: [temporary_part(world ?w0,particular ?x,particular ?y,particular ?t) =>
// AND{non-physical_endurant(?w0,?x), non-physical_endurant(?w0,?y)}];
// (ND8) Constitution
//(defrelation K (?w ?x ?y ?t) :=>
// (and (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)))
constitution__K (world, particular, particular, particular);
//A20: [constitution(world ?w0,particular ?x,particular ?y,particular ?t)
// => AND{ OR{endurant(?w0,?x), perdurant(?w0,?x)},
// OR{endurant(?w0,?y), perdurant(?w0,?y)}, time_interval(?w0,?t)}];
//A21: [constitution(world ?w0,particular ?x,particular ?y,particular ?t)
// => [physical_endurant(?w0,?x) <=> physical_endurant(?w0,?y)] ];
//A22: [constitution(world ?w0,particular ?x,particular ?y,particular ?t)
// => [non-physical_endurant(?w0,?x) <=> non-physical_endurant(?w0,?y)] ];
//A23: [constitution(world ?w0,particular ?x,particular ?y,particular ?t)
// => [perdurant(?w0,?x) <=> perdurant(?w0,?y)] ];
// (ND9) Participation
//(defrelation PC (?w ?x ?y ?t) :=>
// (and (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)))
participant__PC (world, particular, particular, particular);
//A33: [participant(world ?w0,particular ?x,particular ?y,particular ?t)
// => AND{endurant(?w0,?x), perdurant(?w0,?y), time_interval(?w0,?t)}];
// (ND10) Quality
//(defrelation qt (?w ?x ?y) :=> (and (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y)))
qt__quality (world, particular, particular);
//a38:[qt(world ?w0,particular ?x,particular ?y) =>
// AND{quality(?w0,?x), OR{quality(?w0,?y),endurant(?w0,?y),perdurant(?w0,?y)}}];
//a39:[qt(world ?w0,particular ?x,particular ?y) =>
// [temporal_quality(?w0,?x) <=> OR{temporal_quality(?w0,?y),perdurant(?w0,?y)}]];
//a40:[qt(world ?w0,particular ?x,particular ?y)
// => [physical_quality(?w0,?x) <=>
// OR{physical_quality(?w0,?y),physical_endurant(?w0,?y)}] ];
//a41:[qt(world ?w0,particular ?x,particular ?y)
// => [abstract_quality(?w0,?x) <=>
// OR{abstract_quality(?w0,?y),non-physical_endurant(?w0,?y)}] ];
// (ND11) Quale
//(defrelation ql (?w ?x ?y) :=> (and (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y)))
ql__quale (world, particular, particular);
//a51: [ql(world ?w0,particular ?x,particular ?y)
// => AND{temporal_region(?w0,?x), temporal_quality(?w0,?y)}];
// (ND12) Quale (temporal)
//(defrelation ql (?w ?x ?y ?t) :=>
// (and (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)))
temporary_quale__ql (world, particular, particular, particular);
//A58: [temporary_quale(world ?w0,particular ?x,particular ?y,particular ?t)
// => AND{ OR{physical_region(?w0,?x), abstract_region(?w0,?x)},
// OR{physical_quality(?w0,?y), abstract_quality(?w0,?y)},
// time_interval(?w0,?t)}];
//A59: [temporary_quale(world ?w0,particular ?x,particular ?y,particular ?t)
// => AND{physical_region(?w0,?x), physical_quality(?w0,?y)}];
//A60: [temporary_quale(world ?w0,particular ?x,particular ?y,particular ?t)
// => AND{abstract_region(?w0,?x), abstract_quality(?w0,?y)}];
//*****************************************************
// (NA1) NEW AXIOM: total domain
//(forall (?x) (or (PARTICULAR ?x) (UNIVERSAL ?x) (WORLD ?x)))
// (NA2) partition of the domain
//(forall (?x) (and (<=> (PARTICULAR ?x) (and (not (UNIVERSAL ?x)) (not (WORLD ?x))))
// (<=> (UNIVERSAL ?x) (and (not (PARTICULAR ?x)) (not (WORLD ?x))))
// (<=> (WORLD ?x) (and (not (PARTICULAR ?x)) (not (UNIVERSAL ?x))))))
/* already in default ontology:
pm#thing > {(particular universal world)}; //complete subtype partition
*/
// Formal Characterization
//PRINCIPLES USED IN THE TRANSLATION IN KIF:
//Modal operators of possibility and necessity are translated in the standard
// way, see for instance p516 of Handbook of Logic in AI and Logic Prog. Vol4
//The indeces of relations are included prefixing a dot (we preserve the capital or
// lower case distinction)
//These are the only predicates (with their arity) that do not have possible worlds
// as arguments: X_1,PARTICULAR_1,UNIVERSAL_1, =_2
//No need for Barcan formulas, the domain of particulars turns out to be unique
// in the translation
//WLDR is an equivalence relation (from correspondence theory, this implies
// that WLDR is a relation for S5). The axioms (NA10)-(NA12) are not necessary
// because of our definition of WLDR.
// (NA10)
//(forall (?w0) (=> (WORLD ?w0) (WLDR ?w0 ?w0)))
// (NA11)
//(forall (?w0 ?w1)
// (=> (and (WLDR ?w0 ?w1) (WORLD ?w0) (WORLD ?w1)) (WLDR ?w1 ?w0)))
// (NA12)
//(forall (?w0 ?w1 ?w2)
// (=> (and (WLDR ?w0 ?w1) (WLDR ?w1 ?w2) (WORLD ?w0) (WORLD ?w1) (WORLD ?w2))
// (WLDR ?w0 ?w2)))
// ***THE UNIVERSALS ARE NECESSARILY NON-EMPY***-- axiom
// (NA14) -- axiom
//(forall (?w ?f) (=> (and (UNIVERSAL ?f) (WORLD ?w)) (NEP ?w ?f)))
[non-empty_universal(world ?w,universal ?f)];
exit;
// (NA15) -- axiom
//(forall (?w ?f) (=> (and (UNIVERSAL ?f) (WORLD ?w)) (or (not (X ?f)) (RG ?w ?f))))
[ [universal ?f rigid_universal] => rigid(world ?w,?f)];
//explanation: 1) "universal ?f" declares ?f as a universally quantified variable of type
// universal (the scope/context where ?f is declared is the minimal one
// covering all the occurrences of ?f in the formula);
// 2) "?f rigid_universal" is a use of ?f with the additional constraint
// that it must also be of type rigid_universal (the scope/context is the
// local one; syntactically, the additional type must follow the variable;
// a declared variable cannot be re-declared within the same formula).
// (NA16) Instances of PT -- axiom
//(forall (?w0) (=> (WORLD ?w0) (and (PT ?w0 ALL ED PD Q AB) (PT ?w0 ED PED NPED AS)
// (PT ?w0 PED M F POB) (PT ?w0 POB APO NAPO)
// (PT ?w0 NPOB MOB SOB) (PT ?w0 SOB ASO NASO)
// (PT ?w0 ASO SAG SC) (PT ?w0 PD EV STV)
// (PT ?w0 EV ACH ACC) (PT ?w0 STV ST PRO)
// (PT ?w0 Q TQ PQ AQ) (PT ?w0 R TR PR AR))))
[[world ?w0] =>
AND{partition(?w0,entity,endurant,perdurant,quality,abstract),
partition(?w0,endurant,physical_endurant,non-physical_endurant,arbitrary_sum),
partition(?w0,physical_endurant,amount_of_matter,feature,physical_object),
partition(?w0,physical_object,agentive_physical_object,non-agentive_physical_object),
partition(?w0,non-physical_object,mental_object,social_object),
partition(?w0,social_object,agentive_social_object,non-agentive_social_object),
partition(?w0,agentive_social_object,social_agent,society),
partition(?w0,perdurant,event,stative),
partition(?w0,event,achievement,accomplishment),
partition(?w0,stative,state,process),
partition(?w0,quality,temporal_quality,physical_quality,abstract_quality),
partition(?w0,region,temporal_region,physical_region,abstract_region)} ];
// (NA17) Instances of SB -- axiom
//(forall (?w0)
// (=> (WORLD ?w0)
// (and (SB ?w0 ALL ED) (SB ?w0 ALL PD) (SB ?w0 ALL Q) (SB ?w0 ALL AB)
// (SB ?w0 ED PED) (SB ?w0 ED NPED) (SB ?w0 ED AS) (SB ?w0 PED M)
// (SB ?w0 PED F) (SB ?w0 PED POB) (SB ?w0 POB APO) (SB ?w0 POB NAPO)
// (SB ?w0 NPED NPOB) (SB ?w0 NPOB MOB) (SB ?w0 NPOB SOB) (SB ?w0 SOB ASO)
// (SB ?w0 SOB NASO) (SB ?w0 ASO SAG) (SB ?w0 ASO SC) (SB ?w0 PD EV)
// (SB ?w0 PD STV) (SB ?w0 EV ACH) (SB ?w0 EV ACC) (SB ?w0 STV ST)
// (SB ?w0 STV PRO) (SB ?w0 Q TQ) (SB ?w0 Q PQ) (SB ?w0 Q AQ) (SB ?w0 TQ TL)
// (SB ?w0 PQ SL) (SB ?w0 AB FACT) (SB ?w0 AB SET) (SB ?w0 AB R) (SB ?w0 R TR)
// (SB ?w0 R PR) (SB ?w0 R AR) (SB ?w0 TR T) (SB ?w0 PR S))))
[ [world ?w0] =>
AND{subsumes(?w0,entity,endurant), subsumes(?w0,entity,perdurant),
subsumes(?w0,entity,quality), subsumes(?w0,entity,abstract)
subsumes(?w0,endurant,physical_endurant),
subsumes(?w0,endurant,non-physical_endurant),
subsumes(?w0,endurant,arbitrary_sum),
subsumes(?w0,physical_endurant,amount_of_matter),
subsumes(?w0,physical_endurant,feature),
subsumes(?w0,physical_endurant,physical_object),
subsumes(?w0,physical_object,agentive_physical_object),
subsumes(?w0,physical_object,non-agentive_physical_object),
subsumes(?w0,non-physical_endurant,non-physical_object),
subsumes(?w0,non-physical_object,mental_object),
subsumes(?w0,non-physical_object,social_object),
subsumes(?w0,social_object,agentive_social_object),
subsumes(?w0,social_object,non-agentive_social_object),
subsumes(?w0,agentive_social_object,social_agent),
subsumes(?w0,agentive_social_object,society),
subsumes(?w0,perdurant,event), subsumes(?w0,perdurant,stative),
subsumes(?w0,event,achievement), subsumes(?w0,event,accomplishment),
subsumes(?w0,stative,state), subsumes(?w0,stative,process),
subsumes(?w0,quality,temporal_quality), subsumes(?w0,quality,physical_quality),
subsumes(?w0,quality,abstract_quality),
subsumes(?w0,temporal_quality,temporal_location),
subsumes(?w0,physical_quality,spatial_location),
subsumes(?w0,abstract,FACT), subsumes(?w0,abstract,SET),
subsumes(?w0,abstract,region),
subsumes(?w0,region,temporal_region), subsumes(?w0,region,physical_region),
subsumes(?w0,region,abstract_region),
subsumes(?w0,temporal_region,time_interval),
subsumes(?w0,physical_region,space_region)} ];
// (NA18) Existence of sum
//(forall (?w0 ?x ?y) (=> (and (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0))
// (exists (?z) (and (PARTICULAR ?z) (+ ?w0 ?x ?y ?z)))))
[sum(world ?w0,particular ?x ,particular ?y, a particular ?z)];
//"a": existential quantifier
// (NA19) Existence of sigma
//(forall (?w0 ?f) (=> (and (UNIVERSAL ?f) (WORLD ?w0))
// (exists (?z) (and (PARTICULAR ?z) (sigma ?w0 ?f ?z)))))
[sigma(world ?w0,particular ?f, a particular ?z)];
// (NA20) Existence of sum.t
//(forall (?w0 ?x ?y) (=> (and (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0))
// (exists (?z) (and (PARTICULAR ?z) (+.t ?w0 ?x ?y ?z)))))
[sum.t(world ?w0,particular ?x,particular ?y, a particular ?z)];
// (NA21) Existence of sigma.t
//(forall (?w0 ?f) (=> (and (UNIVERSAL ?f) (WORLD ?w0))
// (exists (?z) (and (PARTICULAR ?z) (sigma.t ?w0 ?f ?z)))))
[sigma.t(world ?w0,particular ?x, a particular ?z)];
// this could be added in the def. of UNIVERSAL
//(forall (@f) (<=> (UNIVERSAL @f)
// (exists (?g @h) (and (UNIVERSAL ?g)
// (or (UNIVERSAL @h) (= @h (listof)))
// (= @f (listof ?g @h))))))
// this could be added in the def. of PARTICULAR
//(forall (@x)
// (<=> (PARTICULAR @x)
// (exists (?y @z) (and (PARTICULAR ?y)
// (or (PARTICULAR @z) (= @z (listof)))
// (= @x (listof ?y @z))))))
//********************************************************
//pm: D18 Chapter 4 (p27 ...)
//(Dd1) RG: Rigid Universal
if (latex)
{ `\item[\defdolce{defRGd}]
$\RGd(\phi) \triangleq \Box \forall x(\phi(x) \rightarrow \Box \phi(x))$
\hfill{}($\phi$ \textit{is Rigid})'
}
else if (CASL)
{ `RG(phi : Pi) <=> [] forall x : PT . ((x elem phi) => [] (x elem phi)) ;%(Dd1)%'
}
else if (FCG)
{ type rigid_universal__RG (world ?w0, universal ?f) :=
[ wldr(?w0,world ?w) =>
[ ?f(?w,particular ?x) => AND{ wldr(?w,world ?u), ?f(?u,?x) } ] ] (^Dd1^);
}
else if (KIF)
{ (defrelation RG (?w0 ?f) :=
(and (UNIVERSAL ?f) (WORLD ?w0)
(forall (?w ?x) (=> (and (WLDR ?w0 ?w) (WORLD ?w) (PARTICULAR ?x))
(=> (?f ?w ?x)
(forall (?u) (=> (and (WLDR ?w ?u) (WORLD ?u))
(?f ?u ?x))))))))
}
//(Dd2) NEP: Non-Empty Universal
if (latex)
{ `\item[\defdolce{defNEPd}]
$\NEPd(\phi) \triangleq \Box \exists x(\phi(x))$
\hfill{}($\phi$ {\it is Non-E\mpty})'
}
else if (CASL)
{ `NEP(phi : Pi) <=> [] exists x : PT . ((x elem phi)) ;%(Dd2)%'
}
else if (FCG)
{ type non-empty_universal__NEP (world ?w0, universal ?f) :=
[ wldr(?w0,world ?w) => ?f(?w,a particular ?y) ];
}
else if (KIF)
{ (defrelation NEP (?w0 ?f) :=
(and (UNIVERSAL ?f) (WORLD ?w0)
(forall (?w) (=> (and (WLDR ?w0 ?w) (WORLD ?w))
(exists (?y) (and (PARTICULAR ?y) (?f ?w ?y)))))))
}
//(Dd3) DJ: Disjoint Universals
//(defrelation DJ (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0)
// (forall (?w ?x) (=> (and (WLDR ?w0 ?w) (WORLD ?w) (PARTICULAR ?x))
// (not (and (?f ?w ?x) (?g ?w ?x)))))))
type disjoint__DJ (world ?w0, universal ?f, universal ?g) :=
[ wldr(?w0,world ?w) => !AND{ ?f(?w,a particular ?x), ?g(?w,?x) } ];
//(Dd4) SB: Subsumption
//(defrelation SB (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0)
// (forall (?w ?x) (=> (and (WLDR ?w0 ?w) (WORLD ?w) (PARTICULAR ?x))
// (or (not (?g ?w ?x)) (?f ?w ?x))))))
type subsumes__SB (world ?w0, universal ?f, universal ?g) :=
[ wldr(?w0,world ?w) => [ ?g(?w,particular ?x) => ?f(?w,?x) ] ];
//(Dd5) EQ: Equal Universals
//(defrelation equal (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f)(UNIVERSAL ?g)(WORLD ?w0) (SB ?w0 ?f ?g) (SB ?w0 ?g ?f)))
type equal__EQ (world ?w0, universal ?f, universal ?g) :=
AND{subsumes(?w0,?f,?g), subsumes(?w0,?g,?f)};
//(Dd6) PSB: Properly Subsuming
//(defrelation properly_subsumes (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (SB ?w0 ?f ?g)
// (not (SB ?w0 ?f ?g)))) //pm: typo: ?g<->?f (corrected in the translation)
type properly_subsumes__PSB (world ?w0, universal ?f, universal ?g) :=
AND{ subsumes(?w0,?f,?g), !subsumes(?w0,?g,?f) };
//(Dd7) L: Leaf Universal
//(defrelation L (?w0 ?f) :=
// (and (UNIVERSAL ?f) (WORLD ?w0)
// (forall (?w ?g) (=> (and (WLDR ?w0 ?w) (WORLD ?w) (UNIVERSAL ?g))
// (or (not (?SB ?w0 ?f ?g)) (EQ ?w0 ?f ?g)))))) //pm: ?SB in D7+D10
type leaf_type__L (world ?w0, universal ?f) :=
[ wldr(?w0,world ?w) => [subsumes(?w0,?f,?g) => equal(?w0,?f,?g)] ];
//(Dd8) SBL: Leaf Subsumed by
//(defrelation SBL (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (SB ?w0 ?f ?g) (L ?w0 ?g)))
type subsumes_leaf__SBL (world ?w0, universal ?f, universal ?g) :=
AND{ subsumes(?w0,?f,?g), leaf_type(w0,?g) };
//(Dd9) PSBL: Leaf Properly Subsumed by
//(defrelation properly_subsumes_leaf (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0)
// (properly_subsumes ?w0 ?f ?g) (leaf_type ?w0 ?g)))
type properly_subsumes_leaf__PSBL (world ?w0, universal ?f, universal ?g) :=
AND{ properly_subsumes(?w0,?f,?g), leaf_type(w0,?g) };
//(Dd10) L__: Leaf in the set X
//(defrelation L.X (?w0 ?f) :=
// (and (UNIVERSAL ?f) (WORLD ?w0) (X ?f)
// (forall (?w ?g) (=> (and (WLDR ?w0 ?w) (WORLD ?w) (UNIVERSAL ?g))
// (=> (and (?SB ?w ?f ?g) (X ?g)) (EQ ?w ?f ?g))))))
type leaf_in_set__L.X (world ?w0, X ?f) :=
[ wldr(?w0,world ?w) => [subsumes(?w0,?f,rigid_universal ?g) => equal(?w0,?f,?g)] ];
//(Dd11) SBL__
//(defrelation SBL.X (?w0 ?f ?g) :=
(and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (SB ?w0 ?f ?g) (L.X ?w0 ?g)))
type subsumes_leaf_in_set__SBL (world ?w0, universal ?f, universal ?g) :=
AND{ subsumes(?w0,?f,?g), leaf_in_set(w0,?g) };
//(Dd12) PSBL__
//(defrelation PSBL.X (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (PSB ?w0 ?f ?g) (L.X ?w0 ?g)))
type properly_subsumes_leaf_in_set__PSBL.X (world ?w0, universal ?f, universal ?g) :=
AND{ properly_subsumes(?w0,?f,?g), leaf_in_set(w0,?g) };
// Definition (Dd13) is left for expressivity. In practice it becomes superfluous
// since the user needs to give a list of the n-tuple satisfying relation partition in
// axiom (NA17)
//(Dd13) PT: Partition
//(defrelation PT (?w0 ?f @g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL @g) (WORLD ?w0) (not (item ?f @g))
// (forall (?h ?k)
// (and (=> (and (UNIVERSAL ?h)(UNIVERSAL ?k)(item ?h @g)(item ?k @g)(/= ?h ?k))
// (DJ ?w0 ?h ?k))
// (forall (?w ?x) (=> (and (WLDR ?w0 ?w) (WORLD ?w) (PARTICULAR ?x))
// (<=> (?f ?w ?x)
// (exists(?h) (and(UNIVERSAL ?h)
// (item ?h @g)(?h ?w ?x))))))))))
type partition__PT (world ?w0, universal ?f, universal @g) :=
AND{!item(?f,@g),
[AND{item(universal ?h,@g),item(universal ?k,@g),[?h!=?k]} => disjoint(?w0,?h,?k)],
AND{wldr(?w0,world ?w),
[?f(?w,particular ?x) <=>
AND{item(a universal ?h,@g), item(universal ?h,@g), ?h(?w,?x)}]}};
// Mereological Definitions
//(Dd14) PP: Proper Part
//(defrelation PP (?w0 ?x ?y) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0) (P ?w0 ?x ?y) (not (P ?w0 ?y ?x))))
type proper_part__PP (world ?w0, particular ?x, particular ?y) :=
AND{part(?w0,?x,?y), !part(?w0,?y,?x)};
//(Dd15) O: Overlap
//(defrelation O (?w0 ?x ?y) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0)
// (exists (?z) (and (PARTICULAR ?z) (P ?w0 ?z ?x) (P ?w0 ?z ?y)))))
type overlap__O (world ?w0, particular ?x, particular ?y) :=
AND{part(?w0,a particular ?z,?x), part(?w0,?z,?y)};
//(Dd16) At: Atom
//(defrelation At (?w0 ?x):= (and (PARTICULAR ?x) (WORLD ?w0)
(not(exists(?y) (and (PARTICULAR ?y)(PP ?w0 ?y ?x))))))
type atom__At (world ?w0, particular ?x) :=
![proper_part(?w0,a particular ?y,?x)];
//(Dd17) AtP: Atomic Part
//(defrelation AtP (?w0 ?x ?y) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0) (P ?w0 ?x ?y) (At ?w0 ?x)))
type atomic_part__AtP (world ?w0, particular ?x, particular ?y) :=
AND{part(?w0,?x,?y), atom(?w0,?x)};
//(Dd18) _+_ Binary Sum
//(defrelation + (?w0 ?x ?y ?z) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?z) (WORLD ?w0)
// (forall (?u) (=> (PARTICULAR ?u)
// (<=> (O ?w0 ?u ?z) (or (O ?w0 ?u ?x) (O ?w0 ?u ?y)))))
// (forall (?z1) (=> (and (PARTICULAR ?z1)
// (forall (?u) (=> (PARTICULAR ?u)
// (<=> (O ?w0 ?u ?z1)
// (or (O ?w0 ?u ?x)(O ?w0 ?u ?y))))))
// (= ?z1 ?z)))))
type sum (world ?w0, particular ?x, particular ?y, particular ?z) :=
!AND{[overlap(?w0,particular ?u,?z) <=> OR{overlap(?w0,?u,?x), overlap(?w0,?u,?y)}],
[ [overlap(?w0,particular ?u1,particular ?z1) <=>
OR{overlap(?w0,?u1,?x), overlap(?w0,?u1,?y)}] => [?z1 = ?z] ]};
//pm: automatically translating back to the original KIF formula won't be easy
//(Dd19) (general) Sum
// Note: the rendition in KIF is weaker than the corresponding definition in
//modal FOL: here ?f has to be one of the universal introduced explicitly.
//[A possible way out: use string-variables (@f) to code Boolean
//combinations of universals.]
(defrelation sigma (?w0 ?f ?z) :=
(and (PARTICULAR ?z) (UNIVERSAL ?f) (WORLD ?w0)
(forall (?y)
(=> (PARTICULAR ?y) (<=> (O ?w0 ?y ?z)
(exists (?v)
(and (PARTICULAR ?v) (?f ?w0 ?v) (O ?w0 ?y ?v))))))
(forall (?z1)
(=> (PARTICULAR ?z1)
(exists (?y)
(and (PARTICULAR ?y)
(=> (<=> (O ?w0 ?y ?z1)
(exists (?v)
(and (PARTICULAR ?v) (?f ?w0 ?v) (O ?w0 ?y ?v)))))
(= ?z1 ?z)))))))
type sigma__general_sum (world ?w0, universal ?f, particular ?z) :=
!AND{[overlap(?w0,particular ?y,?z) <=>
AND{?f(?w0,a particular ?v), overlap(?w0,?y,?v)}],
[ [overlap(?w0,a particular ?y1,particular ?z1) <=>
AND{?f(?w0,a particular ?v1), overlap(?w0,?y,?v1)}] => [?z1 = ?z] ]};
//(Dd20) PP: Temporary Proper Part
//(defrelation PP (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0)
// (P ?w0 ?x ?y ?t) (not (P ?w0 ?y ?x ?t))))
type temporary_proper_part__PP (world ?w0, particular ?x, particular ?y, particular ?t)
:= AND{temporary_part(?w0,?x,?y,?t), !temporary_part(?w0,?y,?x,?t)};
//(Dd21) O: Temporary Overlap
//(defrelation O (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0)
// (exists (?z) (and (PARTICULAR ?z) (P ?w0 ?z ?x ?t) (P ?w0 ?z ?y ?t)))))
type overlap__O (world ?w0, particular ?x, particular ?y, particular ?t) :=
AND{temporary_part(?w0,a particular ?z,?x,?t), temporary_part(?w0,?z,?y,?t)};
//(Dd22) At: Temporary Atom
//(defrelation At (?w0 ?x ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?t) (WORLD ?w0)
// (not (exists (?y) (and (PARTICULAR ?y) (PP ?w0 ?y ?x ?t))))))
type temporary_atom__At (world ?w0, particular ?x, particular ?t) :=
![temporary_proper_part(?w0,a particular ?y,?x,?t)];
//(Dd23) AtP: Temporary Atomic Part
//(defrelation AtP (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0)
// (P ?w0 ?x ?y ?t) (At ?w0 ?x ?t)))
type temporary_atomic_part__AtP (world ?w0, particular ?x, particular ?y, particular ?t)
:= AND{temporary_part(?w0,?x,?y,?t), temporary_atom(?w0,?x,?t)};
//(Dd24) Coincidence
//(defrelation =.t (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0)
// (P ?w0 ?x ?y ?t) (P ?w0 ?y ?x ?t)))
type coincidence (world ?w0, particular ?x, particular ?y, particular ?t) :=
AND{temporary_part(?w0,?x,?y,?t), temporary_part(?w0,?y,?x,?t)};
//(Dd25) CP: Constant Part
//(defrelation CP (?w0 ?x ?y) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0)
// (exists (?t) (and (PARTICULAR ?t) (PRE ?w0 ?y ?t)))
// (forall (?t) (=> (and (PARTICULAR ?t) (PRE ?w0 ?y ?t)) (P ?w0 ?x ?y ?t)))))
type constant_part__CP (world ?w0, particular ?x, particular ?y) :=
AND{present_at(?w0,?y,a particular ?t),
[present_at(?w0,?y,particular ?t1) => temporary_part(?w0,?x,?y,?t1)]};
//(Dd26)
//(defrelation +.t (?w0 ?x ?y ?z) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?z) (WORLD ?w0)
// (forall (?u ?t)
// (=> (and (PARTICULAR ?u) (PARTICULAR ?t))
// (<=> (O ?w0 ?u ?z ?t) (or (O ?w0 ?u ?x ?t) (O ?w0 ?u ?y ?t)))))
// (forall (?z1 ?t)
// (=> (and (PARTICULAR ?z1) (PARTICULAR ?t)
// (forall (?u) (=> (PARTICULAR ?u)
// (<=> (O ?w0 ?u ?z1 ?t)
// (or (O ?w0 ?u ?x ?t) (O ?w0 ?u ?y ?t))))))
// (= ?z1 ?z)))))
type binary_sum.t (world ?w0, particular ?x, particular ?y, particular ?z) :=
!AND{[overlap(?w0,particular ?u,?z,particular ?t) <=>
OR{overlap(?w0,?u,?x,?t), overlap(?w0,?u,?y,?t)}],
[ [overlap(?w0,particular ?u1,particular ?z1,particular ?t1) <=>
OR{overlap(?w0,?u1,?x,?t1), overlap(?w0,?u1,?y,?t1)}] => [?z1 = ?z] ]};
//(Dd27)
// NOTE: this rendition includes only the listed universal, for instance,
// no Boolean combination of universals is included [see also comment on (D19)]
//(defrelation sigma.t (?w0 ?f ?z) :=
// (and (PARTICULAR ?z) (UNIVERSAL ?f) (WORLD ?w0)
// (forall (?y ?t)
// (=> (and (PARTICULAR ?y) (PARTICULAR ?t))
// (<=> (O ?w0 ?y ?z ?t)
// (exists (?v)
// (and (PARTICULAR ?v) (?f ?w0 ?v) (O ?w0 ?y ?v ?t))))))
// (forall (?z1 ?t)
// (=> (and (PARTICULAR ?z1) (PARTICULAR ?t))
// (exists (?y)
// (and (PARTICULAR ?y)
// (=> (<=> (O ?w0 ?y ?z1 ?t)
// (exists (?v)
// (and (PARTICULAR ?v) (?f ?w0 ?v) (O ?w0 ?y ?v ?t))))
// (= ?z1 ?z))))))))
type sigma.t__general_sum (world ?w0, universal ?f, particular ?z) :=
!AND{[overlap(?w0,particular ?y,?z,particular ?t) <=>
AND{?f(?w0,a particular ?v), overlap(?w0,?y,?v,t)}],
[ [overlap(?w0,a particular ?y1,particular ?z1,particular ?t1) <=>
AND{?f(?w0,a particular ?v1), overlap(?w0,?y,?v1,?t1)}] => [?z1 = ?z] ]};
// Quality
//(Dd28) dqt: Direct Quality
//(defrelation dqt (?w0 ?x ?y) :=
// (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (qt ?w0 ?x ?y)
// (not (exists (?z) (and (PARTICULAR ?z) (qt ?w0 ?x ?z) (qt ?w0 ?z ?y))))))
type direct_quality__dqt (world ?w0, particular ?x, particular ?y) :=
!AND{qt(?w0,?x,a particular ?z), qt(?w0,?z,?y)};
//(Dd29) qt: Quality of type
//(defrelation qtf (?w0 ?f ?x ?y) :=
// (and (UNIVERSAL ?f) (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0)
// (qt ?w0 ?x ?y) (?f ?w0 ?x) (SBL.X ?w0 Q ?f)))
type qtf__quality_of_type (world ?w0, universal ?f, particular ?x, particular ?y) :=
AND{qt(?w0,?x,?y), ?f(?w0,?x), subsumes_leaf_in_set(?w0,quality,?f)};
// Temporal and Spatial Quale
//(Dd30) ql_T,PD
//(defrelation ql.T.PD (?w0 ?t ?x) :=
// (and (PARTICULAR ?t) (PARTICULAR ?x) (WORLD ?w0) (PD ?w0 ?x)
// (exists (?z) (and (PARTICULAR ?z) (qtf ?w0 TL ?z ?x) (ql ?w0 ?t ?z)))))
type ql_T.PD__temporal_quale_for_perdurant (world ?w0, particular ?t, particular ?x)
:= AND{perdurant(?w0,?x), qtf(?w0,temporal_location,a particular ?z,?x),
ql(?w0,?t,?z)};
//(Dd31) ql_T,ED
//(defrelation ql.T.ED (?w0 ?t ?x) :=
// (and (PARTICULAR ?t) (PARTICULAR ?x) (WORLD ?w0) (ED ?w0 ?x)
// (forall (?u)
// (=> (PARTICULAR ?u)
// (<=> (O ?w0 ?u ?t)
// (exists (?v ?y) (and (PARTICULAR ?v) (PARTICULAR ?y)
// (PC ?w0 ?x ?y ?v) (O ?w0 ?u ?v))))))
// (forall (?t1)
// (=> (PARTICULAR ?t1)
// (exists (?u)
// (and (PARTICULAR ?u)
// (=> (<=> (O ?w0 ?u ?t1)
// (exists (?v ?y)
// (and (PARTICULAR ?v) (PARTICULAR ?y)
// (PC ?w0 ?x ?y ?v) (O ?w0 ?u ?v))))
// (= ?t1 ?t))))))))
type ql_T.ED__temporal_quale_for_endurant (world ?w0, particular ?t, particular ?x) :=
AND{endurant(?w0,?x),
[overlap(?w0,particular ?u,?t) <=>
AND{participant(?w0,?x,a particular ?y,a particular ?v), overlap(?w0,?u,?v)}],
[ [overlap(?w0,a particular ?u1,particular ?t1) <=>
AND{participant(?w0,?x,a particular ?y1,a particular ?v1),
overlap(?w0,?u1,?v1)}],
=> [?t1 = ?t] ]};
//(Dd32) ql_T,TQ
//(defrelation ql.T.TQ (?w0 ?t ?x) :=
// (and (PARTICULAR ?t) (PARTICULAR ?x) (WORLD ?w0) (TQ ?w0 ?x)
// (exists (?z) (and (PARTICULAR ?z) (qt ?w0 ?x ?z) (ql.T.PD ?w0 ?t ?z)))))
type ql_T.TQ__temporal_quale_for_temporal_quality
(world ?w0, particular ?t, particular ?x) :=
AND{temporal_quality(?w0,?x), qt(?w0,?x,a particular ?z), ql.T.PD(?w0,?t,?z)};
//(Dd33) ql_T,PQ_or_AQ
//(defrelation ql.T.PQAQ (?w0 ?t ?x) :=
// (and (PARTICULAR ?t) (PARTICULAR ?x) (WORLD ?w0)
// (or (PQ ?w0 ?x) (AQ ?w0 ?x))
// (exists (?z) (and (PARTICULAR ?z) (qt ?w0 ?x ?z) (ql.T.ED ?w0 ?t ?z)))))
type ql.T.PQAQ__temporal_quale_for_physical_or_abstract_quality
(world ?w0, particular ?t, particular ?x) :=
AND{ OR{physical_quality(?w0,?x), abstract_quality(?w0,?x)},
qt(?w0,?x,a particular ?z), ql.T.ED(?w0,?t,?z)};
//(Dd34) ql_T,Q
//(defrelation ql.T.Q (?w0 ?t ?x) :=
// (and (PARTICULAR ?t) (PARTICULAR ?x) (WORLD ?w0)
// (or (ql.T.TQ ?w0 ?t ?x) (ql.T.PQAQ ?w0 ?t ?x))))
type ql.T.Q__temporal_quale_for_quality (world ?w0, particular ?t, particular ?x) :=
OR{ql.T.TQ(?w0,?t,?x), ql.T.PQAQ(?w0,?t,?x)};
//(Dd35) ql_T: Temporal Quale
//(defrelation ql.T (?w0 ?t ?x) :=
// (and (PARTICULAR ?t) (PARTICULAR ?x) (WORLD ?w0)
// (or (ql.T.ED ?w0 ?t ?x) (ql.T.PD ?w0 ?t ?x) (ql.T.Q ?w0 ?t ?x))))
type ql.T__temporal_quale (world ?w0, particular ?t, particular ?x) :=
OR{ql.T.ED(?w0,?t,?x), ql.T.PD(?w0,?t,?x), ql.T.Q(?w0,?t,?x)};
//(Dd36) ql_S,PED
//(defrelation ql.S.PED (?w0 ?s ?x ?t) :=
// (and (PARTICULAR ?s) (PARTICULAR ?x) (PARTICULAR ?t) (WORLD ?w0) (PED ?w0 ?x)
// (exists (?z) (and (PARTICULAR ?z) (qtf ?w0 SL ?z ?x) (ql ?w0 ?s ?z ?t)))))
type ql.S.PED__spatial_quale_for_physical_endurant
(world ?w0, particular ?s, particular ?x, particular ?t) :=
AND{physical_endurant(?w0,?x), qtf(?w0,spatial_location,,a particular ?z,?x),
temporary_quale(?w0,?s,?z,?t)};
//(Dd37) ql_S,PQ
//(defrelation ql.S.PQ (?s ?x ?t) :=
(and (PARTICULAR ?s) (PARTICULAR ?x) (PARTICULAR ?t) (WORLD ?w0) (PQ ?w0 ?x)
(exists (?z) (and (PARTICULAR ?z) (qt ?w0 ?x ?z) (ql.S.PED ?w0 ?s ?z ?t)))))
type ql.S.PQ__spatial_quale_for_physical_quality
(world ?w0, particular ?s, particular ?x, particular ?t) :=
AND{physical_quality(?w0,?x), qt(?w0,?x,a particular ?z), ql.S.PED(?w0,?s,?z,?t)};
//(Dd38) ql_S,PD
//(defrelation ql.S.PD (?w0 ?s ?x ?t) :=
// (and (PARTICULAR ?s) (PARTICULAR ?x) (PARTICULAR ?t) (WORLD ?w0) (PD ?w0 ?x)
// (exists (?z) (and (PARTICULAR ?z) (mppc ?w0 ?z ?x) (ql.S.PED ?w0 ?s ?z ?t)))))
type ql.S.PD__spatial_quale_for_perdurant
(world ?w0, particular ?s, particular ?x, particular ?t) :=
AND{perdurant(?w0,?x), mppc(?w0,a particular ?z,?x), ql.S.PED(?w0,?s,?z,?t)};
//(Dd39) ql_S: Spatial Quale
//(defrelation ql.S (?w0 ?s ?x ?t) :=
// (and (PARTICULAR ?s) (PARTICULAR ?x) (PARTICULAR ?t) (WORLD ?w0)
// (or (ql.S.PED ?w0 ?s ?x ?t) (ql.S.PQ ?w0 ?s ?x ?t) (ql.S.PD ?w0 ?s ?x ?t))))
type ql.S__spatial_quale (world ?w0, particular ?s, particular ?x, particular ?t) :=
OR{ql.S.PED(?w0,?s,?x,?t), ql.S.PQ(?w0,?s,?x,?t), ql.S.PD(?w0,?s,?x,?t)};
//Being present
//(Dd40) PRE: Being Present at
//(defrelation PRE (?w0 ?x ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?t) (WORLD ?w0)
// (exists (?u) (and (PARTICULAR ?u) (ql.T ?w0 ?u ?x) (P ?w0 ?t ?u)))))
type present_at__PRE (world ?w0, particular ?x, particular ?t) :=
AND{ql.T(?w0,a particular ?u,?x), part(?w0,?t,?u)};
//(Dd41) PRE: Being Present in at
//(defrelation PRE (?w0 ?x ?s ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?s) (PARTICULAR ?t) (WORLD ?w0) (PRE ?w0 ?x ?t)
// (exists (?u) (and (PARTICULAR ?u) (ql.S ?w0 ?u ?x ?t) (P ?w0 ?s ?u)))))
type present_in_at__PRE (world ?w0, particular ?x, particular ?s, particular ?t) :=
AND{present_at(?w0,?x,?t), ql.S(?w0,a particular ?u,?x,?t), part(?w0,?s,?u)};
// Inclusion and Coincidence
//(Dd42) Temporal Inclusion
//(defrelation incl.T (?w0 ?x ?y) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0)
// (exists (?t ?u) (and (PARTICULAR ?t) (PARTICULAR ?u)
// (ql.T ?w0 ?t ?x) (ql.T ?w0 ?u ?y) (P ?w0 ?t ?u)))))
type incl.T__temporal_inclusion (world ?w0, particular ?x, particular ?y) :=
AND{ql.T(?w0,a particular ?t,?x), ql.T(?w0,a particular ?u,?y), part(?w0,?t,?u)};
//(Dd43) Proper Temporal Inclusion
//(defrelation sincl.T (?w0 ?x ?y) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0)
// (exists (?t ?u) (and (PARTICULAR ?t) (PARTICULAR ?u)
// (ql.T ?w0 ?t ?x) (ql.T ?w0 ?u ?y) (PP ?w0 ?t ?u)))))
type sincl.T__proper_temporal_inclusion (world ?w0, particular ?x, particular ?y) :=
AND{ql.T(?w0,a particular ?t,?x), ql.T(?w0,a particular ?u,?y),
proper_part(?w0,?t,?u)};
//(Dd44) Temporary Spatial Inclusion
//(defrelation incl.S.t (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0)
// (exists (?s ?r) (and (PARTICULAR ?s) (PARTICULAR ?r)
// (ql.S ?w0 ?s ?x ?t) (ql.S ?w0 ?r ?y ?t) (P ?w0 ?s ?r)))))
type incl.S.t__temporary_spatial_inclusion
(world ?w0, particular ?x, particular ?y, particular ?t) :=
AND{ql.S(?w0,a particular ?s,?x,?t), ql.S(?w0,a particular ?r,?y,?t),
part(?w0,?s,?r)};
//(Dd45) Temp. Proper Sp. Inclusion
//(defrelation sincl.S.t (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0)
// (exists (?s ?r) (and (PARTICULAR ?s) (PARTICULAR ?r)
// (ql.S ?w0 ?s ?x ?t) (ql.S ?w0 ?r ?y ?t) (PP ?w0 ?s ?r)))))
type sincl.S.t__temporary_proper_spatial_inclusion
(world ?w0, particular ?x, particular ?y, particular ?t) :=
AND{ql.S(?w0,a particular ?s,?x,?t), ql.S(?w0,a particular ?r,?y,?t),
proper_part(?w0,?s,?r)};
//(Dd46) Spatio-temporal Inclusion
//(defrelation incl.S.T (?w0 ?x ?y) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0)
// (exists (?t) (and (PARTICULAR ?t) (PRE ?w0 ?x ?t)))
// (forall (?t) (=> (and (PARTICULAR ?t) (PRE ?w0 ?x ?t))
// (incl.S.t ?w0 ?x ?y ?t)))))
type incl.S.T__spatio-temporal_inclusion (world ?w0, particular ?x, particular ?y) :=
AND{present_at(?w0,?x,a particular ?t),
[present_at(?w0,?x,particular ?t1) => incl.S.t(?w0,?x,?y,?t1)]};
//(Dd47) Spatio-temp. Incl. during
//(defrelation incl.S.T.t (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0) (PRE ?w0 ?x ?t)
// (forall (?u) (=> (and (PARTICULAR ?u) (AtP ?w0 ?u ?t))
// (incl.S.t ?w0 ?x ?y ?u)))))
type incl.S.T.t__temporary_spatio-temporal_inclusion
(world ?w0, particular ?x, particular ?y, particular ?t) :=
AND{present_at(?w0,?x,?t),
[atomic_part(?w0,particular ?u,?t) => incl.S.t(?w0,?x,?y,?u)]};
//(Dd48) Temporal Coincidence
//(defrelation ~.T (?w0 ?x ?y) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0)
// (incl.T ?w0 ?x ?y) (incl.T ?w0 ?y ?x)))
type temporal_coincidence__~.T (world ?w0, particular ?x, particular ?y) :=
AND{incl.T(?w0,?x,?y), incl.T(?w0,?y,?x)};
//(Dd49) Temporary Spatial Coincidence
//(defrelation ~.S.t (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0)
// (incl.S.t ?w0 ?x ?y ?t) (incl.S.t ?w0 ?y ?x ?t)))
type temporary_spatial_coincidence__~.S.t
(world ?w0, particular ?x, particular ?y, particular ?t) :=
AND{incl.S.t(?w0,?x,?y,?t), incl.S.t(?w0,?y,?x,?t)};
//(Dd50) Spatio-temporal Coincidence
//(defrelation ~.S.T (?w0 ?x ?y) :=
// (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y)
// (incl.S.T ?w0 ?x ?y) (incl.S.T ?w0 ?y ?x)))
type spatio-temporal_coincidence__~.S.T (world ?w0, particular ?x, particular ?y) :=
AND{incl.S.T(?w0,?x,?y), incl.S.T(?w0,?y,?x)};
//(Dd51) Spatio-temp. Coincidence during
//(defrelation ~.S.T.t (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0) (PRE ?w0 ?x ?t)
// (forall (?u) (=> (and (PARTICULAR ?u) (AtP ?w0 ?u ?t))
// (~.S.t ?w0 ?x ?y ?u)))))
type temporary_spatio-temporal_coincidence__~.S.T.t
(world ?w0, particular ?x, particular ?y, particular ?t) :=
AND{present_at(?w0,?x,?t), atomic_part(?w0,particular ?u,?t),
temporary_spatial_coincidence(?w0,?x,?y,?u)};
//(Dd52) O_T: Temporal Overlap
//(defrelation O.T (?w0 ?x ?y) :=
// (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y)
// (exists (?t ?u) (and (PARTICULAR ?t) (PARTICULAR ?u)
// (ql.T ?w0 ?t ?x) (ql.T ?w0 ?u ?y) (O ?w0 ?t ?u)))))
type temporal_overlap__O_T (world ?w0, particular ?x, particular ?y) :=
AND{ql.T(?w0,a particular ?t,?x), ql.T(?w0,a particular ?u,?y), overlap(?w0,?t,?u)};
//(Dd53) O_S,t: Temporary Spatial Overlap
//(defrelation O.S.t (?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0)
// (exists (?s ?r) (and (PARTICULAR ?s) (PARTICULAR ?r)
// (ql.S ?w0 ?s ?x ?t) (ql.S ?w0 ?r ?y ?t) (O ?w0 ?s ?r)))))
type temporary_spatial_overlap__O.S.t
(world ?w0, particular ?x, particular ?y, particular ?t)
:= AND{ql.S(?w0,a particular ?s,?x,?t), ql.S(?w0,a particular ?r,?y,t),
overlap(?w0,?s,?r)};
// Perdurant
//(Dd54) P_T: Temporal Part
//(defrelation P.T (?w0 ?x ?y) :=
// (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PD ?w0 ?x) (P ?w0 ?x ?y)
// (forall (?z) (=> (and (PARTICULAR ?z) (P ?w0 ?z ?y) (incl.T ?w0 ?z ?x))
// (P ?w0 ?z ?x)))))
type temporal_part__P_T (world ?w0, particular ?x, particular ?y) :=
AND{perdurant(?w0,?x), part(?w0,?x,?y),
[AND{part(?w0,particular ?z,?y), incl.T(?w0,?z,?x)} => part(?w0,?z,?x)]};
//(Dd55) P_S: Spatial Part
//(defrelation P.S (?w0 ?x ?y) :=
// (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y)
// (PD ?w0 ?x) (P ?w0 ?x ?y) (~.T ?w0 ?x ?y)))
type spatial_part__P_S (world ?w0, particular ?x, particular ?y) :=
AND{perdurant(?w0,?x), part(?w0,?x,?y), temporal_coincidence(?w0,?x,?y)};
//(Dd56) NEP_S: Strongly Non-Empty
//(defrelation NEP.S (?w0 ?f) :=
// (and (UNIVERSAL ?f) (WORLD ?w0) (SB ?w0 PD ?f)
// (forall (?w) (=> (and (WLDR ?w0 ?w) (WORLD ?w))
// (exists (?x ?y) (and (PARTICULAR ?x) (PARTICULAR ?y)
// (?f ?w ?x) (?f ?w ?y)
// (not (P ?w ?x ?y)) (not(P ?w ?y ?x))))))))
type strongly_non-empty_perdurant_class__NEP.S (world ?w0, universal ?f) :=
AND{subsumes(?w0,perdurant,?f), wldr(?w0,world ?w),
?f(w,particular ?x), ?f(w,particular ?y), !part(?w,?x,?y), !part(?w,?y,?x)};
//(Dd57) CM: Cumulative
//(defrelation CM (?w0 ?f) :=
// (and (UNIVERSAL ?f) (WORLD ?w0) (SB ?w0 PD ?f)
// (forall (?w ?x ?y ?z)
// (=> (and (WLDR ?w0 ?w)(WORLD ?w)(PARTICULAR ?x)(PARTICULAR ?y)(PARTICULAR ?z)
// (+ ?w ?x ?y ?z) (?f ?w ?x) (?f ?w ?y))
// (?f ?w ?z)))))
type cumulative_perdurant_class__CM (world ?w0, universal ?f) :=
AND{subsumes(?w0,perdurant,?f), wldr(?w0,world ?w),
[AND{sum(?w,particular ?x,particular ?y,particular ?z), ?f(w,?x), ?f(w,?y)}
=> ?f(w,?z)]};
//(Dd58) cumulative_perdurant_class: Anti-Cumulative
//(defrelation CM~ (?w0 ?f) :=
// (and (UNIVERSAL ?f) (WORLD ?w0) (SB ?w0 PD ?f)
// (forall (?w ?x ?y ?z)
// (=>(and(WLDR ?w0 ?w)(WORLD ?w)(PARTICULAR ?x)(PARTICULAR ?y)(PARTICULAR ?z)
// (+ ?w ?x ?y ?z) (?f ?w ?x) (?f ?w ?y)
// (not (P ?w ?x ?y)) (not (P ?w ?y ?x)))
// (not(?f ?w ?z))))))
type anticumulative_perdurant_class__CM~ (world ?w0, universal ?f) :=
AND{subsumes(?w0,perdurant,?f), wldr(?w0,world ?w),
[AND{sum(?w,particular ?x,particular ?y,particular ?z), ?f(w,?x), ?f(w,?y),
!part(?w,?x,?y), !part(?w,?y,?x)}
=> !?f(w,?z)]};
//(Dd59) HOM: Homeomerous
//(defrelation HOM (?w0 ?f) :=
// (and(UNIVERSAL ?f) (WORLD ?w0) (SB ?w0 PD ?f)
// (forall(?w ?x ?y) (=>(and(WLDR ?w0 ?w)(WORLD ?w)(PARTICULAR ?x)(PARTICULAR ?y)
// (?f ?w ?x) (P.T ?w ?y ?x))
// (?f ?w ?y)))))
type homeomerous_perdurant_class__HOM (world ?w0, universal ?f) :=
AND{subsumes(?w0,perdurant,?f), wldr(?w0,world ?w),
[AND{wldr(?w0,world ?w), ?f(w,particular ?x),
?temporal_part(?w,particular ?y,?x)} => ! ?f(w,?z)]};
//(Dd60) HOM~: Anti-Homeom.
//(defrelation HOM~ (?w0 ?f) :=
// (and (UNIVERSAL ?f) (WORLD ?w0) (SB ?w0 PD ?f)
// (forall (?w ?x)
// (=> (and (WLDR ?w0 ?w) (WORLD ?w) (PARTICULAR ?x) (?f ?w ?x))
// (exists (?y) (and (PARTICULAR ?y) (P.T ?w ?y ?x) (not (?f ?w ?y))))))))
type anti-homeomerous_perdurant_class__HOM~ (world ?w0, universal ?f) :=
AND{subsumes(?w0,perdurant,?f), wldr(?w0,world ?w),
[AND{wldr(?w0,world ?w),?f(w,particular ?x),
?temporal_part(?w,a particular ?y,?x)} => !?f(w,?z)]};
//(Dd61) AT: Atomic
//(defrelation AT (?w0 ?f) :=
// (and (UNIVERSAL ?f) (WORLD ?w0) (SB ?w0 PD ?f)
// (forall (?w ?x) (=> (and (WLDR ?w0 ?w) (WORLD ?w) (PARTICULAR ?x)
// (?f ?w ?x)) (At ?w ?x)))))
type atomic_perdurant_class__AT (world ?w0, universal ?f) :=
AND{subsumes(?w0,perdurant,?f), wldr(?w0,world ?w),
[AND{wldr(?w0,world ?w), ?f(w,particular ?x), ?f(?w,particular ?x)}
=> atom(w,?x)]};
//(Dd62) AT~: Anti-Atomic
//(defrelation AT~ (?w0 ?f) :=
// (and (UNIVERSAL ?f) (WORLD ?w0) (SB ?w0 PD ?f)
// (forall (?w ?x) (=> (and (WLDR ?w0 ?w) (WORLD ?w) (PARTICULAR ?x) (?f ?w ?x))
// (not (At ?w ?x))))))
type anti-atomic_perdurant_class__AT~ (world ?w0, universal ?f) :=
AND{subsumes(?w0,perdurant,?f), wldr(?w0,world ?w),
[AND{wldr(?w0,world ?w), ?f(w,particular ?x), ?f(?w,particular ?x)}
=> !atom(w,?x)]};
//Participation
//(Dd63) PC_C: Constant Participation
//(defrelation PC.C (?w0 ?x ?y) :=
// (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y)
// (exists (?t) (and (PARTICULAR ?t) (PRE ?w0 ?y ?t)))
// (forall (?t) (=> (and (PARTICULAR ?t) (PRE ?w0 ?y ?t)) (PC ?w0 ?x ?y ?t)))))
type constant_participant__PC.C (world ?w0, particular ?x, particular ?y) :=
AND{present_at(?w0,?y,a particular ?t),
[present_at(?w0,?y,particular ?t1) => participant(?w0,?x,?y,?t1)]};
//(Dd64) PC.T: Temporary Total Particip. //pm: assuming PC.t instead of PC.T
//(defrelation PC.T (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0) (PD ?w0 ?y)
// (forall (?z) (=> (and (PARTICULAR ?z) (P ?w0 ?z ?y) (PRE ?w0 ?z ?t))
// (PC ?w0 ?x ?z ?t)))))
type temporary_total_participant__PC.t (world ?w0, particular ?x, particular ?y,
particular ?t) :=
AND{perdurant(?w0,?y),
[AND{part(?w0,particular ?z,?y), present_at(?w0,?z,?t)} =>
participant(?w0,?x,?y,?t)]};
//(Dd65) PC.T: Total Participation
//(defrelation PC.T (?w0 ?x ?y) :=
// (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y)
// (exists (?t) (and (PARTICULAR ?t) (ql.T ?w0 ?t ?y) (PC.T ?w0 ?x ?y ?t)))))
type total_participant__PC.T (world ?w0, particular ?x, particular ?y) :=
AND{ql.T(?w0,a particular ?t,?y), temporary_total_participant(?w0,?x,?y,?t)};
//(Dd66) mpc: Maximal Participant
//(defrelation mpc (?w0 ?x ?y) :=
// (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y)
// (forall (?z ?t)
// (=> (and (PARTICULAR ?z) (PARTICULAR ?t))
// (<=> (O ?w0 ?z ?x ?t)
// (exists (?v)
// (and (PARTICULAR ?v) (PC.T ?w0 ?v ?y ?t) (O ?w0 ?z ?v ?t))))))
// (forall (?z ?x1 ?t)
// (=> (and (PARTICULAR ?z) (PARTICULAR ?x1) (PARTICULAR ?t)
// (<=> (O ?w0 ?z ?x1 ?t)
// (exists (?v)
// (and(PARTICULAR ?v)(PC.T ?w0 ?v ?y ?t)(O ?w0 ?z ?v ?t)))))
// (= ?x1 ?x)))))
type maximal_participant__mpc (world ?w0, particular ?x, particular ?y) :=
AND{perdurant(?w0,?y),
[overlap(?w0,particular ?z,?x,particular ?t) <=>
AND{temporary_total_participant(?w0,a particular ?v,?y,?t),
overlap(?w0,?z,?v,?t)}]
[ [overlap(?w0,particular ?z1,particular ?x1,particular ?t1) <=>
AND{temporary_total_participant(?w0,a particular ?v1,?y,?t1),
overlap(?w0,?z1,?v1,?t1)}]
=> [?x1 = ?x] ]};
//(Dd67) mppc: Maximal Physical Participant
//(defrelation mppc (?w0 ?x ?y) :=
// (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y)
// (forall (?z ?t)
// (=> (and (PARTICULAR ?z) (PARTICULAR ?t))
// (<=> (O ?w0 ?z ?x ?t)
// (exists (?v) (and (PARTICULAR ?v) (PC.T ?w0 ?v ?y ?t)
// (PED ?w0 ?z) (O ?w0 ?z ?v ?t))))))
// (forall (?z ?x1 ?t)
// (=> (and (PARTICULAR ?z) (PARTICULAR ?x1) (PARTICULAR ?t)
// (<=> (O ?w0 ?z ?x1 ?t)
// (exists (?v) (and (PARTICULAR ?v) (PC.T ?w0 ?v ?y ?t)
// (PED ?w0 ?z) (O ?w0 ?z ?v ?t)))))
// (= ?x1 ?x)))))
type maximal_physical_participant__mppc (world ?w0, particular ?x, particular ?y) :=
AND{perdurant(?w0,?y),
[overlap(?w0,particular ?z,?x,particular ?t) <=>
AND{temporary_total_participant(?w0,a particular ?v,?y,?t),
physical_endurant(?w0,?z), overlap(?w0,?z,?v,?t)}]
[ [overlap(?w0,particular ?z1,particular ?x1,particular ?t1) <=>
AND{temporary_total_participant(?w0,a particular ?v1,?y,?t1),
physical_endurant(?w0,?z1), overlap(?w0,?z1,?v1,?t1)}]
=> [?x1 = ?x] ]};
//(Dd68) lf: Life
//(defrelation lf ?w0,?x,?y) :=
// (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y)
// (forall (?z) (=> (PARTICULAR ?z)
// (<=> (O ?w0 ?z ?x)
// (exists (?v) (and (PARTICULAR ?v)
// (PC.T ?w0 ?y ?v) (O ?w0 ?z ?v))))))
// (forall (?z ?u)
// (=> (and (PARTICULAR ?z) (PARTICULAR ?u)
// (<=> (O ?w0 ?z ?u)
// (exists (?v) (and (PARTICULAR ?v)
// (PC.T ?w0 ?y ?v) (O ?w0 ?z ?v)))))
// (= ?u ?x)))))
type life__lf (world ?w0, particular ?x, particular ?y) :=
AND{[overlap(?w0,particular ?z,?x) <=>
AND{total_participant(?w0,?y,a particular ?v), overlap(?w0,?z,?v)}],
[ [overlap(?w0,particular ?z1,particular ?u) <=>
AND{total_participant(?w0,?y,a particular ?v1), overlap(?w0,?z,?v1)}]
=> [?u = ?x] ]};
// Dependence
//(Dd69) SD: Specific Constant Dep.
//(defrelation SD (?w0 ?x ?y) :=
// (or (and (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0)
// (forall (?w)
// (=> (and (WLDR ?w0 ?w) (WORLD ?w))
// (and (exists (?t) (and (PARTICULAR ?t) (PRE ?w ?x ?t)))
// (forall (?t) (=> (and (PARTICULAR ?t) (PRE ?w ?x ?t))
// (PRE ?w ?y ?t)))))))
// (and (UNIVERSAL ?x) (UNIVERSAL ?y) (WORLD ?w0) (DJ ?w0 ?x ?y)
// (forall (?w ?x1)
// (=> (and (WLDR ?w0 ?w) (WORLD ?w) (PARTICULAR ?x1) (?x ?w ?x1))
// (exists (?y1) (and (PARTICULAR ?y1)
// (?y ?w ?y1) (SD ?w ?x1 ?y1))))))))
specific_constant_dependant__SD
> specific_constant_dependant_on_particulars
specific_constant_dependant_on_universals;
type specific_constant_dependant_on_particulars__SD
(world ?w0, particular ?x, particular ?y)
:= AND{[wldr(?w0,world ?w) =>
AND{present_at(?w,?x,a particular ?t), present_at(?w,?y,?t)}]};
type specific_constant_dependant_on_universals__SD
(world ?w0, universal ?x, universal ?y) :=
AND{disjoint(?w0,?x,?y),
[AND{wldr(?w0,world ?w), ?x(?w,particular ?x1)} =>
AND{?y(?w,a particular ?y1),
specific_constant_dependant_on_particulars(?w,?x1,?y1)}]};
//(Dd70) SD: Specific Const. Dep.
//included in def (D69)
//(Dd71) GD: Generic Const. Dep.
//(defrelation GD (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (DJ ?w0 ?f ?g)
// (forall (?w ?x ?t)
// (=> (and (WLDR ?w0 ?w)(WORLD ?w)(PARTICULAR ?x)(PARTICULAR ?t) (?f ?w ?x))
// (and (exists (?t1) (and (PARTICULAR ?t1) (PRE ?w ?x ?t1)))
// (=> (and (At ?w ?t) (PRE ?w ?x ?t))
// (exists (?y) (and (PARTICULAR ?y) (?g ?w ?y) (PRE ?w ?y ?t)))
// ))))))
type generic_constant_dependant__GD (world ?w0, universal ?f, universal ?g) :=
AND{disjoint(?w0,?f,?g),
[AND{wldr(?w0,world ?w), ?f(?w,particular ?x)} =>
AND{present_at(?w,?x,a particular ?t1),
[AND{atom(?w,particular ?t), present_at(?w,?x,?t)} =>
AND{?g(?w,a particular ?y), present_at(?w,?x,?t)}]}]};
//(Dd72) D: Constant Dependence
//(defrelation D (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0)
// (or (SD ?w0 ?f ?g) (GD ?w0 ?f ?g))))
type constant_dependant__D (world ?w0, universal ?f, universal ?g) :=
OR{specific_constant_dependant_on_universals(?w0,?f,?g),
generic_constant_dependant(?w0,?f,?g)};
//(Dd73) OD: One-sided Constant Dependence
//(defrelation OD (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (D ?w0 ?f ?g) (not (D ?w0 ?g ?f))))
type one-sided_constant_dependant__OD (world ?w0, universal ?f, universal ?g) :=
OR{constant_dependant(?w0,?f,?g), !constant_dependant(?w0,?g,?f)};
//(Dd74) OSD: One-sided Specific Constant Dependence
//(defrelation OSD (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f)(UNIVERSAL ?g)(WORLD ?w0) (SD ?w0 ?f ?g) (not (D ?w0 ?g ?f))))
type one-sided_specific_constant_dependant__OSD (world ?w0,universal ?f,universal ?g)
:= AND{specific_constant_dependant_on_universals(?w0,?f,?g),
!constant_dependant(?w0,?g,?f)};
//(Dd75) OGD: One-sided Generic Constant Dependence
//(defrelation OGD (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f)(UNIVERSAL ?g)(WORLD ?w0) (GD ?w0 ?f ?g) (not (D ?w0 ?g ?f))))
type one-sided_generic_constant_dependant__OGD (world ?w0,universal ?f,universal ?g)
:= AND{generic_constant_dependant(?w0,?f,?g), !constant_dependant(?w0,?g,?f)};
//(Dd76) MSD: Mutual Specific Constant Dependence
//(defrelation MSD (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (SD ?w0 ?f ?g) (SD ?w0 ?g ?f)))
type mutual_specific_constant_dependant__MSD (world ?w0, universal ?f, universal ?g)
:= AND{specific_constant_dependant_on_universals(?w0,?f,?g),
specific_constant_dependant_on_universals(?w0,?g,?f)};
//(Dd77) MGD: Mutual Generic Constant Dependence
//(defrelation MGD (?w0 ?f ?g) :=
(and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (GD ?w0 ?f ?g) (GD ?w0 ?g ?f)))
type mutual_generic_constant_dependant__MGD (world ?w0, universal ?f, universal ?g)
:= AND{generic_constant_dependant(?w0,?f,?g),
generic_constant_dependant(?w0,?g,?f)};
// Spatial Dependence
//(Dd78) SD_S: Specific Spatial Dependence
//(defrelation SD.S (?w0 ?x ?y) :=
// (or (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y)
// (forall (?w)
// (=> (and (WLDR ?w0 ?w) (WORLD ?w))
// (and (exists (?t ?s) (and (PARTICULAR ?t) (PARTICULAR ?s)
// (PRE ?w ?x ?s ?t)))
// (forall (?t ?s) (=> (and (PARTICULAR ?t) (PARTICULAR ?s)
// (PRE ?w ?x ?s ?t))
// (PRE ?w ?y ?s ?t)))))))
// (and (WORLD ?w0) (UNIVERSAL ?x) (UNIVERSAL ?y) (DJ ?w0 ?x ?y)
// (forall (?w ?x1)
// (=> (and (WLDR ?w0 ?w) (WORLD ?w) (PARTICULAR ?x1) (?x ?w ?x))
// (exists (?y1) (and (PARTICULAR ?y1) (?y ?w ?y1)
// (SD.S ?w ?x1 ?y1))))))))
specific_spatial_dependant__SD.S
> specific_spatial_dependant_on_particulars
specific_spatial_dependant_on_universals;
type specific_spatial_dependant_on_particulars__SD.S
(world ?w0, particular ?x, particular ?y) :=
AND{[wldr(?w0,world ?w) =>
AND{present_in_at(?w,?x,a particular ?s,a particular ?t),
[present_in_at(?w,?x,particular ?s1,particular ?t1) =>
present_in_at(?w,?y,?s1,?t1)]}]};
type specific_spatial_dependant_on_universals__SD.S
(world ?w0, universal ?x, universal ?y) :=
AND{disjoint(?w0,?x,?y),
[AND{wldr(?w0,world ?w), ?x(?w,particular ?x1)} =>
AND{?y(?w,a particular ?y1),
specific_spatial_dependant_on_particulars(?w,?x1,?y1)}]};
//(Dd79) PSD_S: Partial Specific Spatial Dependence
//(defrelation PSD.S (?w0 ?x ?y) :=
// (or (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y)
// (forall (?w)
// (=> (and (WLDR ?w0 ?w) (WORLD ?w))
// (and (exists (?t ?s)
// (and (PARTICULAR ?t) (PARTICULAR ?s) (PRE ?w ?x ?s ?t)))
// (forall (?t ?s)
// (=> (and (PARTICULAR ?t)(PARTICULAR ?s) (PRE ?w ?x ?s ?t))
// (exists (?r) (and (PARTICULAR ?r) (PP ?w ?r ?s)
// (PRE ?w ?y ?r ?t)))))))))
// (and (WORLD ?w0) (UNIVERSAL ?x) (UNIVERSAL ?y) (DJ ?w0 ?x ?y)
// (forall (?w ?x1)
// (=> (and (WLDR ?w0 ?w) (WORLD ?w) (PARTICULAR ?x1) (?x ?w ?x1))
// (exists (?y1) (and (PARTICULAR ?y1) (?y ?w ?y1)
// (PSD.S ?w ?x1 ?y1))))))))
partial_specific_spatial_dependant__PSD.S
> specific_spatial_dependant_on_particulars
specific_spatial_dependant_on_universals;
type partial_specific_spatial_dependant_on_particulars__PSD.S
(world ?w0, particular ?x, particular ?y) :=
AND{[wldr(?w0,world ?w) =>
AND{present_in_at(?w,?x,a particular ?s,a particular ?t),
[present_in_at(?w,?x,particular ?s1,particular ?t1) =>
AND{proper_part(?w,particular ?r,?s), present_in_at(?w,?y,?r,?t1)}]}]};
type partial_specific_spatial_dependant_on_universals__PSD.S
(world ?w0, universal ?x, universal ?y) :=
AND{disjoint(?w0,?x,?y),
[AND{wldr(?w0,world ?w), ?x(?w,particular ?x1)} =>
AND{?y(?w,a particular ?y1),
partial_specific_spatial_dependant_on_particulars(?w,?x1,?y1)}]};
//(Dd80) P-1SD_S: Inverse Partial Specific Spatial Dependence
//(defrelation P1SD.S (?w0 ?x ?y) :=
// (or (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y)
// (forall (?w)
// (=> (and (WLDR ?w0 ?w) (WORLD ?w))
// (and (exists (?t ?s)
// (and (PARTICULAR ?t) (PARTICULAR ?s) (PRE ?w ?x ?s ?t)))
// (forall (?t ?s)
// (=> (and (PARTICULAR ?t) (PARTICULAR ?s) (PRE ?w ?x ?s ?t))
// (exists (?r) (and (PARTICULAR ?r) (PP ?w ?s ?r)
// (PRE ?w ?y ?r ?t)))))))))
// (and (WORLD ?w0) (UNIVERSAL ?x) (UNIVERSAL ?y) (DJ ?w0 ?x ?y)
// (forall (?w ?x1)
// (=> (and (WLDR ?w0 ?w) (WORLD ?w) (PARTICULAR ?x1) (?x ?w ?x1))
// (exists (?y1)
// (and (PARTICULAR ?y1) (?y ?w ?y1) (P1SD.S ?w ?x1 ?y1))))))))
inverse_partial_specific_spatial_dependant__P1SD.S
> inverse_specific_spatial_dependant_on_particulars
inverse_specific_spatial_dependant_on_universals;
inverse_partial_specific_spatial_dependant_on_particulars__P1SD.S
< partial_specific_spatial_dependant_on_particulars;
type inverse_partial_specific_spatial_dependant_on_universals__P1SD.S
(world ?w0, universal ?x, universal ?y) :=
AND{disjoint(?w0,?x,?y),
[AND{wldr(?w0,world ?w), ?x(?w,particular ?x1)} =>
AND{?y(?w,a particular ?y1),
inverse_partial_specific_spatial_dependant_on_particulars(?w,?x1,?y1)}]};
//(Dd81) SD_S
//included in def D78)
//(Dd82) PSD_S
//included in def D79)
//(Dd83) P-1SD_S
//included in def D80)
//(Dd84) GD_S: Generic Spatial Dependence
//(defrelation GD.S (?w0 ?f ?g) :=
// (and (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (DJ ?w0 ?f ?g)
// (forall (?w ?x ?s ?t)
// (=> (and (WLDR ?w0 ?w)(WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?t)
// (PARTICULAR ?s) (?f ?w ?x))
// (and (exists (?t1 ?s1)
// (and (PARTICULAR ?t1) (PARTICULAR ?s1) (PRE ?w ?x ?s1 ?t1)))
// (=> (and (At ?w ?t) (PRE ?w ?x ?s ?t))
// (exists (?y)
// (and(PARTICULAR ?y)(?g ?w ?y)(PRE ?w ?y ?s ?t)))))))))
type generic_spatial_dependant__GD.S (world ?w0, universal ?f, universal ?g) :=
AND{disjoint(?w0,?f,?g),
[AND{wldr(?w0,world ?w), ?f(?w,particular ?x)} =>
AND{present_in_at(?w,?x,particular ?s1,a particular ?t1),
[AND{atom(?w,particular ?t), present_in_at(?w,?x,particular ?s,?t)} =>
AND{?g(?w,a particular ?y), present_in_at(?w,?x,?s,?t)}]}]};
//(Dd85) PGD_S: Partial Generic Spatial Dependence
//(defrelation PGD.S (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (DJ ?w0 ?f ?g)
// (forall (?w ?x ?s ?t)
// (=> (and (WLDR ?w0 ?w) (WORLD ?w) /*pm: here, additional ')' removed */
// (PARTICULAR ?x) (PARTICULAR ?s) (PARTICULAR ?t) (?f ?w ?x))
// (and (exists (?s1 ?t1)
// (and (PRE ?w ?x ?s1 ?t1) (PARTICULAR ?s1) (PARTICULAR ?t1))
// (=> (and (At ?w ?t) (PRE ?w ?x ?s ?t))
// (exists (?y ?u)
// (and (PARTICULAR ?y) (PARTICULAR ?u)
// (?g ?w ?y) (PP ?w ?u ?s) (PRE ?w ?y ?u ?t)))))))))
type partial__generic_spatial_dependant__PGD.S (world ?w0,universal ?f,universal ?g)
:= AND{disjoint(?w0,?f,?g),
[AND{wldr(?w0,world ?w), ?f(?w,particular ?x)} =>
AND{present_in_at(?w,?x,a particular ?s1,a particular ?t1),
[AND{atom(?w,particular ?t), present_in_at(?w,?x,particular ?s,?t)} =>
AND{?g(?w,a particular ?y), proper_part(?w,a particular ?u,?s),
present_in_at(?w,?y,?u,?t)}]}]};
//(Dd86) P-1GD_S: Inverse Partial Generic Spatial Dependence
//(defrelation P1GD.S (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (DJ ?w0 ?f ?g)
// (forall (?w ?x ?s ?t)
// (=> (and (WLDR ?w0 ?w) (WORLD ?w) /*pm: here, additional ')' removed */
// (PARTICULAR ?x) (PARTICULAR ?s) (PARTICULAR ?t) (?f ?w ?x))
// (and (exists (?s1 ?t1)
// (and (PRE ?w ?x ?s1 ?t1) (PARTICULAR ?s1) (PARTICULAR ?t1))
// (=> (and (At ?w ?t) (PRE ?w ?x ?s ?t))
// (exists (?y ?u)
// (and (PARTICULAR ?y) (PARTICULAR ?u)
// (?g ?w ?y) (PP ?w ?s ?u) (PRE ?w ?y ?u ?t)))))))))
type inverse__partial__generic_spatial_dependant__P1GD.S
(world ?w0, universal ?f, universal ?g) :=
AND{disjoint(?w0,?f,?g),
[AND{wldr(?w0,world ?w), ?f(?w,particular ?x)} =>
AND{present_in_at(?w,?x,a particular ?s1,a particular ?t1),
[AND{atom(?w,particular ?t), present_in_at(?w,?x,particular ?s,?t)} =>
AND{?g(?w,a particular ?y), proper_part(?w,?s,a particular ?u),
present_in_at(?w,?y,?u,?t)}]}]};
//(Dd87) DGD_S: Direct Generic Spatial Dependence
//(defrelation DGD.S (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (GD.S ?w0 ?f ?g)
// (not (exists (?h) (and (UNIVERSAL ?h) (GD.S ?w0 ?f ?h) (GD.S ?w0 ?h ?g))))))
type direct_generic_spatial_dependant__DGD.S (world ?w0, universal ?f, universal ?g)
:= AND{generic_spatial_dependant(?w0,?f,?g),
!AND{generic_spatial_dependant(?w0,?f,a universal ?h),
generic_spatial_dependant(?w0,?h,?g)}};
//(Dd88) Sdt_S: Temporary Specific Spatial Dependence
//(defrelation SDt.S (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0)
// (SD.S ?w0 ?x ?y) (PRE ?w0 ?x ?t)))
type temporary_specific_spatial_dependant__SDt.S
(world ?w0, particular ?x, particular ?y, particular ?t) :=
AND{specific_spatial_dependant_on_particulars(?w0,?x,?y),
present_at(?w0,?x,?t)};
//(Dd89) GDt_S: Temp. Gen. Sp. Dep.
//(defrelation GDt.S (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0)
// (exists (?f ?g) (and (UNIVERSAL ?f) (UNIVERSAL ?g) (?f ?w0 ?x) (?g ?w0 ?y)
// (GD.S ?w0 ?f ?g) (~.S.t ?w0 ?x ?y ?t)))))
type temporary_generic_spatial_dependant__GDt.S
(world ?w0, particular ?x, particular ?y, particular ?t) :=
AND{?f(?w0,?x), ?g(?w0,?y),
generic_spatial_dependant(?w0,a particular ?f,a particular ?g),
temporary_spatial_coincidence(?w0,?x,?y,?t)};
//(Dd90) DGDt_S: Temp. Direct Sp. Dep.
//(defrelation DGDt.S (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0)
// (exists (?f ?g) (and (UNIVERSAL ?f) (UNIVERSAL ?g) (?f ?w0 ?x) (?g ?w0 ?y)
(DGD.S ?w0 ?f ?g) (~.S.t ?w0 ?x ?y ?t)))))
type temporary_direct_spatial_dependant__DGDt.S
(world ?w0, particular ?x, particular ?y, particular ?t) :=
AND{?f(?w0,?x), ?g(?w0,?y),
direct_generic_spatial_dependant(?w0,a particular ?f,a particular ?g),
temporary_spatial_coincidence(?w0,?x,?y,?t)};
//(Dd91) OSD_S: One-sided Specific Spatial Dependence
//(defrelation OSD.S (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f)(UNIVERSAL ?g)(WORLD ?w0)(SD.S ?w0 ?f ?g) (not (D ?w0 ?g ?f))))
type one-sided_specific_spatial_dependant__OSD.S (world ?w0,universal ?f,universal ?g)
:= AND{specific_spatial_dependant_on_universals(?w0,?f,?g),
!constant_dependant(?w0,?g,?f)};
//(Dd92) OGD_S: One-sided Generic Spatial Dependence
//(defrelation OGD.S (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f)(UNIVERSAL ?g)(WORLD ?w0)(GD.S ?w0 ?f ?g)(not (D ?w0 ?g ?f))))
type one-sided_generic_spatial_dependant__OGD.S (world ?w0,universal ?f,universal ?g)
:= AND{generic_spatial_dependant(?w0,?f,?g), !constant_dependant(?w0,?g,?f)};
//(Dd93) MSD_S: Mutual Specific Spatial Dependence
//(defrelation MSD.S (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (SD.S ?w0 ?f ?g) (SD.S ?w0 ?g ?f)))
type mutual_specific_spatial_dependant__MSD.S (world ?w0, universal ?f, universal ?g)
:= AND{specific_spatial_dependant_on_universals(?w0,?f,?g),
specific_spatial_dependant_on_universals(?w0,?g,?f)};
//(Dd94) MGD_S: Mutual Generic Spatial Dependence
//(defrelation MGD.S (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (GD.S ?w0 ?f ?g) (GD.S ?w0 ?g ?f)))
type mutual_generic_spatial_dependant__MGD.S (world ?w0, universal ?f, universal ?g)
:= AND{generic_spatial_dependant(?w0,?f,?g), generic_spatial_dependant(?w0,?g,?f)};
// Constitution
//(Dd95) DK: Direct Constitution
//(defrelation DK (?w0 ?x ?y ?t) :=
// (and (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t) (WORLD ?w0) (K ?w0 ?x ?y ?t)
// (not (exists (?z) (and (PARTICULAR ?z) (K ?w0 ?x ?z ?t) (K ?w0 ?z ?y ?t))))))
type direct_constitution__DK (world ?w0, universal ?x, universal ?y, universal ?t) :=
AND{constitution(?w0,?x,?y,?t),
!AND{constitution(?w0,?x,a particular ?z,?t),constitution(?w0,?z,?y,?t)}};
//(Dd96) SK: Constantly Specifically Constituted by
//(defrelation SK (?w0 ?x ?y) :=
// (or (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y)
// (forall (?w)
// (=> (and (WLDR ?w0 ?w) (WORLD ?w))
// (and (exists (?t) (and (PARTICULAR ?t) (PRE ?w ?x ?t))
// (forall (?t) (=> (and (PARTICULAR ?t) (PRE ?w ?x ?t))
// (K ?w ?y ?x ?t))))))))
// (and (UNIVERSAL ?x) (UNIVERSAL ?y) (WORLD ?w0) (DJ ?w0 ?f ?g)
// (forall (?w ?x1)
// (=> (and (WLDR ?w0 ?w) (WORLD ?w) (PARTICULAR ?x1) (?f ?w ?x1))
// (exists(?y1) (and PARTICULAR ?y1)(?y ?w ?y1)(SK ?w ?x1 ?y1))))))))
type constant_specific_constitution__SK (world ?w0, universal ?x, universal ?y) :=
OR{[wldr(?w0,world ?w) =>
AND{present_at(?w,?x,a particular ?t),
[present_at(?w,?x,particular ?t1) => constitution(?w,?y,?x,?t1)]}],
[AND{disjoint(?w0,?x,?y),
[AND{wldr(?w0,world ?w), ?x(w,particular ?x1)} =>
AND{?y(?w,?y1), constant_specific_constitution(?w,?x1,a particular ?y1)}
]}]};
//(Dd97) SK: Constantly Specifically Constituted by
//included in def (D96)
//(Dd98) GK: Constantly Generically Constituted by
//(defrelation GK (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (DJ ?w0 ?f ?g)
// (forall (?w ?x ?t)
// (=> (and (WLDR ?w0 ?w)(WORLD ?w)(PARTICULAR ?x)(PARTICULAR ?t) (?f ?w ?x))
// (and (exists (?t1) (and (PARTICULAR ?t1) (PRE ?w ?x ?t1)))
// (=> (and (At ?w ?t) (PRE ?w ?x ?t))
// (exists (?y)(and (PARTICULAR ?y) (?g ?w ?y) (K ?w ?y ?x ?t))))))
// )))
type constant_generic_constitution__GK (world ?w0, universal ?f, universal ?g) :=
AND{disjoint(?w0,?f,?g),
[AND{wldr(?w0,world ?w), ?f(w,particular ?x)} =>
AND{present_at(?w,?x,a particular ?t1),
[AND{atom(?w,particular ?t), present_at(?w,?x,?t)} =>
AND{?g(?w,a particular ?y), constitution(?w,?y,?x,?t)}]}]};
//(Dd99) K__Constituted by
//(defrelation K (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0)
// (or (SK ?w0 ?f ?g) (GK ?w0 ?f ?g))))
type constituted_by__K (world ?w0, universal ?f, universal ?g) :=
OR{constant_specific_constitution(?w0,?f,?g),
constant_generic_constitution(?w0,?f,?g)};
//(Dd100) OSK: One-sided Cons. Specif. Const. by
//(defrelation OSK (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0)
// (SK ?w0 ?f ?g) (not (K ?w0 ?g ?f))))
type one-sided_constant_specific_constitution__OSK
(world ?w0, universal ?f, universal ?g)
:= AND{constant_specific_constitution(?w0,?f,?g), !constituted_by(?w0,?g,?f)};
//(Dd101) OGK: One-sided Cons. Generic. Const. by
//(defrelation OGK (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (GK ?w0 ?f ?g) (not (K ?w0 ?g ?f))))
type one-sided_constant_generic_constitution__OGK
(world ?w0, universal ?f, universal ?g)
:= AND{constant_generic_constitution(?w0,?f,?g), !constituted_by(?w0,?g,?f)};
//(Dd102) MSK: Mutual Specific Constitution
//(defrelation MSK (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (SK ?w0 ?f ?g) (SK ?w0 ?g ?f)))
type mutual_specific_constitution__MGK (world ?w0, universal ?f, universal ?g) :=
AND{constant_specific_constitution(?w0,?f,?g),
constant_specific_constitution(?w0,?g,?f)};
//(Dd103) MGK: Mutual Generic Constitution
//(defrelation MSK (?w0 ?f ?g) :=
// (and (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (GK ?w0 ?f ?g) (GK ?w0 ?g ?f)))
type mutual_generic_constitution__MSK (world ?w0, universal ?f, universal ?g) :=
AND{constant_generic_constitution(?w0,?f,?g),
constant_generic_constitution(?w0,?g,?f)};
// Characterization of functions and relations
// Parthood, Argument Restrictions
//(Ad1)
//(forall (?w0 ?x ?y)
// (=> (and (P ?w0 ?x ?y) (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y))
// (and (or (AB ?w0 ?x) (PD ?w0 ?x)) (or (AB ?w0 ?y) (PD ?w0 ?y)))))
[part(world ?w0,particular ?x,particular ?y) =>
AND{ OR{abstract(?w0,?x), perdurant(?w0,?x)},
OR{abstract(?w0,?y), perdurant(?w0,?y)}];
//(Ad2)
//(forall (?w0 ?x ?y)
// (=> (and (P ?w0 ?x ?y) (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y))
// (<=> (PD ?w0 ?x) (PD ?w0 ?y))))
[part(world ?w0,particular ?x,particular ?y) =>
[perdurant(?w0,?x) <=> perdurant(?w0,?y)];
//(Ad3)
//(forall (?w0 ?x ?y) (=> (and(P ?w0 ?x ?y)(WORLD ?w0)(PARTICULAR ?x)(PARTICULAR ?y))
// (<=> (AB ?w0 ?x) (AB ?w0 ?y))))
[part(world ?w0,particular ?x,particular ?y) =>
[abstract(?w0,?x) <=> abstract(?w0,?y)];
//(Ad4)
//(forall (?w0 ?x ?y ?f)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (UNIVERSAL ?f)
// (P ?w0 ?x ?y) (SB ?w0 R ?f) (X ?f))
// (<=> (?f ?w0 ?x) (?f ?w0 ?y))))
[AND{part(world ?w0,particular ?x,particular ?y), subsumes(?w0,region,X ?f)} =>
[?f(?w0,?x) <=> ?f(?w0,?y)];
// Ground Axioms
//(Ad5)
//(forall (?w0 ?x) (=> (and (WORLD ?w0) (PARTICULAR ?x) (or (AB ?w0 ?x) (PD ?w0 ?x)))
// (P ?w0 ?x ?x)))
[OR{abstract(world ?w0,particular ?x), perdurant(?w0,?x)} => part(world ?w0,?x,?y)];
//(Ad6)
//(forall (?w0 ?x ?y)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (P ?w0 ?x ?y) (P ?w0 ?y ?x))
// (= ?x ?y)))
[AND{part(world ?w0,particular ?x,particular ?y), part(?w0,?y,?x)} =>
[?x = ?y] ];
//(Ad7)
//(forall (?w0 ?x ?y ?z)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?z)
// (P ?w0 ?x ?y) (P ?w0 ?y ?z))
// (P ?w0 ?x ?z)))
[AND{part(world ?w0,particular ?x,particular ?y), part(?w0,?y,particular ?z)} =>
part(?w0,?x,?z)];
//(Ad8)
//(forall (?w0 ?x ?y)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y)
// (or (AB ?w0 ?x) (PD ?w0 ?x)) (not (P ?w0 ?x ?y)))
// (exists (?z) (and (PARTICULAR ?x)
// (P ?w0 ?z ?x) (not (O ?w0 ?z ?y))))))
[OR{abstract(world ?w0,particular ?x), perdurant(?w0,?x), !part(?w0,?x,particular ?y)}
=> AND{part(?w0,a particular ?z,?x), !overlap(?w0,?z,?y)};
//(Ad9)
// Note: this version in KIF consider only the universal explicitly listed
//[see comment on (D19)]
//(forall (?w0 ?f)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f)
// (exists (?x) (and (PARTICULAR ?x) (?f ?w0 ?x)))
// (or (forall (?x) (=> (and (PARTICULAR ?x) (?f ?w0 ?x)) (AB ?w0 ?x)))
// (forall (?x) (=> (and (PARTICULAR ?x) (?f ?w0 ?x)) (PD ?w0 ?x)))))
// (exists (?y) (and (PARTICULAR ?y) (sigma ?w0 ?f ?y)))))
[AND{universal ?f, ?f(world ?w0,a particular ?x),
OR{[?f(?w0,?x1) => abstract(?w0,?x1)], [?f(?w0,?x2) => perdurant(?w0,?x2)]}}
=> sigma(?w0,?f(a particular ?y))];
// Temporary Parthood //pm: see (ND7)
// Argument restrictions
//(Ad10)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (P ?w0 ?x ?y ?t))
// (and (ED ?w0 ?x) (ED ?w0 ?y) (T ?w0 ?t))))
[temporary_part(world ?w0,particular ?x,particular ?y,particular ?t) =>
AND{endurant(?w0,?x), endurant(?w0,?y), time_interval(?w0,?t)}];
//(Ad11)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (P ?w0 ?x ?y ?t))
// (<=> (PED ?w0 ?x) (PED ?w0 ?y))))
[temporary_part(world ?w0,particular ?x,particular ?y,particular ?t) =>
AND{physical_endurant(?w0,?x), physical_endurant(?w0,?y)}];
//(Ad12)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (P ?w0 ?x ?y ?t))
// (<=> (NPED ?w0 ?x) (NPED ?w0 ?y))))
[temporary_part(world ?w0,particular ?x,particular ?y,particular ?t) =>
AND{non-physical_endurant(?w0,?x), non-physical_endurant(?w0,?y)}];
// Ground Axioms
//(Ad13)
//(forall (?w0 ?x ?y ?z ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x)(PARTICULAR ?y)(PARTICULAR ?z) (PARTICULAR ?t)
// (P ?w0 ?x ?y ?t) (P ?w0 ?y ?z ?t))
// (P ?w0 ?x ?z ?t)))
[AND{temporary_part(world ?w0,particular ?x,particular ?y,particular ?t),
temporary_part(?w0,?y,particular ?z,?t)} => temporary_part(?w0,?x,?z,?t)];
//(Ad14)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (ED ?w0 ?x) (ED ?w0 ?y) (PRE ?w0 ?x ?t) (PRE ?w0 ?y ?t)
// (not (P ?w0 ?x ?y ?t)))
// (exists(?z)(and (PARTICULAR ?z) (P ?w0 ?z ?x ?t) (not (O ?w0 ?z ?y ?t))))))
[AND{endurant(world ?w0,particular ?x), endurant(?w0,particular ?y),
present_at(?w0,?x,particular ?t), present_at(?w0,?y,?t),
!temporary_part(?w0,?x,?y,?t)}
=> [AND{temporary_part(?w0,a particular ?z,?x,?t), !overlap(?w0,?z,?y,?t)}] ];
//(Ad15) [see comment on (D19)]
//(forall (?w0 ?f)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f)
// (exists (?x) (and (PARTICULAR ?x) (?f ?w0 ?x)))
// (forall (?x) (=> (and (PARTICULAR ?x)(?f ?w0 ?x)) (ED ?w0 ?x))))
// (exists (?y) (and (PARTICULAR ?y) (sigma.t ?w0 ?f ?y)))))
[AND{universal ?f, ?f(world ?w0,a particular),
[?f(?w0,particular ?x) => endurant(?w0,?x)}
=> [sigma.t(?w0,?f(a particular ?y))] ];
// Links With Other Primitives
//(Ad16)
//(forall (?w0 ?x ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?t) (ED ?w0 ?x) (PRE ?w0 ?x ?t))
// (P ?w0 ?x ?x ?t)))
[AND{endurant(world ?w0,particular ?x), present_at(?w0,?x,particular ?t)}
=> temporary_part(?w0,?x,?x,?t)];
//(Ad17)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (P ?w0 ?x ?y ?t))
// (and (PRE ?w0 ?x ?t) (PRE ?w0 ?y ?t))))
[temporary_part(world ?w0,particular ?x,particular ?y,particular ?t)
=> AND{present_at(?w0,?x,?t), present_at(?w0,?y,?t)}];
//(Ad18)
//(forall (?w0 ?x ?y ?t ?u)
// (=> (and (WORLD ?w0) (PARTICULAR ?x)(PARTICULAR ?y)(PARTICULAR ?t)(PARTICULAR ?u)
// (P ?w0 ?x ?y ?t) (P ?w0 ?u ?t))
// (P ?w0 ?x ?y ?u)))
[AND{temporary_part(world ?w0,particular ?x,particular ?y,particular ?t),
part(?w0,particular ?u,?t)} => temporary_part(?w0,?x,?y,?u)];
//(Ad19)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (PED ?w0 ?x) (P ?w0 ?x ?y ?t))
// (incl.S.t ?w0 ?x ?y ?t)))
[AND{physical_endurant(world ?w0,particular ?x),
temporary_part(?w0,particular ?x,particular ?y,particular ?t)}
=> incl.S.t(?w0,?x,?y,?t)];
// Constitution
// Argument restrictions
//(Ad20)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (K ?w0 ?x ?y ?t))
// (and (or (ED ?w0 ?x)(PD ?w0 ?x)) (or (ED ?w0 ?y)(PD ?w0 ?y)) (T ?w0 ?t))))
[constitution(world ?w0,particular ?x,particular ?y,particular ?t)
=> AND{ OR{endurant(?w0,?x), perdurant(?w0,?x)},
OR{endurant(?w0,?y), perdurant(?w0,?y)}, time_interval(?w0,?t)}];
//(Ad21)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (K ?w0 ?x ?y ?t))
// (<=> (PED ?w0 ?x) (PED ?w0 ?y))))
[constitution(world ?w0,particular ?x,particular ?y,particular ?t)
=> [physical_endurant(?w0,?x) <=> physical_endurant(?w0,?y)] ];
//(Ad22)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (K ?w0 ?x ?y ?t))
// (<=> (NPED ?w0 ?x) (NPED ?w0 ?y))))
[constitution(world ?w0,particular ?x,particular ?y,particular ?t)
=> [non-physical_endurant(?w0,?x) <=> non-physical_endurant(?w0,?y)] ];
//(Ad23)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (K ?w0 ?x ?y ?t))
// (<=> (PD ?w0 ?x) (PD ?w0 ?y))))
[constitution(world ?w0,particular ?x,particular ?y,particular ?t)
=> [perdurant(?w0,?x) <=> perdurant(?w0,?y)] ];
// Ground Axioms
//(Ad24)
//(forall (?w0 ?x ?y ?t)
(=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
(K ?w0 ?x ?y ?t))
(not (K ?w0 ?y ?x ?t))))
[constitution(world ?w0,particular ?x,particular ?y,particular ?t)
=> !constitution(?w0,?y,?x,?t)];
//(Ad25)
//(forall (?w0 ?x ?y ?z ?t)
// (=> (and (WORLD ?w0)(PARTICULAR ?x)(PARTICULAR ?y)(PARTICULAR ?z)(PARTICULAR ?t)
// (K ?w0 ?x ?y ?t) (K ?w0 ?y ?z ?t))
// (K ?w0 ?x ?z ?t)))
[AND{constitution(world ?w0,particular ?x,particular ?y,particular ?t),
constitution(?w0,?y,?z,?t)} => constitution(?w0,?x,?z,?t)];
// Links with other Primitives
//(Ad26)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (K ?w0 ?x ?y ?t))
// (and (PRE ?w0 ?x ?t) (PRE ?w0 ?y ?t))))
[constitution(world ?w0,particular ?x,particular ?y,particular ?t),
=> AND{present_at(?w0,?x,?t), present_at(?w0,?y,?t)}];
//(Ad27)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t))
// (<=> (K ?w0 ?x ?y ?t)
// (forall (?u) (=> (and (PARTICULAR ?u) (P ?w0 ?u ?t))
// (K ?w0 ?x ?y ?u))))))
[constitution(world ?w0,particular ?x,particular ?y,particular ?t),
<=> AND{part(?w0,particular ?u,?t), constitution(?w0,?x,?y,?u)}];
//(Ad28)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (PED ?w0 ?x) (K ?w0 ?x ?y ?t))
// (~.S.t ?w0 ?x ?y ?t)))
[AND{physical_endurant(world ?w0,particular ?x),
constitution(?w0,?x,particular ?y,particular ?t)}
=> temporary_spatial_coincidence(?w0,?x,?y,?t)];
//(Ad29)
//(forall (?w0 ?x ?y ?y1 ?t)
// (=> (and (WORLD ?w0)(PARTICULAR ?x)(PARTICULAR ?y)(PARTICULAR ?y1)(PARTICULAR ?t)
// (K ?w0 ?x ?y ?t) (P ?w0 ?y1 ?y ?t))
// (exists (?x1) (and (PARTICULAR ?x1) (P ?w0 ?x1 ?x ?t) (K ?w0 ?x1 ?y1 ?t)))))
[AND{constitution(world ?w0,particular ?x,particular ?y,particular ?t),
temporary_part(?w0,particular ?y1,?y,?t)}
=> AND{temporary_part(?w0,a particular ?x1,?x,?t), constitution(?w0,?x1,?y1,?t)}];
// Links between Categories
//(Ad30)
//(forall (?w0) (=> (WORLD ?w0) (GK ?w0 NAPO M)))
[constant_generic_constitution(world ?w0,non-agentive_physical_object,
amount_of_matter)];
//(Ad31)
//(forall (?w0) (=> (WORLD ?w0) (GK ?w0 APO NAPO)))
[constant_generic_constitution(world ?w0,agentive_physical_object,
non-agentive_physical_object)];
//(Ad32)
//(forall (?w0) (=> (WORLD ?w0) (GK ?w0 SC SAG)))
[constant_generic_constitution(world ?w0,society,social_agent)];
// Participation
// Argument restrictions
//(Ad33)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (PC ?w0 ?x ?y ?t))
// (and (ED ?w0 ?x) (PD ?w0 ?y) (T ?w0 ?t))))
[participant(world ?w0,particular ?x,particular ?y,particular ?t)
=> AND{endurant(?w0,?x), perdurant(?w0,?y), time_interval(?w0,?t)}];
// Existential Axioms
//(a34)
//(forall (?w0 ?x ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?t)
// (PD ?w0 ?x) (PRE ?w0 ?x ?t))
// (exists (?y) (and (PARTICULAR ?y) (PC ?w0 ?y ?x ?t)))))
[present_at(world ?w0,particular ?x,particular ?t)
=> participant(?w0,a particular ?y,?x,?t)];
//(a35)
//(forall (?w0 ?x)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (ED ?w0 ?x))
// (exists (?y ?t) (and (PARTICULAR ?y) (PARTICULAR ?t) (PC ?w0 ?x ?y ?t)))))
[endurant(world ?w0,particular ?x)
=> participant(?w0,?x,a particular ?y,a particular ?t)];
// Links with other Primitives
//(a36)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (PC ?w0 ?x ?y ?t))
// (and (PRE ?w0 ?x ?t) (PRE ?w0 ?y ?t))))
[participant(world ?w0,particular ?x,particular ?y,particular ?t)
=> AND{present_at(?w0,?x,?t), present_at(?w0,?y,?t)}];
//(a37)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t))
// (<=> (PC ?w0 ?x ?y ?t)
// (forall (?u) (=> (and (PARTICULAR ?u) (P ?w0 ?u ?t))
// (PC ?w0 ?x ?y ?u))))))
[participant(world ?w0,particular ?x,particular ?y,particular ?t)
<=> AND{part(?w0,particular ?u,?t), participant(?w0,?x,?y,?u)}];
// Quality
// Argument restrictions:
//(a38)
//(forall (?w0 ?x ?y)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (qt ?w0 ?x ?y))
// (and (Q ?w0 ?x) (or (Q ?w0 ?y) (ED ?w0 ?y) (PD ?w0 ?y)))))
[qt(world ?w0,particular ?x,particular ?y)
=> AND{quality(?w0,?x), OR{quality(?w0,?y),endurant(?w0,?y),perdurant(?w0,?y)}}];
//(a39)
//(forall (?w0 ?x ?y)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (qt ?w0 ?x ?y))
// (<=> (TQ ?w0 ?x) (or (TQ ?w0 ?y) (PD ?w0 ?y)))))
[qt(world ?w0,particular ?x,particular ?y)
=> [temporal_quality(?w0,?x) <=> OR{temporal_quality(?w0,?y),perdurant(?w0,?y)}] ];
//(a40)
//(forall (?w0 ?x ?y)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (qt ?w0 ?x ?y))
// (<=> (PQ ?w0 ?x) (or (PQ ?w0 ?y) (PED ?w0 ?y)))))
[qt(world ?w0,particular ?x,particular ?y)
=> [physical_quality(?w0,?x) <=>
OR{physical_quality(?w0,?y),physical_endurant(?w0,?y)}] ];
//(a41)
//(forall (?w0 ?x ?y)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (qt ?w0 ?x ?y))
// (<=> (AQ ?w0 ?x) (or (AQ ?w0 ?y) (NPED ?w0 ?y)))))
[qt(world ?w0,particular ?x,particular ?y)
=> [abstract_quality(?w0,?x) <=>
OR{abstract_quality(?w0,?y),non-physical_endurant(?w0,?y)}] ];
// Ground Axioms:
//(a42)
//(forall (?w0 ?x ?y ?z)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?z)
// (qt ?w0 ?x ?y) (qt ?w0 ?y ?z))
// (qt ?w0 ?x ?z)))
[AND{qt(world ?w0,particular ?x,particular ?y), qt(?w0,?y,particular ?z)
=> qt(?w0,?x,?z)];
//(a43)
//(forall (?w0 ?x ?y ?z)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?z)
// (qt ?w0 ?x ?y) (qt ?w0 ?x ?z))
// (= ?y ?z)))
[AND{qt(world ?w0,particular ?x,particular ?y), qt(?w0,?x,particular ?z)
=> [?y = ?z] ];
//(a44)
//(forall (?w0 ?f ?x ?y ?z)
// (=> (and (WORLD ?w0)
// (UNIVERSAL ?f) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?z)
// (qtf ?w0 ?f ?x ?y) (qtf ?w0 ?f ?z ?y))
// (= ?x ?z)))
[AND{universal ?f, qtf(world ?w0,?f(particular ?x,particular ?y)),
qtf(?w0,?f(particular ?z,?y))} => [?x = ?z] ];
//(a45)
//(forall (?w0 ?f ?g ?x ?y ?z)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f)
// (UNIVERSAL ?g) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?z)
// (qtf ?w0 ?f ?x ?y) (qtf ?w0 ?g ?y ?z))
// (DJ ?w0 ?f ?g)))
[AND{universal ?f, qtf(world ?w0,?f(particular ?x,particular ?y)),
qtf(?w0,?g(particular ?y,particular ?z))}
=> disjoint(?w0,?f,?g)];
// Existential Axioms:
//(a46)
//(forall (?w0 ?x)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (TQ ?w0 ?x))
// (exists (?y)
// (and (PARTICULAR ?y) (qt ?w0 ?x ?y) (PD ?w0 ?y)
// (forall (?z) (=> (and (PARTICULAR ?z) (qt ?w0 ?x ?z) (PD ?w0 ?z))
// (= ?z ?y)))))))
[temporal_quality(world ?w0,particular ?x)
=> AND{qt(?w0,?x,a particular ?y), perdurant(?w0,?y),
[AND{qt(?w0,?x,particular ?z), perdurant(?w0,?z)} => [?z = ?y]]
}];
//(a47)
//(forall (?w0 ?x)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PQ ?w0 ?x))
// (exists (?y)
// (and (PARTICULAR ?y) (qt ?w0 ?x ?y) (PED ?w0 ?y)
// (forall (?z) (=> (and (PARTICULAR ?z) (qt ?w0 ?x ?z) (PED ?w0 ?z))
// (= ?z ?y)))))))
[physical_quality(world ?w0,particular ?x)
=> AND{qt(world ?w0,?x,a particular ?y), physical_endurant(?w0,?y),
[AND{qt(?w0,?x,particular ?z), physical_endurant(?w0,?z)} => [?z = ?y]]
}];
//(a48)
//(forall (?w0 ?x)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (AQ ?w0 ?x))
// (exists (?y)
// (and (PARTICULAR ?y) (qt ?w0 ?x ?y) (NPED ?w0 ?y)
// (forall (?z) (=> (and (PARTICULAR ?z) (qt ?w0 ?x ?z) (NPED ?w0 ?z))
// (= ?z ?y)))))))
[abstract_quality(world ?w0,particular ?x)
=> AND{qt(world ?w0,?x,a particular ?y), non-physical_endurant(?w0,?y),
[AND{qt(?w0,?x,particular ?z), non-physical_endurant(?w0,?z)} => [?z = ?y]]
}];
//(a49)
//(forall (?w0 ?x)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PD ?w0 ?x))
// (exists (?y) (and (PARTICULAR ?y) (qtf ?w0 TL ?y ?x)))))
[perdurant(world ?w0,particular ?x)
=> qtf(world ?w0,temporal_location,a particular ?y,?x)];
//(a50)
//(forall (?w0 ?x)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PED ?w0 ?x))
// (exists (?y) (and (PARTICULAR ?y) (qtf ?w0 SL ?y ?x)))))
[physical_endurant(world ?w0,particular ?x)
=> qtf(world ?w0,spatial_location,a particular ?y,?x)];
//(a51)
//(forall (?w0 ?x)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (NPED ?w0 ?x))
// (exists (?f ?y)
// (and (PARTICULAR ?y) (UNIVERSAL ?f) (SBL ?w0 AQ ?f) (qtf ?w0 ?f ?y ?x)))))
[non-physical_endurant(world ?w0,particular ?x)
=> AND{universal ?f, subsumes_leaf(?w0,abstract_quality,?f), qtf(?w0,?f(y,?x))}];
// Quale
// Immediate Quale
// Argument restrictions:
//(Ad52)
//(forall (?w0 ?x ?y)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (ql ?w0 ?x ?y))
// (and (TR ?w0 ?x) (TQ ?w0 ?y))))
[ql(world ?w0,particular ?x,particular ?y)
=> AND{temporal_region(?w0,?x), temporal_quality(?w0,?y)}];
//(Ad53)
//(forall (?w0 ?x ?y)
// (=> (and (WORLD ?w0)(PARTICULAR ?x)(PARTICULAR ?y) (ql ?w0 ?x ?y) (TL ?w0 ?y))
// (T ?w0 ?x)))
[AND{ql(world ?w0,particular ?x,particular ?y), temporal_location(?w0,?y)}
=> time_interval(?w0,?x)];
// Basic Axioms:
//(Ad54)
//(forall (?w0 ?x ?x1 ?y)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?x1) (PARTICULAR ?y)
// (ql ?w0 ?x ?y) (ql ?w0 ?x1 ?y))
// (= ?x ?x1)))
[AND{ql(world ?w0,particular ?x,particular ?y), ql(?w0,particular ?x1,?y)}
=> [?x = ?x1] ];
// Existential Axioms:
//(Ad55)
//(forall (?w0 ?x)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (TQ ?w0 ?x))
// (exists (?y) (and (PARTICULAR ?y) (ql ?w0 ?y ?x)))))
[temporal_quality(world ?w0,particular ?x) => ql(?w0,a particular ?y,?x)];
//(Ad56)
//(forall (?w0 ?f ?x ?y ?r ?r1)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (PARTICULAR ?x) (PARTICULAR ?y)
// (PARTICULAR ?r) (PARTICULAR ?r1)
// (L.X ?w0 ?f) (?f ?w0 ?x) (?f ?w0 ?y) (ql ?w0 ?r ?x) (ql ?w0 ?r1 ?y))
// (exists (?g) (and (UNIVERSAL ?g) (L.X ?w0 ?g) (?g ?w0 ?r) (?g ?w0 ?r1)))))
[AND{universal ?f, L.X(world ?w0,?f), ?f(?w0,particular ?x), ?f(?w0,particular ?y),
ql(?w0,particular ?r,?x), ql(?w0,particular ?r1,?y)}
=> AND{L.X(?w0,a universal ?g), ?g(?w0,?r), ?g(?w0,?r1)}];
//(Ad57)
//(forall (?w0 ?f ?x ?y ?r ?r1)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (PARTICULAR ?x) (PARTICULAR ?y)
// (PARTICULAR ?r) (PARTICULAR ?r1) (L.X ?w0 ?f)
// (?f ?w0 ?x) (not (?f ?w0 ?y)) (ql ?w0 ?r ?x) (ql ?w0 ?r1 ?y))
// (not (exists (?g)
// (and (UNIVERSAL ?g) (L.X ?w0 ?g) (?g ?w0 ?r) (?g ?w0 ?r1))))))
[AND{universal ?f, L.X(world ?w0,?f), ?f(?w0,particular ?x), ! ?f(?w0,particular ?y),
ql(?w0,particular ?r,?x), ql(?w0,particular ?r1,?y)}
=> !AND{L.X(?w0,a universal ?g), ?g(?w0,?r), ?g(?w0,?r1)}];
// Temporary Quale
// Argument restrictions:
//(Ad58)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (ql ?w0 ?x ?y ?t))
// (and (or (PR ?w0 ?x)(AR ?w0 ?x)) (or (PQ ?w0 ?y)(AQ ?w0 ?y)) (T ?w0 ?t))))
[temporary_quale(world ?w0,particular ?x,particular ?y,particular ?t)
=> AND{ OR{physical_region(?w0,?x), abstract_region(?w0,?x)},
OR{physical_quality(?w0,?y), abstract_quality(?w0,?y)},
time_interval(?w0,?t)}];
//(Ad59)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (ql ?w0 ?x ?y ?t))
// (<=> (PR ?w0 ?x) (PQ ?w0 ?y))))
[temporary_quale(world ?w0,particular ?x,particular ?y,particular ?t)
=> AND{physical_region(?w0,?x), physical_quality(?w0,?y)}];
//(Ad60)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (ql ?w0 ?x ?y ?t))
// (<=> (AR ?w0 ?x) (AQ ?w0 ?y))))
[temporary_quale(world ?w0,particular ?x,particular ?y,particular ?t)
=> AND{abstract_region(?w0,?x), abstract_quality(?w0,?y)}];
//(Ad61)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (ql ?w0 ?x ?y ?t) (SL ?w0 ?y))
// (S ?w0 ?x)))
[AND{temporary_quale(world ?w0,particular ?x,particular ?y,particular ?t),
spatial_location(?w0,?y)} => space_region(?w0,?x)];
// Existential Axioms: //pm: ?t quantification + (PARTICULAR ?t) missing?
//(Ad62)
//(forall (?w0 ?x)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (or(PQ ?w0 ?x)(AQ ?w0 ?x)) (PRE ?w0 ?x ?t))
// (exists (?y) (and (PARTICULAR ?y) (ql ?w0 ?y ?x ?t)))))
[AND{ OR{physical_quality(world ?w0,particular ?x), abstract_quality(?w0,?x)},
present_at(?w0,?x,particular ?t)}
=> temporary_quale(?w0,a particular ?y,?x,?t)];
//(Ad63)
//(forall (?w0 ?f ?x ?y ?r ?r1 ?t)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (PARTICULAR ?x) (PARTICULAR ?y)
// (PARTICULAR ?r) (PARTICULAR ?r1) (PARTICULAR ?t) (L.X ?w0 ?f)
// (?f ?w0 ?x) (?f ?w0 ?y) (ql ?w0 ?r ?x ?t) (ql ?w0 ?r1 ?y ?t))
// (exists (?g) (and (UNIVERSAL ?g) (L.X ?w0 ?g) (?g ?w0 ?r) (?g ?w0 ?r1)))))
[AND{universal ?f, L.X(world ?w0,?f), ?f(?w0,particular ?x), ?f(?w0,particular ?y),
temporary_quale(?w0,particular ?r,?x,?t),
temporary_quale(?w0,particular ?r1,?y,?t)}
=> AND{L.X(?w0,a universal ?g), ?g(?w0,?r), ?g(?w0,?r1)}];
//(Ad64)
//(forall (?w0 ?f ?x ?y ?r ?r1 ?t)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (PARTICULAR ?x) (PARTICULAR ?y)
// (PARTICULAR ?r) (PARTICULAR ?r1) (PARTICULAR ?t) (L.X ?w0 ?f)
// (?f ?w0 ?x) (not (?f ?w0 ?y)) (ql ?w0 ?r ?x ?t) (ql ?w0 ?r1 ?y ?t))
// (not (exists (?g)
// (and (UNIVERSAL ?g) (L.X ?w0 ?g) (?g ?w0 ?r) (?g ?w0 ?r1))))))
[AND{universal ?f, L.X(world ?w0,?f), ?f(?w0,particular ?x), ! ?f(?w0,particular ?y),
temporary_quale(?w0,particular ?r,?x,?t),
temporary_quale(?w0,particular ?r1,?y,?t)}
=> !AND{L.X(?w0,a universal ?g), ?g(?w0,?r), ?g(?w0,?r1)}];
// Link with Parthood and extension:
//(Ad65)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (ql ?w0 ?x ?y ?t))
// (PRE ?w0 ?y ?t)))
[temporary_quale(world ?w0,particular ?x,particular ?y,particular ?t)
=> present_at(?w0,?y,?t)];
//(Ad66)
//(forall (?w0 ?x ?y ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t))
// (<=> (ql ?w0 ?x ?y ?t)
// (forall (?u) (=> (and (PARTICULAR ?u) (P ?w0 ?u ?t))
// (ql ?w0 ?x ?y ?u))))))
[temporary_quale(world ?w0,particular ?x,particular ?y,particular ?t)
=> AND{part(?w0,particular ?u,?t), temporary_quale(?w0,?x,?y,?u)}];
// Dependence and Spatial Dependence
// Links between categories
//(Ad67)
//(forall (?w0) (=> (WORLD ?w0) (MSD ?w0 TQ PD)))
[mutual_specific_constant_dependant(world ?w0,temporal_quality perdurant)];
//(Ad68)
//(forall (?w0) (=> (WORLD ?w0) (MSD.S ?w0 PQ PED)))
[mutual_specific_spatial_dependant(world ?w0,physical_quality,physical_endurant)];
//(Ad69)
//(forall (?w0) (=> (WORLD ?w0) (MSD ?w0 AQ NPED)))
[mutual_specific_constant_dependant(world ?w0,abstract_quality,non-physical_endurant)];
//(Ad70)
//(forall (?w0) (=> (WORLD ?w0) (OGD ?w0 F NAPO)))
[one-sided_generic_constant_dependant(world ?w0,feature,non-agentive_physical_object)];
//(Ad71)
//(forall (?w0) (=> (WORLD ?w0) (OSD ?w0 MOB APO)))
[one-sided_generic_constant_dependant(world ?w0,mental_object,agentive_physical_object)];
//(Ad72)
//(forall (?w0) (=> (WORLD ?w0) (OGD ?w0 SAG APO)))
[one-sided_generic_constant_dependant(world ?w0,social_agent,agentive_physical_object)];
//(Ad73)
//(forall (?w0) (=> (WORLD ?w0) (OGD ?w0 NASO SC)))
[one-sided_generic_constant_dependant(world ?w0,non-agentive_social_object,society)];
//(Ad74)
//(forall (?w0) (=> (WORLD ?w0) (OD ?w0 NPED PED)))
[OD(world ?w0,non-physical_endurant,physical_endurant)];
// Characterization of Categories
// Perdurant
// Conditions on Perdurant's Leaves
//(Ad75)
//(forall (?w0 ?f) (=> (and (WORLD ?w0) (UNIVERSAL ?f) (PSBL ?w0 ACH ?f))
// (and (NEP.S ?w0 ?f) (CM~ ?w0 ?f) (AT ?w0 ?f))))
[properly_subsumes_leaf(world ?w0,achievement,universal ?f)
=> AND{strongly_non-empty_perdurant_class(?w0,?f),
anticumulative_perdurant_class(?w0,?f), atomic_perdurant_class(?w0,?f)}];
//(Ad76)
//(forall (?w0 ?f) (=> (and (WORLD ?w0) (UNIVERSAL ?f) (PSBL ?w0 ACC ?f))
// (and (NEP.S ?w0 ?f) (CM~ ?w0 ?f) (AT~ ?w0 ?f))))
[properly_subsumes_leaf(world ?w0,accomplishment,universal ?f)
=> AND{strongly_non-empty_perdurant_class(?w0,?f),
anticumulative_perdurant_class(?w0,?f),
anti-atomic_perdurant_class(?w0,?f)}];
//(Ad77)
//(forall (?w0 ?f) (=> (and (WORLD ?w0) (UNIVERSAL ?f) (PSBL ?w0 ST ?f))
// (and (NEP.S ?w0 ?f) (CM ?w0 ?f) (HOM ?w0 ?f))))
[properly_subsumes_leaf(world ?w0,state,universal ?f)
=> AND{strongly_non-empty_perdurant_class(?w0,?f),
cumulative_perdurant_class(?w0,?f),
homeomerous_perdurant_class(?w0,?f)}];
//(Ad78)
//(forall (?w0 ?f) (=> (and (WORLD ?w0) (UNIVERSAL ?f) (PSBL ?w0 PRO ?f))
// (and (NEP.S ?w0 ?f) (CM ?w0 ?f) (HOM~ ?w0 ?f))))
[properly_subsumes_leaf(world ?w0,process,universal ?f)
=> AND{strongly_non-empty_perdurant_class(?w0,?f),
cumulative_perdurant_class(?w0,?f),
anti-homeomerous_perdurant_class(?w0,?f)}];
// Existential Axioms
//(Ad79)
//(forall (?w0) (=> (WORLD ?w0) (exists(?f)(and (UNIVERSAL ?f)(PSBL ?w0 ACH ?f)))))
[properly_subsumes_leaf(world ?w0,achievement,a universal ?f)];
//(Ad80)
//(forall (?w0) (=> (WORLD ?w0) (exists(?f)(and (UNIVERSAL ?f)(PSBL ?w0 ACC ?f)))))
[properly_subsumes_leaf(world ?w0,accomplishment,a universal ?f)];
//(Ad81)
//(forall (?w0) (=> (WORLD ?w0) (exists(?f)(and (UNIVERSAL ?f)(PSBL ?w0 ST ?f)))))
[properly_subsumes_leaf(world ?w0,state,a universal ?f)];
//(Ad82)
//(forall (?w0) (=> (WORLD ?w0) (exists(?f)(and(UNIVERSAL ?f)(PSBL ?w0 PRO ?f)))))
[properly_subsumes_leaf(world ?w0,process,a universal ?f)];
// =========================================
//THEOREMS
//General Properties
//(Td1)
//(forall (?w0 ?x ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?t))
// (not (K ?w0 ?x ?x ?t))))
[!constitution(world ?w0,particular ?x,?x,particular ?t)];
//(Td2)
//(forall (?w0 ?f ?g)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (SK ?w0 ?f ?g))
// (SD ?w0 ?f ?g)))
[constant_specific_constitution(world ?w0,universal ?f,universal ?g)
=> specific_constant_dependant(?w0,?f,?g)];
//(Td3)
//(forall (?w0 ?f ?g)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (GK ?w0 ?f ?g))
// (GD ?w0 ?f ?g)))
[constant_generic_constitution(world ?w0,universal ?f,universal ?g)
=> generic_constant_dependant(?w0,?f,?g)];
//(Td4)
//(forall (?w0 ?f ?g ?h)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (UNIVERSAL ?h)
// (SK ?w0 ?f ?g) (SK ?w0 ?g ?h) (DJ ?w0 ?f ?h))
// (SK ?w0 ?f ?h)))
[AND{constant_specific_constitution(world ?w0,universal ?f,universal ?g),
constant_specific_constitution(?w0,?g,universal ?h), disjoint(?w0,?f,?h)}
=> constant_specific_constitution(?w0,?f,?h)];
//(Td5)
//(forall (?w0 ?f ?g ?h)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (UNIVERSAL ?h)
// (GK ?w0 ?f ?g) (GK ?w0 ?g ?h) (DJ ?w0 ?f ?h))
// (GK ?w0 ?f ?h)))
[AND{constant_generic_constitution(world ?w0,universal ?f,universal ?g),
constant_generic_constitution(?w0,?g,universal ?h), disjoint(?w0,?f,?h)}
=> constant_generic_constitution(?w0,?f,?h)];
//Ground Properties
//(Td6)
//(forall (?w0 ?x ?t) (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?t))
// (not (PC ?w0 ?x ?x ?t))))
[!participant(world ?w0,particular ?x,?x,particular ?t)];
//(Td7)
//(forall (?w0 ?x ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)
// (PC ?w0 ?x ?y ?t))
// (not (PC ?w0 ?y ?x ?t))))
[participant(world ?w0,particular ?x,particular ?y,particular ?t)
=> !participant(?w0,?y,?x,?t)];
//(Td8)
//(forall (?w0 ?x) (=> (and (WORLD ?w0) (PARTICULAR ?x))
// (not (qt ?w0 ?x ?x))))
[!qt(world ?w0,particular ?x,?x)];
//General properties
//(Td9)
//(forall (?w0 ?f ?g ?h)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (UNIVERSAL ?h)
// (SD ?w0 ?f ?g) (SD ?w0 ?g ?h) (DJ ?w0 ?f ?h))
// (SD ?w0 ?f ?h)))
[AND{specific_constant_dependant(world ?w0,universal ?f,universal ?g),
specific_constant_dependant(?w0,?g,universal ?h), disjoint(?w0,?f,?h)}
=> specific_constant_dependant(?w0,?f,?h)];
//(Td10)
//(forall (?w0 ?f ?g ?h)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (UNIVERSAL ?h)
// (GD ?w0 ?f ?g) (GD ?w0 ?g ?h) (DJ ?w0 ?f ?h))
// (GD ?w0 ?f ?h)))
[AND{generic_constant_dependant(world ?w0,universal ?f,universal ?g),
generic_constant_dependant(?w0,?g,universal ?h), disjoint(?w0,?f,?h)}
=> generic_constant_dependant(?w0,?f,?h)];
//(Td11)
//(forall (?w0 ?f ?g ?h)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (UNIVERSAL ?h)
// (SD ?w0 ?f ?g) (GD ?w0 ?g ?h) (DJ ?w0 ?f ?h))
// (GD ?w0 ?f ?h)))
[AND{specific_constant_dependant(world ?w0,universal ?f,universal ?g),
generic_constant_dependant(?w0,?g,universal ?h), disjoint(?w0,?f,?h)}
=> generic_constant_dependant(?w0,?f,?h)];
//(Td12)
//(forall (?w0 ?f ?g ?h)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (UNIVERSAL ?h)
// (GD ?w0 ?f ?g) (SD ?w0 ?g ?h) (DJ ?w0 ?f ?h))
// (GD ?w0 ?f ?h)))
[AND{generic_constant_dependant(world ?w0,universal ?f,universal ?g),
specific_constant_dependant(?w0,?g,universal ?h), disjoint(?w0,?f,?h)}
=> generic_constant_dependant(?w0,?f,?h)];
//(Td13)
//(forall (?w0 ?f ?g)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (SD.S ?w0 ?f ?g))
// (SD ?w0 ?f ?g)))
[specific_spatial_dependant(world ?w0,,universal ?f,universal ?g)
=> specific_constant_dependant(?w0,?f,?g)];
//(Td14)
//(forall (?w0 ?f ?g)
// (=> (and (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (GD.S ?w0 ?f ?g))
// (GD ?w0 ?f ?g)))
[generic_spatial_dependant(world ?w0,,universal ?f,universal ?g)
=> generic_constant_dependant(?w0,?f,?g)];
//Being Present
//(Td15)
//(forall (?w0 ?x)
// (=> (and (WORLD ?w0)(PARTICULAR ?x) (or (ED ?w0 ?x)(PD ?w0 ?x)(Q ?w0 ?x)))
// (exists (?t) (and (PARTICULAR ?t) (PRE ?w0 ?x ?t)))))
[OR{endurant(world ?w0,particular ?x), perdurant(?w0,?x), quality(?w0,?x)}
=> present_at(?w0,?x,a particular ?t)];
//(Td16)
//(forall (?w0 ?x ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?t)
// (or (PED ?w0 ?x) (PQ ?w0 ?x)) (PRE ?w0 ?x ?t))
// (exists (?s) (and (PARTICULAR ?s) (PRE ?w0 ?s ?x ?t)))))
[AND{OR{physical_endurant(world ?w0,particular ?x), physical_quality(?w0,?x)},
present_at(?w0,?x,?t)} => present_in_at(?w0,a particular ?s,?x,?t)];
//(Td17)
//(forall (?w0 ?x ?t ?t1)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?t) (PARTICULAR ?t1)
// (PRE ?w0 ?x ?t) (P ?w0 ?t1 ?t))
// (PRE ?w0 ?x ?t1)))
[AND{present_at(world ?w0,particular ?x,particular ?t), part(?w0,particular ?t1,?t)}
=> present_at(?w0,?x,?t1)];
//(Td18)
//(forall (?w0 ?x ?s ?t)
// (=> (and (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?s) (PARTICULAR ?t)
// (PRE ?w0 ?s ?x ?t))
// (PRE ?w0 ?x ?t)))
[present_in_at(world ?w0,particular ?s, particular x,particular ?t)
=> present_at(?w0,?x,?t)];