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;


//(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) :=>

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) :=>

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) :=>

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) :=>

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
//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)))

// (NA14) -- axiom
//(forall (?w ?f) (=> (and (UNIVERSAL ?f) (WORLD ?w))  (NEP ?w ?f)))

[non-empty_universal(world ?w,universal ?f)];


// (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] =>
     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,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,abstract,FACT), subsumes(?w0,abstract,SET),
      subsumes(?w0,region,temporal_region), subsumes(?w0,region,physical_region),
      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)];