API tools faq
paste
Advertisement
logicmoo

Untitled

logicmoo
Feb 7th, 2015
457
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
ZXBasic 71.49 KB | None | 0 0
raw download clone embed print report
  1. ;;; Deliverable D17 (V2.1) in KIF (text format)
  2. ;;; 28 May 03
  3.  
  4. ;THIS IS A TRANSLATION IN KIF (ACCORDING TO THE KIF-DRAFT
  5. ;PROPOSED TO THE AMERICAN NATIONAL STANDARD NCITS.T2/98-004
  6. ;http://logic.stanford.edu/kif/dpans.html) OF THE
  7. ;DELIVERABLE D17 V2.1 of which
  8. ;it should be considered an appendix.
  9. ;FOR aknowldegments, please check the main document D17
  10. ;FOR comments on this version, please contact:
  11. ;stborgo@indiana.edu
  12.  
  13. ;REVIEW INFO
  14. ;CHANGES - COMMENTS
  15. ;(changes in comments OR due TO changes in the Deliverable
  16. ;D17 are NOT reported)
  17.  
  18. ;(D13) changed WORD into WORLD - Typo
  19. ;(NA3)-(NA9) have been dropped - These occur already
  20. ;somewhere ELSE
  21. ;(NA10)-(NA12) are left AS comments - These are guaranteed
  22. ;by def. (ND5)
  23. ;(NA13) has been dropped -  It follows from (NA14) AND (D2)
  24.  
  25.  
  26. ; Basic functions AND relations
  27. ; new non-rigid universals introduced in specialized
  28. ; theories OR in new versions of DOLCE need TO be added in
  29. ; this definition AS new disjunction clauses of
  30. ; form (= ?f ä)
  31. ; (ND1): universals
  32. (defrelation UNIVERSAL (?f) :=
  33.    (OR (X ?f)))
  34.  
  35. ; new rigid universals introduced in new versions of DOLCE
  36. ; (OR by the user) need TO be added in this definition
  37. ; (ND2) rigid universals
  38. (defrelation X (?f) :=
  39.    (OR (= ?f ALL) (= ?f AB) (= ?f R) (= ?f TR) (= ?f T) (= ?f PR) (=
  40. ?f S) (= ?f AR)
  41. (= ?f Q) (= ?f TQ) (= ?f TL) (= ?f PQ) (= ?f SL) (= ?f AQ) (= ?f ED)
  42. (= ?f M) (= ?f
  43. PED) (= ?f F) (= ?f POB) (= ?f APO) (= ?f NAPO) (= ?f NPED) (= ?f
  44. NPOB) (= ?f MOB)
  45. (= ?f SOB) (= ?f ASO) (= ?f SAG) (= ?f SC) (= ?f NASO) (= ?f AS) (=
  46. ?f PD) (= ?f
  47. EV) (= ?f ACH) (= ?f ACC) (= ?f STV) (= ?f ST) (= ?f PRO))))
  48.  
  49.  
  50. ; there are no particulars in this version of DOLCE, any
  51. ; particular has TO be added in this definition, the def.
  52. ; will have form : (OR (= ?x ä) (= ?x ä))
  53. ; (ND3) particulars
  54. (defrelation PARTICULAR(?x) :=
  55.   )
  56.  
  57. ; there are no named worlds in this version of DOLCE, any
  58. ; world has TO be added in this definition, the def. Will
  59. ; have form : (OR (= ?w ä) (= ?w ä))
  60. ; (ND4) worlds
  61. (defrelation WORLD(?w) :=
  62.   )
  63.  
  64. ; (ND5) accessibility relation on worlds
  65. (defrelation WLDR(?w ?v) :=
  66.   (AND (WORLD ?w) (WORLD ?v)))
  67.  
  68. ; (ND6) Parthood
  69. (defrelation P (?w ?x ?y) :=>
  70.   (AND (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y)))
  71.  
  72. ; (ND7) Temporal Parthood
  73. (defrelation P (?w ?x ?y ?t) :=>
  74.   (AND (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)))
  75.  
  76. ; (ND8) Constitution
  77. (defrelation K (?w ?x ?y ?t) :=>
  78.   (AND (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)))
  79.  
  80. ; (ND9) Participation
  81. (defrelation PC (?w ?x ?y ?t) :=>
  82.   (AND (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)))
  83.  
  84. ; (ND10) Quality
  85. (defrelation qt (?w ?x ?y) :=>
  86.   (AND (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y)))
  87.  
  88. ; (ND11) Quale
  89. (defrelation ql (?w ?x ?y) :=>
  90.   (AND (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y)))
  91.  
  92. ; (ND12) Quale (temporal)
  93. (defrelation ql (?w ?x ?y ?t) :=>
  94.   (AND (WORLD ?w) (PARTICULAR ?x) (PARTICULAR ?y) (PARTICULAR ?t)))
  95.  
  96.  
  97. ;*****************************************************
  98.  
  99. ; (NA1) NEW AXIOM: total domain
  100. (forall (?x)
  101.       (OR (PARTICULAR ?x) (UNIVERSAL ?x) (WORLD ?x)))
  102.  
  103. ; (NA2) partition of the domain
  104. (forall (?x)
  105.       (AND (<=> (PARTICULAR ?x)
  106.                 (AND (NOT (UNIVERSAL ?x)) (NOT (WORLD ?x))))
  107.            (<=> (UNIVERSAL ?x)
  108.                 (AND (NOT (PARTICULAR ?x)) (NOT (WORLD ?x))))
  109.            (<=> (WORLD ?x)
  110.                 (AND (NOT (PARTICULAR ?x)) (NOT (UNIVERSAL ?x))))))
  111.  
  112. ; Formal Characterization
  113. ;PRINCIPLES USED IN THE TRANSLATION IN KIF:
  114. ;Modal operators of possibility AND necessity are translated in the standard
  115. ;  way, see FOR instance p516 of Handbook of Logic in AI AND Logic Prog. Vol.4;
  116. ;The indeces of relations are included prefixing a dot (we preserve
  117. the capital OR
  118. ;  lower case distinction)
  119. ;These are the only predicates (with their arity) that DO NOT have
  120. possible worlds
  121. ;  AS arguments:
  122. ;  X_1,PARTICULAR_1,UNIVERSAL_1, =_2
  123.  
  124.  
  125. ;No need FOR Barcan formulas, the domain of particulars turns out TO be unique
  126. ;  in the translation
  127.  
  128. ;WLDR is an equivalence relation (from corrispondence theory, this implies
  129. ;  that WLDR is a relation FOR S5). The axioms (NA10)-(NA12) are NOT necessary
  130. ;  because of our definition of WLDR.
  131. ; (NA10)
  132. ;(forall (?w0) (=> (WORLD ?w0) (WLDR ?w0 ?w0)))
  133. ; (NA11)
  134. ;(forall (?w0 ?w1)
  135. ;    (=> (AND (WLDR ?w0 ?w1) (WORLD ?w0) (WORLD ?w1))
  136. ;        (WLDR ?w1 ?w0)))
  137. ; (NA12)
  138. ;(forall (?w0 ?w1 ?w2)
  139. ;    (=> (AND (WLDR ?w0 ?w1)
  140. ;             (WLDR ?w1 ?w2)
  141. ;             (WORLD ?w0)
  142. ;             (WORLD ?w1)
  143. ;             (WORLD ?w2))
  144. ;        (WLDR ?w0 ?w2)))
  145.  
  146.  
  147. ; ***THE UNIVERSALS ARE NECESSARILY NON-EMPY***-- axiom
  148. ; (NA14) -- axiom
  149. (forall (?w ?f) (=> (AND (UNIVERSAL ?f) (WORLD ?w))
  150.                      (NEP ?w ?f)))
  151.  
  152. ; (NA15) -- axiom
  153. (forall (?w ?f) (=> (AND (UNIVERSAL ?f) (WORLD ?w))
  154.                      (OR (NOT (X ?f)) (RG ?w ?f))))
  155.  
  156. ; (NA16) Instances of PT -- axiom
  157.   (forall (?w0) (=> (WORLD ?w0)
  158.                         (AND (PT ?w0 ALL ED PD Q AB)
  159.                         (PT ?w0 ED PED NPED AS)
  160.                         (PT ?w0 PED M F POB)
  161.                         (PT ?w0 POB APO NAPO)
  162.                         (PT ?w0 NPOB MOB SOB)
  163.                         (PT ?w0 SOB ASO NASO)
  164.                         (PT ?w0 ASO SAG SC)
  165.                         (PT ?w0 PD EV STV)
  166.                         (PT ?w0 EV ACH ACC)
  167.                         (PT ?w0 STV ST PRO)
  168.                         (PT ?w0 Q TQ PQ AQ)
  169.                         (PT ?w0 R TR PR AR))))
  170.  
  171.  
  172. ; (NA17) Instances of SB -- axiom
  173. (forall (?w0)
  174.      (=> (WORLD ?w0)
  175.          (AND (SB ?w0 ALL ED) (SB ?w0 ALL PD) (SB ?w0 ALL Q) (SB ?w0 ALL AB)
  176.               (SB ?w0 ED PED) (SB ?w0 ED NPED) (SB ?w0 ED AS)
  177.               (SB ?w0 PED M) (SB ?w0 PED F) (SB ?w0 PED POB)
  178.               (SB ?w0 POB APO) (SB ?w0 POB NAPO)
  179.               (SB ?w0 NPED NPOB)
  180.               (SB ?w0 NPOB MOB) (SB ?w0 NPOB SOB)
  181.               (SB ?w0 SOB ASO) (SB ?w0 SOB NASO)
  182.               (SB ?w0 ASO SAG) (SB ?w0 ASO SC)
  183.               (SB ?w0 PD EV) (SB ?w0 PD STV)
  184.               (SB ?w0 EV ACH) (SB ?w0 EV ACC)
  185.               (SB ?w0 STV ST) (SB ?w0 STV PRO)
  186.               (SB ?w0 Q TQ) (SB ?w0 Q PQ) (SB ?w0 Q AQ)
  187.               (SB ?w0 TQ TL)
  188.               (SB ?w0 PQ SL)
  189.               (SB ?w0 AB FACT) (SB ?w0 AB SET) (SB ?w0 AB R)
  190.               (SB ?w0 R TR) (SB ?w0 R PR) (SB ?w0 R AR)
  191.               (SB ?w0 TR T)
  192.               (SB ?w0 PR S))))
  193.  
  194. ; (NA18) Existence of sum
  195. (forall (?w0 ?x ?y)
  196.          (=> (AND (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0))
  197.              (exists (?z)
  198.                      (AND (PARTICULAR ?z) (+ ?w0 ?x ?y ?z)))))
  199.  
  200. ; (NA19) Existence of sigma
  201. (forall (?w0 ?f)
  202.          (=> (AND (UNIVERSAL ?f) (WORLD ?w0))
  203.              (exists (?z)
  204.                      (AND (PARTICULAR ?z) (sigma ?w0 ?f ?z)))))
  205.  
  206. ; (NA20) Existence of sum.t
  207. (forall (?w0 ?x ?y)
  208.          (=> (AND (PARTICULAR ?x) (PARTICULAR ?y) (WORLD ?w0))
  209.              (exists (?z)
  210.                      (AND (PARTICULAR ?z) (+.t ?w0 ?x ?y ?z)))))
  211.  
  212. ; (NA21) Existence of sigma.t
  213. (forall (?w0 ?f)
  214.          (=> (AND (UNIVERSAL ?f) (WORLD ?w0))
  215.              (exists (?z)
  216.                      (AND (PARTICULAR ?z) (sigma.t ?w0 ?f ?z)))))
  217.  
  218. ; this could be added in the def. of UNIVERSAL
  219. ;(forall (@f)
  220. ;        (<=> (UNIVERSAL @f)
  221. ;             (exists (?g @h) (AND (UNIVERSAL ?g)
  222. ;                                  (OR (UNIVERSAL @h) (= @h (listof)))
  223. ;                                  (= @f (listof ?g @h))))))
  224.  
  225. ; this could be added in the def. of PARTICULAR
  226. ;(forall (@x)
  227. ;        (<=> (PARTICULAR @x)
  228. ;             (exists (?y @z) (AND (PARTICULAR ?y)
  229. ;                                  (OR (PARTICULAR @z) (= @z (listof)))
  230. ;                                  (= @x (listof ?y @z))))))
  231.  
  232.  
  233. ;********************************************************
  234. ;(D1)  RG: Rigid Universal
  235. (defrelation RG (?w0 ?f) :=
  236.   (AND (UNIVERSAL ?f)
  237.        (WORLD ?w0)
  238.        (forall (?w ?x)
  239.                (=> (AND (WLDR ?w0 ?w) (WORLD ?w) (PARTICULAR ?x))
  240.                    (=> (?f ?w ?x)
  241.                        (forall (?u)
  242.                                (=> (AND (WLDR ?w ?u) (WORLD ?u))
  243.                                    (?f ?u ?x))))))))
  244.  
  245. ;(D2) NEP: Non-Empty Universal
  246. (defrelation NEP (?w0 ?f) :=
  247.   (AND (UNIVERSAL ?f)
  248.        (WORLD ?w0)
  249.        (forall (?w)
  250.                (=> (AND (WLDR ?w0 ?w) (WORLD ?w))
  251.                    (exists (?y)
  252.                            (AND (PARTICULAR ?y) (?f ?w ?y)))))))
  253.  
  254. ;(D3) DJ: Disjoint Universals
  255. (defrelation DJ (?w0 ?f ?g) :=
  256.   (AND (UNIVERSAL ?f)
  257.        (UNIVERSAL ?g)
  258.        (WORLD ?w0)
  259.        (forall (?w ?x)
  260.                (=> (AND (WLDR ?w0 ?w)
  261.                         (WORLD ?w)
  262.                         (PARTICULAR ?x))
  263.                    (NOT (AND (?f ?w ?x) (?g ?w ?x)))))))
  264.  
  265. ;(D4) SB: Subsumption
  266. (defrelation SB (?w0 ?f ?g) :=
  267.   (AND (UNIVERSAL ?f)
  268.        (UNIVERSAL ?g)
  269.        (WORLD ?w0)
  270.        (forall (?w ?x)
  271.                (=> (AND (WLDR ?w0 ?w)
  272.                         (WORLD ?w)
  273.                         (PARTICULAR ?x))
  274.                    (OR (NOT (?g ?w ?x)) (?f ?w ?x))))))
  275.  
  276. ;(D5) EQ: Equal Universals
  277. (defrelation EQ (?w0 ?f ?g) :=
  278.   (AND (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (SB ?w0 ?f ?g) (SB ?w0 ?g ?f)))
  279.  
  280. ;(D6) PSB: Properly Subsuming
  281. (defrelation PSB (?w0 ?f ?g) :=
  282.   (AND (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (SB ?w0 ?f ?g)
  283.        (NOT (SB ?w0 ?f ?g))))
  284.  
  285. ;(D7) L: Leaf Universal
  286. (defrelation L (?w0 ?f) :=
  287.   (AND (UNIVERSAL ?f)
  288.        (WORLD ?w0)
  289.        (forall (?w ?g)
  290.                (=> (AND (WLDR ?w0 ?w)
  291.                         (WORLD ?w)
  292.                         (UNIVERSAL ?g))
  293.                    (OR (NOT (?SB ?w0 ?f ?g)) (EQ ?w0 ?f ?g))))))
  294.  
  295. ;(D8) SBL: Leaf Subsumed by
  296. (defrelation SBL (?w0 ?f ?g) :=
  297.   (AND (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (SB ?w0 ?f ?g) (L ?w0 ?g)))
  298.  
  299. ;(D9) PSBL: Leaf Properly Subsumed by
  300. (defrelation PSBL (?w0 ?f ?g) :=
  301.   (AND (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (PSB ?w0 ?f ?g) (L ?w0 ?g)))
  302.  
  303. ;(D10) L__: Leaf in the set X
  304.   (defrelation L.X (?w0 ?f) :=
  305.   (AND (UNIVERSAL ?f)
  306.        (WORLD ?w0)
  307.        (X ?f)
  308.        (forall (?w ?g)
  309.                (=> (AND (WLDR ?w0 ?w) (WORLD ?w) (UNIVERSAL ?g))
  310.                    (=> (AND (?SB ?w ?f ?g) (X ?g))
  311.                        (EQ ?w ?f ?g))))))
  312.  
  313. ;(D11) SBL__
  314. (defrelation SBL.X (?w0 ?f ?g) :=
  315.   (AND (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (SB ?w0 ?f ?g) (L.X ?w0 ?g)))
  316.  
  317. ;(D12) PSBL__
  318. (defrelation PSBL.X (?w0 ?f ?g) :=
  319.   (AND (UNIVERSAL ?f) (UNIVERSAL ?g) (WORLD ?w0) (PSB ?w0 ?f ?g) (L.X ?w0 ?g)))
  320.  
  321. ; Definition (D13) is left FOR expressivity. In practice it becomes superfluous
  322. ; since the user needs TO give a list of the n-tuple satisfying relation PT in
  323. ; axiom (NA17)
  324. ;(D13) PT: Partition
  325. (defrelation PT (?w0 ?f @g) :=
  326.   (AND (UNIVERSAL ?f)
  327.      (UNIVERSAL @g)
  328.      (WORLD ?w0)
  329.      (NOT (item ?f @g))
  330.      (forall (?h ?k)
  331.            (AND (=> (AND (UNIVERSAL ?h)
  332.                          (UNIVERSAL ?k)
  333.                          (item ?h @g)
  334.                          (item ?k @g)
  335.                          (/= ?h ?k))
  336.                     (DJ ?w0 ?h ?k))
  337.                 (forall (?w ?x)
  338.                      (=> (AND (WLDR ?w0 ?w)
  339.                               (WORLD ?w)
  340.                               (PARTICULAR ?x))
  341.                          (<=> (?f ?w ?x)
  342.                               (exists (?h)
  343.                                    (AND (UNIVERSAL ?h)
  344.                                         (item ?h @g)
  345.                                         (?h ?w ?x))))))))))
  346.  
  347. ; Mereological Definitions
  348. ;(D14) PP: Proper Part
  349. (defrelation PP (?w0 ?x ?y) :=
  350.   (AND (PARTICULAR ?x)
  351.        (PARTICULAR ?y)
  352.        (WORLD ?w0)
  353.        (P ?w0 ?x ?y)
  354.        (NOT (P ?w0 ?y ?x))))
  355.  
  356. ;(D15) O: Overlap
  357. (defrelation O (?w0 ?x ?y) :=
  358.   (AND (PARTICULAR ?x)
  359.        (PARTICULAR ?y)
  360.        (WORLD ?w0)
  361.        (exists (?z) (AND (PARTICULAR ?z)
  362.                          (P ?w0 ?z ?x)
  363.                          (P ?w0 ?z ?y)))))
  364.  
  365. ;(D16) AT: Atom
  366. (defrelation AT (?w0 ?x) :=
  367.   (AND (PARTICULAR ?x)
  368.        (WORLD ?w0)
  369.        (NOT (exists (?y) (AND (PARTICULAR ?y)
  370.                               (PP ?w0 ?y ?x))))))
  371.  
  372. ;(D17) AtP: Atomic Part
  373. (defrelation AtP (?w0 ?x ?y) :=
  374.   (AND (PARTICULAR ?x)
  375.        (PARTICULAR ?y)
  376.        (WORLD ?w0)
  377.        (P ?w0 ?x ?y)
  378.        (AT ?w0 ?x)))
  379.  
  380. ;(D18) __ Binary Sum
  381. (defrelation + (?w0 ?x ?y ?z) :=
  382.   (AND (PARTICULAR ?x)
  383.        (PARTICULAR ?y)
  384.        (PARTICULAR ?z)
  385.        (WORLD ?w0)
  386.        (forall (?u)
  387.                (=> (PARTICULAR ?u)
  388.                    (<=> (O ?w0 ?u ?z)
  389.                         (OR (O ?w0 ?u ?x) (O ?w0 ?u ?y)))))
  390.        (forall (?z1)
  391.                (=> (AND (PARTICULAR ?z1)
  392.                         (forall (?u)
  393.                              (=> (PARTICULAR ?u)
  394.                                  (<=> (O ?w0 ?u ?z1)
  395.                                       (OR (O ?w0 ?u ?x) (O ?w0 ?u ?y))))))
  396.                    (= ?z1 ?z)))))
  397.  
  398. ;(D19) (general) Sum
  399. ; Note: the rendition in KIF is weaker than the corresponding definition  in
  400. ;modal FOL; here ?f has TO be one of the universal introduced explicitly.
  401. ;[A possible way out: use string-variables (@f) TO CODE Boolean
  402. ;combinations of universals.]
  403. (defrelation sigma (?w0 ?f ?z) :=
  404.   (AND (PARTICULAR ?z)
  405.        (UNIVERSAL ?f)
  406.        (WORLD ?w0)
  407.        (forall (?y)
  408.                (=> (PARTICULAR ?y)
  409.                    (<=> (O ?w0 ?y ?z)
  410.                         (exists (?v)
  411.                                 (AND (PARTICULAR ?v)
  412.                                      (?f ?w0 ?v)
  413.                                      (O ?w0 ?y ?v))))))
  414.        (forall (?z1)
  415.            (=> (PARTICULAR ?z1)
  416.                (exists (?y)
  417.                   (AND (PARTICULAR ?y)
  418.                        (=> (<=> (O ?w0 ?y ?z1)
  419.                                 (exists (?v)
  420.                                     (AND (PARTICULAR ?v)
  421.                                          (?f ?w0 ?v)
  422.                                          (O ?w0 ?y ?v)))))
  423.                        (= ?z1 ?z)))))))
  424.  
  425. ;(D20) PP: Temporary Proper Part
  426. (defrelation PP (?w0 ?x ?y ?t) :=
  427.   (AND (PARTICULAR ?x)
  428.        (PARTICULAR ?y)
  429.        (PARTICULAR ?t)
  430.        (WORLD ?w0)
  431.        (P ?w0 ?x ?y ?t)
  432.        (NOT (P ?w0 ?y ?x ?t))))
  433.  
  434. ;(D21) O: Temporary Overlap
  435. (defrelation O (?w0 ?x ?y ?t) :=
  436.   (AND (PARTICULAR ?x)
  437.        (PARTICULAR ?y)
  438.        (PARTICULAR ?t)
  439.        (WORLD ?w0)
  440.        (exists (?z) (AND (PARTICULAR ?z)
  441.                          (P ?w0 ?z ?x ?t)
  442.                          (P ?w0 ?z ?y ?t)))))
  443.  
  444. ;(D22) AT: Temporary Atom
  445. (defrelation AT (?w0 ?x ?t) :=
  446.   (AND (PARTICULAR ?x)
  447.        (PARTICULAR ?t)
  448.        (WORLD ?w0)
  449.        (NOT (exists (?y)
  450.                   (AND (PARTICULAR ?y) (PP ?w0 ?y ?x ?t))))))
  451.  
  452. ;(D23) AtP: Temporary Atomic Part
  453. (defrelation AtP (?w0 ?x ?y ?t) :=
  454.   (AND (PARTICULAR ?x)
  455.        (PARTICULAR ?y)
  456.        (PARTICULAR ?t)
  457.        (WORLD ?w0)
  458.        (P ?w0 ?x ?y ?t)
  459.        (AT ?w0 ?x ?t)))
  460.  
  461. ;(D24) Coincidence
  462. (defrelation =.t (?w0 ?x ?y ?t) :=
  463.   (AND (PARTICULAR ?x)
  464.        (PARTICULAR ?y)
  465.        (PARTICULAR ?t)
  466.        (WORLD ?w0)
  467.        (P ?w0 ?x ?y ?t)
  468.        (P ?w0 ?y ?x ?t)))
  469.  
  470. ;(D25) CP: Constant Part
  471. (defrelation CP (?w0 ?x ?y) :=
  472.   (AND (PARTICULAR ?x)
  473.        (PARTICULAR ?y)
  474.        (WORLD ?w0)
  475.        (exists (?t)
  476.                (AND (PARTICULAR ?t) (PRE ?w0 ?y ?t)))
  477.        (forall (?t)
  478.                (=> (AND (PARTICULAR ?t) (PRE ?w0 ?y ?t))
  479.                    (P ?w0 ?x ?y ?t)))))
  480.  
  481. ;(D26)
  482. (defrelation +.t (?w0 ?x ?y ?z) :=
  483.   (AND (PARTICULAR ?x)
  484.        (PARTICULAR ?y)
  485.        (PARTICULAR ?z)
  486.        (WORLD ?w0)
  487.        (forall (?u ?t)
  488.             (=> (AND (PARTICULAR ?u) (PARTICULAR ?t))
  489.                 (<=> (O ?w0 ?u ?z ?t)
  490.                      (OR (O ?w0 ?u ?x ?t) (O ?w0 ?u ?y ?t)))))
  491.        (forall (?z1 ?t)
  492.             (=> (AND (PARTICULAR ?z1)
  493.                      (PARTICULAR ?t)
  494.                      (forall (?u)
  495.                          (=> (PARTICULAR ?u)
  496.                              (<=> (O ?w0 ?u ?z1 ?t)
  497.                                   (OR (O ?w0 ?u ?x ?t) (O ?w0 ?u ?y ?t))))))
  498.                  (= ?z1 ?z)))))
  499.  
  500. ;(D27)
  501. ; NOTE: this rendition includes only the listed universal, FOR instance,
  502. ; no Boolean combination  of universals is included [see also comment on (D19)]
  503. (defrelation sigma.t (?w0 ?f ?z) :=
  504.   (AND (PARTICULAR ?z)
  505.        (UNIVERSAL ?f)
  506.        (WORLD ?w0)
  507.        (forall (?y ?t)
  508.                (=> (AND (PARTICULAR ?y) (PARTICULAR ?t))
  509.                    (<=> (O ?w0 ?y ?z ?t)
  510.                         (exists (?v)
  511.                                 (AND (PARTICULAR ?v)
  512.                                      (?f ?w0 ?v)
  513.                                      (O ?w0 ?y ?v ?t))))))
  514.        (forall (?z1 ?t)
  515.            (=> (AND (PARTICULAR ?z1) (PARTICULAR ?t))
  516.                (exists (?y)
  517.                   (AND (PARTICULAR ?y)
  518.                        (=> (<=> (O ?w0 ?y ?z1 ?t)
  519.                                 (exists (?v)
  520.                                    (AND (PARTICULAR ?v)
  521.                                         (?f ?w0 ?v)
  522.                                         (O ?w0 ?y ?v ?t))))
  523.                            (= ?z1 ?z))))))))
  524.  
  525. ; Quality
  526. ;(D28) dqt: Direct Quality
  527. (defrelation dqt (?w0 ?x ?y) :=
  528.   (AND (WORLD ?w0)
  529.        (PARTICULAR ?x)
  530.        (PARTICULAR ?y)
  531.        (qt ?w0 ?x ?y)
  532.        (NOT (exists (?z)
  533.                     (AND (PARTICULAR ?z)
  534.                          (qt ?w0 ?x ?z)
  535.                          (qt ?w0 ?z ?y))))))
  536.  
  537. ;(D29) qt: Quality of typeä
  538. (defrelation qtf (?w0 ?f ?x ?y) :=
  539.   (AND (UNIVERSAL ?f)
  540.        (PARTICULAR ?x)
  541.        (PARTICULAR ?y)
  542.        (WORLD ?w0)
  543.        (qt ?w0 ?x ?y)
  544.        (?f ?w0 ?x)
  545.        (SBL.X ?w0 Q ?f)))
  546.  
  547. ; Temporal AND Spatial Quale
  548. ;(D30) ql_T,PD
  549. (defrelation ql.T.PD (?w0 ?t ?x) :=
  550.   (AND (PARTICULAR ?t)
  551.        (PARTICULAR ?x)
  552.        (WORLD ?w0)
  553.        (PD ?w0 ?x)
  554.        (exists (?z) (AND (PARTICULAR ?z)
  555.                          (qtf ?w0 TL ?z ?x)
  556.                          (ql ?w0 ?t ?z)))))
  557.  
  558. ;(D31) ql_T,ED
  559.   (defrelation ql.T.ED (?w0 ?t ?x) :=
  560.   (AND (PARTICULAR ?t)
  561.        (PARTICULAR ?x)
  562.        (WORLD ?w0)
  563.        (ED ?w0 ?x)
  564.        (forall (?u)
  565.             (=> (PARTICULAR ?u)
  566.                 (<=> (O ?w0 ?u ?t)
  567.                      (exists (?v ?y)
  568.                           (AND (PARTICULAR ?v)
  569.                                (PARTICULAR ?y)
  570.                                (PC ?w0 ?x ?y ?v)
  571.                                (O ?w0 ?u ?v))))))
  572.        (forall (?t1)
  573.             (=> (PARTICULAR ?t1)
  574.                 (exists (?u)
  575.                     (AND (PARTICULAR ?u)
  576.                          (=> (<=> (O ?w0 ?u ?t1)
  577.                                   (exists (?v ?y)
  578.                                       (AND (PARTICULAR ?v)
  579.                                            (PARTICULAR ?y)
  580.                                            (PC ?w0 ?x ?y ?v)
  581.                                            (O ?w0 ?u ?v))))
  582.                              (= ?t1 ?t))))))))
  583.  
  584. ;(D32) ql_T,TQ
  585. (defrelation ql.T.TQ (?w0 ?t ?x) :=
  586.   (AND (PARTICULAR ?t)
  587.        (PARTICULAR ?x)
  588.        (WORLD ?w0)
  589.        (TQ ?w0 ?x)
  590.        (exists (?z) (AND (PARTICULAR ?z)
  591.                          (qt ?w0 ?x ?z)
  592.                          (ql.T.PD ?w0 ?t ?z)))))
  593.  
  594. ;(D33) ql_T,PQ_or_AQ
  595. (defrelation ql.T.PQAQ (?w0 ?t ?x) :=
  596.   (AND (PARTICULAR ?t)
  597.        (PARTICULAR ?x)
  598.        (WORLD ?w0)
  599.        (OR (PQ ?w0 ?x) (AQ ?w0 ?x))
  600.        (exists (?z) (AND (PARTICULAR ?z)
  601.                          (qt ?w0 ?x ?z)
  602.                          (ql.T.ED ?w0 ?t ?z)))))
  603.  
  604. ;(D34) ql_T,Q
  605. (defrelation ql.T.Q (?w0 ?t ?x) :=
  606.   (AND (PARTICULAR ?t)
  607.        (PARTICULAR ?x)
  608.        (WORLD ?w0)
  609.        (OR (ql.T.TQ ?w0 ?t ?x)
  610.            (ql.T.PQAQ ?w0 ?t ?x))))
  611.  
  612. ;(D35) ql_T: Temporal Quale
  613. (defrelation ql.T (?w0 ?t ?x) :=
  614.   (AND (PARTICULAR ?t)
  615.        (PARTICULAR ?x)
  616.        (WORLD ?w0)
  617.        (OR (ql.T.ED ?w0 ?t ?x)
  618.            (ql.T.PD ?w0 ?t ?x)
  619.            (ql.T.Q ?w0 ?t ?x))))
  620.  
  621. ;(D36) ql_S,PED
  622. (defrelation ql.S.PED (?w0 ?s ?x ?t) :=
  623.   (AND (PARTICULAR ?s)
  624.        (PARTICULAR ?x)
  625.        (PARTICULAR ?t)
  626.        (WORLD ?w0)
  627.        (PED ?w0 ?x)
  628.        (exists (?z) (AND (PARTICULAR ?z)
  629.                          (qtf ?w0 SL ?z ?x)
  630.                          (ql ?w0 ?s ?z ?t)))))
  631.  
  632. ;(D37) ql_S,PQ
  633. (defrelation ql.S.PQ (?s ?x ?t) :=
  634.   (AND (PARTICULAR ?s)
  635.        (PARTICULAR ?x)
  636.        (PARTICULAR ?t)
  637.        (WORLD ?w0)
  638.        (PQ ?w0 ?x)
  639.        (exists (?z) (AND (PARTICULAR ?z)
  640.                          (qt ?w0 ?x ?z)
  641.                          (ql.S.PED ?w0 ?s ?z ?t)))))
  642.  
  643. ;(D38) ql_S,PD
  644. (defrelation ql.S.PD (?w0 ?s ?x ?t) :=
  645.   (AND (PARTICULAR ?s)
  646.        (PARTICULAR ?x)
  647.        (PARTICULAR ?t)
  648.        (WORLD ?w0)
  649.        (PD ?w0 ?x)
  650.        (exists (?z) (AND (PARTICULAR ?z)
  651.                          (mppc ?w0 ?z ?x)
  652.                          (ql.S.PED ?w0 ?s ?z ?t)))))
  653.  
  654. ;(D39) ql_S: Spatial Quale
  655. (defrelation ql.S (?w0 ?s ?x ?t) :=
  656.   (AND (PARTICULAR ?s)
  657.        (PARTICULAR ?x)
  658.        (PARTICULAR ?t)
  659.        (WORLD ?w0)
  660.        (OR (ql.S.PED ?w0 ?s ?x ?t)
  661.            (ql.S.PQ ?w0 ?s ?x ?t)
  662.            (ql.S.PD ?w0 ?s ?x ?t))))
  663.  
  664. ;Being present
  665. ;(D40) PRE: Being Present AT
  666. (defrelation PRE (?w0 ?x ?t) :=
  667.   (AND (PARTICULAR ?x)
  668.        (PARTICULAR ?t)
  669.        (WORLD ?w0)
  670.        (exists (?u) (AND (PARTICULAR ?u)
  671.                          (ql.T ?w0 ?u ?x)
  672.                          (P ?w0 ?t ?u)))))
  673.  
  674. ;(D41) PRE: Being Present in AT
  675. (defrelation PRE (?w0 ?x ?s ?t) :=
  676.   (AND (PARTICULAR ?x)
  677.        (PARTICULAR ?s)
  678.        (PARTICULAR ?t)
  679.        (WORLD ?w0)
  680.        (PRE ?w0 ?x ?t)
  681.        (exists (?u) (AND (PARTICULAR ?u)
  682.                          (ql.S ?w0 ?u ?x ?t)
  683.                          (P ?w0 ?s ?u)))))
  684.  
  685. ; Inclusion AND Coincidence
  686. ;(D42) Temporal Inclusion
  687. (defrelation incl.T (?w0 ?x ?y) :=
  688.   (AND (PARTICULAR ?x)
  689.        (PARTICULAR ?y)
  690.        (WORLD ?w0)
  691.        (exists (?t ?u) (AND (PARTICULAR ?t)
  692.                             (PARTICULAR ?u)
  693.                             (ql.T ?w0 ?t ?x)
  694.                             (ql.T ?w0 ?u ?y)
  695.                             (P ?w0 ?t ?u)))))
  696.  
  697. ;(D43) Proper Temporal Inclusion
  698. (defrelation sincl.T (?w0 ?x ?y) :=
  699.   (AND (PARTICULAR ?x)
  700.        (PARTICULAR ?y)
  701.        (WORLD ?w0)
  702.        (exists (?t ?u) (AND (PARTICULAR ?t)
  703.                             (PARTICULAR ?u)
  704.                             (ql.T ?w0 ?t ?x)
  705.                             (ql.T ?w0 ?u ?y)
  706.                             (PP ?w0 ?t ?u)))))
  707.  
  708. ;(D44) Temporary Spatial Inclusion
  709. (defrelation incl.S.t (?w0 ?x ?y ?t) :=
  710.   (AND (PARTICULAR ?x)
  711.        (PARTICULAR ?y)
  712.        (PARTICULAR ?t)
  713.        (WORLD ?w0)
  714.        (exists (?s ?r) (AND (PARTICULAR ?s)
  715.                             (PARTICULAR ?r)
  716.                             (ql.S ?w0 ?s ?x ?t)
  717.                             (ql.S ?w0 ?r ?y ?t)
  718.                             (P ?w0 ?s ?r)))))
  719.  
  720. ;(D45) Temp. Proper Sp. Inclusion
  721. (defrelation sincl.S.t (?w0 ?x ?y ?t) :=
  722.   (AND (PARTICULAR ?x)
  723.        (PARTICULAR ?y)
  724.        (PARTICULAR ?t)
  725.        (WORLD ?w0)
  726.        (exists (?s ?r) (AND (PARTICULAR ?s)
  727.                             (PARTICULAR ?r)
  728.                             (ql.S ?w0 ?s ?x ?t)
  729.                             (ql.S ?w0 ?r ?y ?t)
  730.                             (PP ?w0 ?s ?r)))))
  731.  
  732. ;(D46) Spatio-temporal Inclusion
  733. (defrelation incl.S.T (?w0 ?x ?y) :=
  734.   (AND (PARTICULAR ?x)
  735.      (PARTICULAR ?y)
  736.      (WORLD ?w0)
  737.      (exists (?t) (AND (PARTICULAR ?t) (PRE ?w0 ?x ?t)))
  738.      (forall (?t) (=> (AND (PARTICULAR ?t) (PRE ?w0 ?x ?t))
  739.                       (incl.S.t ?w0 ?x ?y ?t)))))
  740.  
  741. ;(D47) Spatio-temp. Incl. during
  742. (defrelation incl.S.T.t (?w0 ?x ?y ?t) :=
  743.   (AND (PARTICULAR ?x)
  744.        (PARTICULAR ?y)
  745.        (PARTICULAR ?t)
  746.        (WORLD ?w0)
  747.        (PRE ?w0 ?x ?t)
  748.        (forall (?u) (=> (AND (PARTICULAR ?u) (AtP ?w0 ?u ?t))
  749.                         (incl.S.t ?w0 ?x ?y ?u)))))
  750.  
  751. ;(D48) Temporal Coincidence
  752. (defrelation ~.T (?w0 ?x ?y) :=
  753.   (AND (PARTICULAR ?x)
  754.        (PARTICULAR ?y)
  755.        (WORLD ?w0)
  756.        (incl.T ?w0 ?x ?y)
  757.        (incl.T ?w0 ?y ?x)))
  758.  
  759. ;(D49) Temporary Spatial Coincidence
  760. (defrelation ~.S.t (?w0 ?x ?y ?t) :=
  761.   (AND (PARTICULAR ?x)
  762.        (PARTICULAR ?y)
  763.        (PARTICULAR ?t)
  764.        (WORLD ?w0)
  765.        (incl.S.t ?w0 ?x ?y ?t)
  766.        (incl.S.t ?w0 ?y ?x ?t)))
  767.  
  768. ;(D50) Spatio-temporal Coincidence
  769. (defrelation ~.S.T (?w0 ?x ?y) :=
  770.   (AND (WORLD ?w0)
  771.        (PARTICULAR ?x)
  772.        (PARTICULAR ?y)
  773.        (incl.S.T ?w0 ?x ?y)
  774.        (incl.S.T ?w0 ?y ?x)))
  775.  
  776. ;(D51) Spatio-temp. Coincidence during
  777. (defrelation ~.S.T.t (?w0 ?x ?y ?t) :=
  778.   (AND (PARTICULAR ?x)
  779.        (PARTICULAR ?y)
  780.        (PARTICULAR ?t)
  781.        (WORLD ?w0)
  782.        (PRE ?w0 ?x ?t)
  783.        (forall (?u) (=> (AND (PARTICULAR ?u) (AtP ?w0 ?u ?t))
  784.                         (~.S.t ?w0 ?x ?y ?u)))))
  785.  
  786. ;(D52) O_T: Temporal Overlap
  787. (defrelation O.T (?w0 ?x ?y) :=
  788.   (AND (PARTICULAR ?x)
  789.        (PARTICULAR ?y)
  790.        (WORLD ?w0)
  791.        (exists (?t ?u) (AND (PARTICULAR ?t)
  792.                             (PARTICULAR ?u)
  793.                             (ql.T ?w0 ?t ?x)
  794.                             (ql.T ?w0 ?u ?y)
  795.                             (O ?w0 ?t ?u)))))
  796.  
  797. ;(D53) O_S,t: Temporary Spatial Overlap
  798. (defrelation O.S.t (?x ?y ?t) :=
  799.   (AND (PARTICULAR ?x)
  800.        (PARTICULAR ?y)
  801.        (PARTICULAR ?t)
  802.        (WORLD ?w0)
  803.        (exists (?s ?r) (AND (PARTICULAR ?s)
  804.                             (PARTICULAR ?r)
  805.                             (ql.S ?w0 ?s ?x ?t)
  806.                             (ql.S ?w0 ?r ?y ?t)
  807.                             (O ?w0 ?s ?r)))))
  808.  
  809. ; Perdurant
  810. ;(D54) P_T: Temporal Part
  811. (defrelation P.T (?w0 ?x ?y) :=
  812.   (AND (PARTICULAR ?x)
  813.        (PARTICULAR ?y)
  814.        (WORLD ?w0)
  815.        (PD ?w0 ?x)
  816.        (P ?w0 ?x ?y)
  817.        (forall (?z) (=> (AND (PARTICULAR ?z)
  818.                              (P ?w0 ?z ?y)
  819.                              (incl.T ?w0 ?z ?x))
  820.                         (P ?w0 ?z ?x)))))
  821.  
  822. ;(D55) P_S: Spatial Part
  823. (defrelation P.S (?w0 ?x ?y) :=
  824.   (AND (PARTICULAR ?x)
  825.        (PARTICULAR ?y)
  826.        (WORLD ?w0)
  827.        (PD ?w0 ?x)
  828.        (P ?w0 ?x ?y)
  829.        (~.T ?w0 ?x ?y)))
  830.  
  831. ;(D56) NEP_S: Strongly Non-Empty
  832. (defrelation NEP.S (?w0 ?f) :=
  833.   (AND (UNIVERSAL ?f)
  834.        (WORLD ?w0)
  835.        (SB ?w0 PD ?f)
  836.        (forall (?w) (=> (AND (WLDR ?w0 ?w) (WORLD ?w))
  837.                         (exists (?x ?y)
  838.                              (AND (PARTICULAR ?x)
  839.                                   (PARTICULAR ?y)
  840.                                   (?f ?w ?x)
  841.                                   (?f ?w ?y)
  842.                                   (NOT (P ?w ?x ?y))
  843.                                   (NOT (P ?w ?y ?x))))))))
  844.  
  845. ;(D57) CM: Cumulative
  846. (defrelation CM (?w0 ?f) :=
  847.   (AND (UNIVERSAL ?f)
  848.        (WORLD ?w0)
  849.        (SB ?w0 PD ?f)
  850.        (forall (?w ?x ?y ?z)
  851.                (=> (AND (WLDR ?w0 ?w)
  852.                         (WORLD ?w)
  853.                         (PARTICULAR ?x)
  854.                         (PARTICULAR ?y)
  855.                         (PARTICULAR ?z)
  856.                         (+ ?w ?x ?y ?z)
  857.                         (?f ?w ?x)
  858.                         (?f ?w ?y))
  859.                    (?f ?w ?z)))))
  860.  
  861. ;(D58) CMó: Anti-Cumulative
  862. (defrelation CM~ (?w0 ?f) :=
  863.   (AND (UNIVERSAL ?f)
  864.        (WORLD ?w0)
  865.        (SB ?w0 PD ?f)
  866.        (forall (?w ?x ?y ?z)
  867.                (=> (AND (WLDR ?w0 ?w)
  868.                         (WORLD ?w)
  869.                         (PARTICULAR ?x)
  870.                         (PARTICULAR ?y)
  871.                         (PARTICULAR ?z)
  872.                         (+ ?w ?x ?y ?z)
  873.                         (?f ?w ?x)
  874.                         (?f ?w ?y)
  875.                         (NOT (P ?w ?x ?y))
  876.                         (NOT (P ?w ?y ?x)))
  877.                    (NOT (?f ?w ?z))))))
  878.  
  879. ;(D59) HOM: Homeomerous
  880. (defrelation HOM (?w0 ?f) :=
  881.   (AND (UNIVERSAL ?f)
  882.        (WORLD ?w0)
  883.        (SB ?w0 PD ?f)
  884.        (forall (?w ?x ?y) (=> (AND (WLDR ?w0 ?w)
  885.                                    (WORLD ?w)
  886.                                    (PARTICULAR ?x)
  887.                                    (PARTICULAR ?y)
  888.                                    (?f ?w ?x)
  889.                                    (P.T ?w ?y ?x))
  890.                                (?f ?w ?y)))))
  891.  
  892. ;(D60) HOMó: Anti-Homeom.
  893. (defrelation HOM~ (?w0 ?f) :=
  894.   (AND (UNIVERSAL ?f)
  895.     (WORLD ?w0)
  896.     (SB ?w0 PD ?f)
  897.     (forall (?w ?x)
  898.             (=> (AND (WLDR ?w0 ?w)
  899.                      (WORLD ?w)
  900.                      (PARTICULAR ?x)
  901.                      (?f ?w ?x))
  902.                 (exists (?y)
  903.                      (AND (PARTICULAR ?y)
  904.                           (P.T ?w ?y ?x)
  905.                           (NOT (?f ?w ?y))))))))
  906.  
  907. ;(D61) AT: Atomic
  908. (defrelation AT (?w0 ?f) :=
  909.   (AND (UNIVERSAL ?f)
  910.        (WORLD ?w0)
  911.        (SB ?w0 PD ?f)
  912.        (forall (?w ?x) (=> (AND (WLDR ?w0 ?w)
  913.                                 (WORLD ?w)
  914.                                 (PARTICULAR ?x)
  915.                                 (?f ?w ?x))
  916.                            (AT ?w ?x)))))
  917.  
  918. ;(D62) ATó: Anti-Atomic
  919. (defrelation AT~ (?w0 ?f) :=
  920.   (AND (UNIVERSAL ?f)
  921.        (WORLD ?w0)
  922.        (SB ?w0 PD ?f)
  923.        (forall (?w ?x) (=> (AND (WLDR ?w0 ?w)
  924.                                 (WORLD ?w)
  925.                                 (PARTICULAR ?x)
  926.                                 (?f ?w ?x))
  927.                            (NOT (AT ?w ?x))))))
  928.  
  929. ;Participation
  930. ;(D63) PC_C: Constant Participation
  931. (defrelation PC.C (?w0 ?x ?y) :=
  932.   (AND (PARTICULAR ?x)
  933.        (PARTICULAR ?y)
  934.        (WORLD ?w0)
  935.        (exists (?t) (AND (PARTICULAR ?t) (PRE ?w0 ?y ?t)))
  936.        (forall (?t) (=> (AND (PARTICULAR ?t)
  937.                              (PRE ?w0 ?y ?t))
  938.                         (PC ?w0 ?x ?y ?t)))))
  939.  
  940. ;(D64) PC_T: Temporary Total Particip.
  941. (defrelation PC.T (?w0 ?x ?y ?t) :=
  942.   (AND (PARTICULAR ?x)
  943.        (PARTICULAR ?y)
  944.        (PARTICULAR ?t)
  945.        (WORLD ?w0)
  946.        (PD ?w0 ?y)
  947.        (forall (?z)
  948.              (=> (AND (PARTICULAR ?z)
  949.                       (P ?w0 ?z ?y)
  950.                       (PRE ?w0 ?z ?t))
  951.                  (PC ?w0 ?x ?z ?t)))))
  952.  
  953. ;(D65) PC_T: Total Participation
  954. (defrelation PC.T (?w0 ?x ?y) :=
  955.   (AND (PARTICULAR ?x)
  956.        (PARTICULAR ?y)
  957.        (WORLD ?w0)
  958.        (exists (?t) (AND (PARTICULAR ?t)
  959.                          (ql.T ?w0 ?t ?y)
  960.                          (PC.T ?w0 ?x ?y ?t)))))
  961.  
  962. ;(D66) mpc: Maximal Participant
  963. (defrelation mpc (?w0 ?x ?y) :=
  964.   (AND (PARTICULAR ?x)
  965.        (PARTICULAR ?y)
  966.        (WORLD ?w0)
  967.        (forall (?z ?t)
  968.                (=> (AND (PARTICULAR ?z) (PARTICULAR ?t))
  969.                    (<=> (O ?w0 ?z ?x ?t)
  970.                         (exists (?v)
  971.                                 (AND (PARTICULAR ?v)
  972.                                      (PC.T ?w0 ?v ?y ?t)
  973.                                      (O ?w0 ?z ?v ?t))))))
  974.        (forall (?z ?x1 ?t)
  975.                (=> (AND (PARTICULAR ?z)
  976.                         (PARTICULAR ?x1)
  977.                         (PARTICULAR ?t)
  978.                         (<=> (O ?w0 ?z ?x1 ?t)
  979.                              (exists (?v)
  980.                                  (AND (PARTICULAR ?v)
  981.                                       (PC.T ?w0 ?v ?y ?t)
  982.                                       (O ?w0 ?z ?v ?t)))))
  983.                    (= ?x1 ?x)))))
  984.  
  985. ;(D67) mppc: Maximal Physical Participant
  986. (defrelation mppc (?w0 ?x ?y) :=
  987.   (AND (PARTICULAR ?x)
  988.        (PARTICULAR ?y)
  989.        (WORLD ?w0)
  990.        (forall (?z ?t)
  991.                (=> (AND (PARTICULAR ?z) (PARTICULAR ?t))
  992.                    (<=> (O ?w0 ?z ?x ?t)
  993.                         (exists (?v)
  994.                                 (AND (PARTICULAR ?v)
  995.                                      (PC.T ?w0 ?v ?y ?t)
  996.                                      (PED ?w0 ?z)
  997.                                      (O ?w0 ?z ?v ?t))))))
  998.        (forall (?z ?x1 ?t)
  999.                (=> (AND (PARTICULAR ?z)
  1000.                         (PARTICULAR ?x1)
  1001.                         (PARTICULAR ?t)
  1002.                         (<=> (O ?w0 ?z ?x1 ?t)
  1003.                              (exists (?v)
  1004.                                  (AND (PARTICULAR ?v)
  1005.                                       (PC.T ?w0 ?v ?y ?t)
  1006.                                       (PED ?w0 ?z)
  1007.                                       (O ?w0 ?z ?v ?t)))))
  1008.                    (= ?x1 ?x)))))
  1009.  
  1010. ;(D68) lf: Life
  1011. (defrelation lf (?w0 ?x ?y) :=
  1012.   (AND (PARTICULAR ?x)
  1013.        (PARTICULAR ?y)
  1014.        (WORLD ?w0)
  1015.        (forall (?z)
  1016.                (=> (PARTICULAR ?z)
  1017.                    (<=> (O ?w0 ?z ?x)
  1018.                         (exists (?v)
  1019.                                 (AND (PARTICULAR ?v)
  1020.                                      (PC.T ?w0 ?y ?v)
  1021.                                      (O ?w0 ?z ?v))))))
  1022.        (forall (?z ?u)
  1023.                (=> (AND (PARTICULAR ?z) (PARTICULAR ?u)
  1024.                         (<=> (O ?w0 ?z ?u)
  1025.                              (exists (?v)
  1026.                                  (AND (PARTICULAR ?v)
  1027.                                       (PC.T ?w0 ?y ?v)
  1028.                                       (O ?w0 ?z ?v)))))
  1029.                    (= ?u ?x)))))
  1030.  
  1031. ; Dependence
  1032. ;(D69) SD: Specific Constant Dep.
  1033. (defrelation SD (?w0 ?x ?y) :=
  1034.   (OR (AND (PARTICULAR ?x)
  1035.            (PARTICULAR ?y)
  1036.            (WORLD ?w0)
  1037.            (forall (?w)
  1038.                (=> (AND (WLDR ?w0 ?w) (WORLD ?w))
  1039.                    (AND (exists (?t)
  1040.                              (AND (PARTICULAR ?t) (PRE ?w ?x ?t)))
  1041.                         (forall (?t)
  1042.                              (=> (AND (PARTICULAR ?t) (PRE ?w ?x ?t))
  1043.                                  (PRE ?w ?y ?t)))))))
  1044.       (AND (UNIVERSAL ?x)
  1045.            (UNIVERSAL ?y)
  1046.            (WORLD ?w0)
  1047.            (DJ ?w0 ?x ?y)
  1048.            (forall (?w ?x1)
  1049.                (=> (AND (WLDR ?w0 ?w)
  1050.                         (WORLD ?w)
  1051.                         (PARTICULAR ?x1)
  1052.                         (?x ?w ?x1))
  1053.                    (exists (?y1) (AND (PARTICULAR ?y1)
  1054.                                       (?y ?w ?y1)
  1055.                                       (SD ?w ?x1 ?y1))))))))
  1056.  
  1057. ;(D70) SD: Specific CONST. Dep.
  1058. ;included in def (D69)
  1059.  
  1060. ;(D71) GD: Generic CONST. Dep.
  1061. (defrelation GD (?w0 ?f ?g) :=
  1062.   (AND (UNIVERSAL ?f)
  1063.        (UNIVERSAL ?g)
  1064.        (WORLD ?w0)
  1065.        (DJ ?w0 ?f ?g)
  1066.        (forall (?w ?x ?t)
  1067.             (=> (AND (WLDR ?w0 ?w)
  1068.                      (WORLD ?w)
  1069.                      (PARTICULAR ?x)
  1070.                      (PARTICULAR ?t)
  1071.                      (?f ?w ?x))
  1072.                 (AND (exists (?t1)
  1073.                          (AND (PARTICULAR ?t1) (PRE ?w ?x ?t1)))
  1074.                      (=> (AND (AT ?w ?t) (PRE ?w ?x ?t))
  1075.                          (exists (?y)
  1076.                                  (AND (PARTICULAR ?y)
  1077.                                       (?g ?w ?y)
  1078.                                       (PRE ?w ?y ?t)))))))))
  1079.  
  1080. ;(D72) D: Constant Dependence
  1081. (defrelation D (?w0 ?f ?g) :=
  1082.   (AND (UNIVERSAL ?f)
  1083.        (UNIVERSAL ?g)
  1084.        (WORLD ?w0)
  1085.        (OR (SD ?w0 ?f ?g) (GD ?w0 ?f ?g))))
  1086.  
  1087. ;(D73) OD: One-sided Constant Dependence
  1088. (defrelation OD (?w0 ?f ?g) :=
  1089.   (AND (UNIVERSAL ?f)
  1090.        (UNIVERSAL ?g)
  1091.        (WORLD ?w0)
  1092.        (D ?w0 ?f ?g)
  1093.        (NOT (D ?w0 ?g ?f))))
  1094.  
  1095. ;(D74) OSD: One-sided Specific Constant Dependence
  1096. (defrelation OSD (?w0 ?f ?g) :=
  1097.   (AND (UNIVERSAL ?f)
  1098.        (UNIVERSAL ?g)
  1099.        (WORLD ?w0)
  1100.        (SD ?w0 ?f ?g)
  1101.        (NOT (D ?w0 ?g ?f))))
  1102.  
  1103. ;(D75) OGD: One-sided Generic Constant Dependence
  1104. (defrelation OGD (?w0 ?f ?g) :=
  1105.   (AND (UNIVERSAL ?f)
  1106.        (UNIVERSAL ?g)
  1107.        (WORLD ?w0)
  1108.        (GD ?w0 ?f ?g)
  1109.        (NOT (D ?w0 ?g ?f))))
  1110.  
  1111. ;(D76) MSD: Mutual Specific Constant Dependence
  1112. (defrelation MSD (?w0 ?f ?g) :=
  1113.   (AND (UNIVERSAL ?f)
  1114.        (UNIVERSAL ?g)
  1115.        (WORLD ?w0)
  1116.        (SD ?w0 ?f ?g)
  1117.        (SD ?w0 ?g ?f)))
  1118.  
  1119. ;(D77) MGD: Mutual Generic Constant Dependence
  1120. (defrelation MGD (?w0 ?f ?g) :=
  1121.   (AND (UNIVERSAL ?f)
  1122.        (UNIVERSAL ?g)
  1123.        (WORLD ?w0)
  1124.        (GD ?w0 ?f ?g)
  1125.        (GD ?w0 ?g ?f)))
  1126.  
  1127. ; Spatial Dependence
  1128. ;(D78) SD_S: Specific Spatial Dependence
  1129. (defrelation SD.S (?w0 ?x ?y) :=
  1130.   (OR (AND (WORLD ?w0)
  1131.            (PARTICULAR ?x)
  1132.            (PARTICULAR ?y)
  1133.            (forall (?w)
  1134.               (=> (AND (WLDR ?w0 ?w) (WORLD ?w))
  1135.                   (AND (exists (?t ?s)
  1136.                                (AND (PARTICULAR ?t)
  1137.                                     (PARTICULAR ?s)
  1138.                                     (PRE ?w ?x ?s ?t)))
  1139.                        (forall (?t ?s)
  1140.                                (=> (AND (PARTICULAR ?t)
  1141.                                         (PARTICULAR ?s)
  1142.                                         (PRE ?w ?x ?s ?t))
  1143.                                    (PRE ?w ?y ?s ?t)))))))
  1144.       (AND (WORLD ?w0)
  1145.            (UNIVERSAL ?x)
  1146.            (UNIVERSAL ?y)
  1147.            (DJ ?w0 ?x ?y)
  1148.            (forall (?w ?x1)
  1149.                  (=> (AND (WLDR ?w0 ?w)
  1150.                           (WORLD ?w)
  1151.                           (PARTICULAR ?x1)
  1152.                           (?x ?w ?x))
  1153.                      (exists (?y1)
  1154.                           (AND (PARTICULAR ?y1)
  1155.                                (?y ?w ?y1)
  1156.                                (SD.S ?w ?x1 ?y1))))))))
  1157.  
  1158. ;(D79) PSD_S: Partial Specific Spatial Dependence
  1159. (defrelation PSD.S (?w0 ?x ?y) :=
  1160.   (OR (AND (WORLD ?w0)
  1161.        (PARTICULAR ?x)
  1162.        (PARTICULAR ?y)
  1163.        (forall (?w)
  1164.           (=> (AND (WLDR ?w0 ?w) (WORLD ?w))
  1165.               (AND (exists (?t ?s)
  1166.                         (AND (PARTICULAR ?t)
  1167.                              (PARTICULAR ?s)
  1168.                              (PRE ?w ?x ?s ?t)))
  1169.                    (forall (?t ?s)
  1170.                        (=> (AND (PARTICULAR ?t)
  1171.                                 (PARTICULAR ?s)
  1172.                                 (PRE ?w ?x ?s ?t))
  1173.                            (exists (?r)
  1174.                                (AND (PARTICULAR ?r)
  1175.                                     (PP ?w ?r ?s)
  1176.                                     (PRE ?w ?y ?r ?t)))))))))
  1177.       (AND (WORLD ?w0)
  1178.            (UNIVERSAL ?x)
  1179.            (UNIVERSAL ?y)
  1180.            (DJ ?w0 ?x ?y)
  1181.            (forall (?w ?x1)
  1182.                  (=> (AND (WLDR ?w0 ?w)
  1183.                           (WORLD ?w)
  1184.                           (PARTICULAR ?x1)
  1185.                           (?x ?w ?x1))
  1186.                      (exists (?y1)
  1187.                           (AND (PARTICULAR ?y1)
  1188.                                (?y ?w ?y1)
  1189.                                (PSD.S ?w ?x1 ?y1))))))))
  1190.  
  1191. ;(D80) P-1SD_S: INVERSE Partial Specific Spatial Dependence
  1192. (defrelation P1SD.S (?w0 ?x ?y) :=
  1193.   (OR (AND (WORLD ?w0)
  1194.         (PARTICULAR ?x)
  1195.         (PARTICULAR ?y)
  1196.         (forall (?w)
  1197.            (=> (AND (WLDR ?w0 ?w) (WORLD ?w))
  1198.                (AND (exists (?t ?s)
  1199.                         (AND (PARTICULAR ?t)
  1200.                              (PARTICULAR ?s)
  1201.                              (PRE ?w ?x ?s ?t)))
  1202.                     (forall (?t ?s)
  1203.                        (=> (AND (PARTICULAR ?t)
  1204.                                 (PARTICULAR ?s)
  1205.                                 (PRE ?w ?x ?s ?t))
  1206.                            (exists (?r)
  1207.                                (AND (PARTICULAR ?r)
  1208.                                     (PP ?w ?s ?r)
  1209.                                     (PRE ?w ?y ?r ?t)))))))))
  1210.       (AND (WORLD ?w0)
  1211.            (UNIVERSAL ?x)
  1212.            (UNIVERSAL ?y)
  1213.            (DJ ?w0 ?x ?y)
  1214.            (forall (?w ?x1)
  1215.                  (=> (AND (WLDR ?w0 ?w)
  1216.                           (WORLD ?w)
  1217.                           (PARTICULAR ?x1)
  1218.                           (?x ?w ?x1))
  1219.                      (exists (?y1)
  1220.                           (AND (PARTICULAR ?y1)
  1221.                                (?y ?w ?y1)
  1222.                                (P1SD.S ?w ?x1 ?y1))))))))
  1223.  
  1224. ;(D81) SD_S
  1225. ;included in def (D78)
  1226.  
  1227. ;(D82) PSD_S
  1228. ;included in def (D79)
  1229.  
  1230. ;(D83) P-1SD_S
  1231. ;included in def (D80)
  1232.  
  1233. ;(D84) GD_S: Generic Spatial Dependence
  1234. (defrelation GD.S (?w0 ?f ?g) :=
  1235.   (AND (WORLD ?w0)
  1236.        (UNIVERSAL ?f)
  1237.        (UNIVERSAL ?g)
  1238.        (DJ ?w0 ?f ?g)
  1239.        (forall (?w ?x ?s ?t)
  1240.              (=> (AND (WLDR ?w0 ?w)
  1241.                       (WORLD ?w)
  1242.                       (PARTICULAR ?x)
  1243.                       (PARTICULAR ?t)
  1244.                       (PARTICULAR ?s)
  1245.                       (?f ?w ?x))
  1246.                  (AND (exists (?t1 ?s1)
  1247.                           (AND (PARTICULAR ?t1)
  1248.                                (PARTICULAR ?s1)
  1249.                                (PRE ?w ?x ?s1 ?t1)))
  1250.                       (=> (AND (AT ?w ?t) (PRE ?w ?x ?s ?t))
  1251.                           (exists (?y)
  1252.                                (AND (PARTICULAR ?y)
  1253.                                     (?g ?w ?y)
  1254.                                     (PRE ?w ?y ?s ?t)))))))))
  1255.  
  1256. ;(D85) PGD_S: Partial Generic Spatial Dependence
  1257. (defrelation PGD.S (?w0 ?f ?g) :=
  1258.   (AND (UNIVERSAL ?f)
  1259.      (UNIVERSAL ?g)
  1260.      (WORLD ?w0)
  1261.      (DJ ?w0 ?f ?g)
  1262.      (forall (?w ?x ?s ?t)
  1263.           (=> (AND (WLDR ?w0 ?w)
  1264.                    (WORLD ?w))
  1265.                    (PARTICULAR ?x)
  1266.                    (PARTICULAR ?s)
  1267.                    (PARTICULAR ?t)
  1268.                    (?f ?w ?x))
  1269.               (AND (exists (?s1 ?t1)
  1270.                         (AND (PRE ?w ?x ?s1 ?t1)
  1271.                              (PARTICULAR ?s1)
  1272.                              (PARTICULAR ?t1))
  1273.                    (=> (AND (AT ?w ?t) (PRE ?w ?x ?s ?t))
  1274.                        (exists (?y ?u)
  1275.                             (AND (PARTICULAR ?y)
  1276.                                  (PARTICULAR ?u)
  1277.                                  (?g ?w ?y)
  1278.                                  (PP ?w ?u ?s)
  1279.                                  (PRE ?w ?y ?u ?t)))))))))
  1280.  
  1281. ;(D86) P-1GD_S: INVERSE Partial Generic Spatial Dependence
  1282. (defrelation P1GD.S (?w0 ?f ?g) :=
  1283.   (AND (UNIVERSAL ?f)
  1284.      (UNIVERSAL ?g)
  1285.      (WORLD ?w0)
  1286.      (DJ ?w0 ?f ?g)
  1287.      (forall (?w ?x ?s ?t)
  1288.           (=> (AND (WLDR ?w0 ?w)
  1289.                    (WORLD ?w))
  1290.                    (PARTICULAR ?x)
  1291.                    (PARTICULAR ?s)
  1292.                    (PARTICULAR ?t)
  1293.                    (?f ?w ?x))
  1294.               (AND (exists (?t1 ?s1)
  1295.                        (AND (PARTICULAR ?t1)
  1296.                             (PARTICULAR ?s1)
  1297.                             (PRE ?w ?x ?s1 ?t1))
  1298.                    (=> (AND (AT ?w ?t) (PRE ?w ?x ?t))
  1299.                        (exists (?y ?u)
  1300.                             (AND (PARTICULAR ?y)
  1301.                                  (PARTICULAR ?u)
  1302.                                  (?g ?w ?y)
  1303.                                  (PP ?w ?s ?u)
  1304.                                  (PRE ?w ?y ?u ?t)))))))))
  1305.  
  1306. ;(D87) DGD_S: Direct Generic Spatial Dependence
  1307. (defrelation DGD.S (?w0 ?f ?g) :=
  1308.   (AND (UNIVERSAL ?f)
  1309.        (UNIVERSAL ?g)
  1310.        (WORLD ?w0)
  1311.        (GD.S ?w0 ?f ?g)
  1312.        (NOT (exists (?h) (AND (UNIVERSAL ?h)
  1313.                               (GD.S ?w0 ?f ?h)
  1314.                               (GD.S ?w0 ?h ?g))))))
  1315.  
  1316. ;(D88) Sdt_S: Temporary Specific Spatial Dependence
  1317. (defrelation SDt.S (?w0 ?x ?y ?t) :=
  1318.   (AND (PARTICULAR ?x)
  1319.        (PARTICULAR ?y)
  1320.        (PARTICULAR ?t)
  1321.        (WORLD ?w0)
  1322.        (SD.S ?w0 ?x ?y)
  1323.        (PRE ?w0 ?x ?t)))
  1324.  
  1325. ;(D89) GDt_S: Temp. Gen. Sp. Dep.
  1326. (defrelation GDt.S (?w0 ?x ?y ?t) :=
  1327.   (AND (PARTICULAR ?x)
  1328.        (PARTICULAR ?y)
  1329.        (PARTICULAR ?t)
  1330.        (WORLD ?w0)
  1331.        (exists (?f ?g) (AND (UNIVERSAL ?f)
  1332.                             (UNIVERSAL ?g)
  1333.                             (?f ?w0 ?x)
  1334.                             (?g ?w0 ?y)
  1335.                             (GD.S ?w0 ?f ?g)
  1336.                             (~.S.t ?w0 ?x ?y ?t)))))
  1337.  
  1338. ;(D90) DGDt_S: Temp. Direct Sp. Dep.
  1339. (defrelation DGDt.S (?w0 ?x ?y ?t) :=
  1340.   (AND (PARTICULAR ?x)
  1341.        (PARTICULAR ?y)
  1342.        (PARTICULAR ?t)
  1343.        (WORLD ?w0)
  1344.        (exists (?f ?g) (AND (UNIVERSAL ?f)
  1345.                             (UNIVERSAL ?g)
  1346.                             (?f ?w0 ?x)
  1347.                             (?g ?w0 ?y)
  1348.                             (DGD.S ?w0 ?f ?g)
  1349.                             (~.S.t ?w0 ?x ?y ?t)))))
  1350.  
  1351. ;(D91) OSD_S: One-sided Specific Spatial Dependence
  1352. (defrelation OSD.S (?w0 ?f ?g) :=
  1353.   (AND (UNIVERSAL ?f)
  1354.        (UNIVERSAL ?g)
  1355.        (WORLD ?w0)
  1356.        (SD.S ?w0 ?f ?g)
  1357.        (NOT (D ?w0 ?g ?f))))
  1358.  
  1359. ;(D92) OGD_S: One-sided Generic Spatial Dependence
  1360. (defrelation OGD.S (?w0 ?f ?g) :=
  1361.   (AND (UNIVERSAL ?f)
  1362.        (UNIVERSAL ?g)
  1363.        (WORLD ?w0)
  1364.        (GD.S ?w0 ?f ?g)
  1365.        (NOT (D ?w0 ?g ?f))))
  1366.  
  1367. ;(D93) MSD_S: Mutual Specific Spatial Dependence
  1368. (defrelation MSD.S (?w0 ?f ?g) :=
  1369.   (AND (UNIVERSAL ?f)
  1370.        (UNIVERSAL ?g)
  1371.        (WORLD ?w0)
  1372.        (SD.S ?w0 ?f ?g)
  1373.        (SD.S ?w0 ?g ?f)))
  1374.  
  1375. ;(D94) MGD_S: Mutual Generic Spatial Dependence
  1376. (defrelation MGD.S (?w0 ?f ?g) :=
  1377.   (AND (UNIVERSAL ?f)
  1378.        (UNIVERSAL ?g)
  1379.        (WORLD ?w0)
  1380.        (GD.S ?w0 ?f ?g)
  1381.        (GD.S ?w0 ?g ?f)))
  1382.  
  1383. ; Constitution
  1384. ;(D95) DK: Direct Constitution
  1385. (defrelation DK (?w0 ?x ?y ?t) :=
  1386.   (AND (PARTICULAR ?x)
  1387.        (PARTICULAR ?y)
  1388.        (PARTICULAR ?t)
  1389.        (WORLD ?w0)
  1390.        (K ?w0 ?x ?y ?t)
  1391.        (NOT (exists (?z) (AND (PARTICULAR ?z)
  1392.                               (K ?w0 ?x ?z ?t)
  1393.                               (K ?w0 ?z ?y ?t))))))
  1394.  
  1395. ;(D96) SK: Constantly Specifically Constituted by
  1396. (defrelation SK (?w0 ?x ?y) :=
  1397.   (OR (AND (WORLD ?w0)
  1398.            (PARTICULAR ?x)
  1399.            (PARTICULAR ?y)
  1400.            (forall (?w)
  1401.                (=> (AND (WLDR ?w0 ?w) (WORLD ?w))
  1402.                    (AND (exists (?t)
  1403.                                (AND (PARTICULAR ?t) (PRE ?w ?x ?t))
  1404.                         (forall (?t)
  1405.                                (=> (AND (PARTICULAR ?t)
  1406.                                         (PRE ?w ?x ?t))
  1407.                                    (K ?w ?y ?x ?t))))))))
  1408.       (AND (UNIVERSAL ?x)
  1409.            (UNIVERSAL ?y)
  1410.            (WORLD ?w0)
  1411.            (DJ ?w0 ?f ?g)
  1412.            (forall (?w ?x1)
  1413.               (=> (AND (WLDR ?w0 ?w)
  1414.                        (WORLD ?w)
  1415.                        (PARTICULAR ?x1)
  1416.                        (?f ?w ?x1))
  1417.                   (exists (?y1)
  1418.                        (AND (PARTICULAR ?y1)
  1419.                             (?y ?w ?y1)
  1420.                             (SK ?w ?x1 ?y1))))))))
  1421.  
  1422. ;(D97) SK: Constantly Specifically Constituted by
  1423. ;included in def (D96)
  1424.  
  1425. ;(D98) GK: Constantly Generically Constituted by
  1426. (defrelation GK (?w0 ?f ?g) :=
  1427.   (AND (UNIVERSAL ?f)
  1428.        (UNIVERSAL ?g)
  1429.        (WORLD ?w0)
  1430.        (DJ ?w0 ?f ?g)
  1431.        (forall (?w ?x ?t)
  1432.             (=> (AND (WLDR ?w0 ?w)
  1433.                      (WORLD ?w)
  1434.                      (PARTICULAR ?x)
  1435.                      (PARTICULAR ?t)
  1436.                      (?f ?w ?x))
  1437.                 (AND (exists (?t1)
  1438.                          (AND (PARTICULAR ?t1) (PRE ?w ?x ?t1)))
  1439.                      (=> (AND (AT ?w ?t) (PRE ?w ?x ?t))
  1440.                          (exists (?y)
  1441.                               (AND (PARTICULAR ?y)
  1442.                                    (?g ?w ?y)
  1443.                                    (K ?w ?y ?x ?t)))))))))
  1444.  
  1445. ;(D99) K__Constituted by
  1446. (defrelation K (?w0 ?f ?g) :=
  1447.   (AND (UNIVERSAL ?f)
  1448.        (UNIVERSAL ?g)
  1449.        (WORLD ?w0)
  1450.        (OR (SK ?w0 ?f ?g) (GK ?w0 ?f ?g))))
  1451.  
  1452. ;(D100) OSK: One-sided Cons. Specif. CONST. by
  1453. (defrelation OSK (?w0 ?f ?g) :=
  1454.   (AND (UNIVERSAL ?f)
  1455.        (UNIVERSAL ?g)
  1456.        (WORLD ?w0)
  1457.        (SK ?w0 ?f ?g)
  1458.        (NOT (K ?w0 ?g ?f))))
  1459.  
  1460. ;(D101) OGK: One-sided Cons. Generic. CONST. by
  1461. (defrelation OGK (?w0 ?f ?g) :=
  1462.   (AND (UNIVERSAL ?f)
  1463.        (UNIVERSAL ?g)
  1464.        (WORLD ?w0)
  1465.        (GK ?w0 ?f ?g)
  1466.        (NOT (K ?w0 ?g ?f))))
  1467.  
  1468. ;(D102) MSK: Mutual Specific Constitution
  1469. (defrelation MSK (?w0 ?f ?g) :=
  1470.   (AND (UNIVERSAL ?f)
  1471.        (UNIVERSAL ?g)
  1472.        (WORLD ?w0)
  1473.        (SK ?w0 ?f ?g)
  1474.        (SK ?w0 ?g ?f)))
  1475.  
  1476. ;(D103) MGK: Mutual Generic Constitution
  1477. (defrelation MSK (?w0 ?f ?g) :=
  1478.   (AND (UNIVERSAL ?f)
  1479.        (UNIVERSAL ?g)
  1480.        (WORLD ?w0)
  1481.        (GK ?w0 ?f ?g)
  1482.        (GK ?w0 ?g ?f)))
  1483.  
  1484. ; Characterization of functions AND relations
  1485. ; Parthood
  1486. ; Argument Restrictions
  1487. ;(A1)
  1488. (forall (?w0 ?x ?y)
  1489.      (=> (AND (P ?w0 ?x ?y)
  1490.               (WORLD ?w0)
  1491.               (PARTICULAR ?x)
  1492.               (PARTICULAR ?y))
  1493.          (AND (OR (AB ?w0 ?x) (PD ?w0 ?x))
  1494.               (OR (AB ?w0 ?y) (PD ?w0 ?y)))))
  1495.  
  1496. ;(A2)
  1497. (forall (?w0 ?x ?y)
  1498.      (=> (AND (P ?w0 ?x ?y)
  1499.               (WORLD ?w0)
  1500.               (PARTICULAR ?x)
  1501.               (PARTICULAR ?y))
  1502.          (<=> (PD ?w0 ?x) (PD ?w0 ?y))))
  1503.  
  1504. ;(A3)
  1505. (forall (?w0 ?x ?y)
  1506.      (=> (AND (P ?w0 ?x ?y)
  1507.               (WORLD ?w0)
  1508.               (PARTICULAR ?x)
  1509.               (PARTICULAR ?y))
  1510.          (<=> (AB ?w0 ?x)
  1511.               (AB ?w0 ?y))))
  1512.  
  1513. ;(A4)
  1514. (forall (?w0 ?x ?y ?f)
  1515.      (=> (AND (WORLD ?w0)
  1516.               (PARTICULAR ?x)
  1517.               (PARTICULAR ?y)
  1518.               (UNIVERSAL ?f)
  1519.               (P ?w0 ?x ?y)
  1520.               (SB ?w0 R ?f)
  1521.               (X ?f))
  1522.          (<=> (?f ?w0 ?x) (?f ?w0 ?y))))
  1523.  
  1524. ; Ground Axioms
  1525. ;(A5)
  1526. (forall (?w0 ?x)
  1527.      (=> (AND (WORLD ?w0)
  1528.               (PARTICULAR ?x)
  1529.               (OR (AB ?w0 ?x) (PD ?w0 ?x)))
  1530.          (P ?w0 ?x ?x)))
  1531.  
  1532. ;(A6)
  1533. (forall (?w0 ?x ?y)
  1534.      (=> (AND (WORLD ?w0)
  1535.               (PARTICULAR ?x)
  1536.               (PARTICULAR ?y)
  1537.               (P ?w0 ?x ?y)
  1538.               (P ?w0 ?y ?x))
  1539.          (= ?x ?y)))
  1540.  
  1541. ;(A7)
  1542. (forall (?w0 ?x ?y ?z)
  1543.      (=> (AND (WORLD ?w0)
  1544.               (PARTICULAR ?x)
  1545.               (PARTICULAR ?y)
  1546.               (PARTICULAR ?z)
  1547.               (P ?w0 ?x ?y)
  1548.               (P ?w0 ?y ?z))
  1549.          (P ?w0 ?x ?z)))
  1550.  
  1551. ;(A8)
  1552. (forall (?w0 ?x ?y)
  1553.      (=> (AND (WORLD ?w0)
  1554.               (PARTICULAR ?x)
  1555.               (PARTICULAR ?y)
  1556.               (OR (AB ?w0 ?x) (PD ?w0 ?x))
  1557.               (NOT (P ?w0 ?x ?y)))
  1558.          (exists (?z)
  1559.               (AND (PARTICULAR ?x)
  1560.                    (P ?w0 ?z ?x)
  1561.                    (NOT (O ?w0 ?z ?y))))))
  1562.  
  1563. ;(A9)
  1564. ; Note: this version in KIF consider only the universal explicitly listed
  1565. ;[see comment on (D19)]
  1566. (forall (?w0 ?f)
  1567.      (=> (AND (WORLD ?w0)
  1568.               (UNIVERSAL ?f)
  1569.               (exists (?x)
  1570.                  (AND (PARTICULAR ?x) (?f ?w0 ?x)))
  1571.               (OR (forall (?x)
  1572.                       (=> (AND (PARTICULAR ?x) (?f ?w0 ?x))
  1573.                           (AB ?w0 ?x)))
  1574.                   (forall (?x)
  1575.                       (=> (AND (PARTICULAR ?x) (?f ?w0 ?x))
  1576.                           (PD ?w0 ?x)))))
  1577.          (exists (?y)
  1578.               (AND (PARTICULAR ?y) (sigma ?w0 ?f ?y)))))
  1579.  
  1580. ; Temporary Parthood
  1581. ; Argument restrictions
  1582. ;(A10)
  1583. (forall (?w0 ?x ?y ?t)
  1584.      (=> (AND (WORLD ?w0)
  1585.               (PARTICULAR ?x)
  1586.               (PARTICULAR ?y)
  1587.               (PARTICULAR ?t)
  1588.               (P ?w0 ?x ?y ?t))
  1589.          (AND (ED ?w0 ?x) (ED ?w0 ?y) (T ?w0 ?t))))
  1590.  
  1591. ;(A11)
  1592. (forall (?w0 ?x ?y ?t)
  1593.      (=> (AND (WORLD ?w0)
  1594.               (PARTICULAR ?x)
  1595.               (PARTICULAR ?y)
  1596.               (PARTICULAR ?t)
  1597.               (P ?w0 ?x ?y ?t))
  1598.          (<=> (PED ?w0 ?x) (PED ?w0 ?y))))
  1599.  
  1600. ;(A12)
  1601. (forall (?w0 ?x ?y ?t)
  1602.      (=> (AND (WORLD ?w0)
  1603.               (PARTICULAR ?x)
  1604.               (PARTICULAR ?y)
  1605.               (PARTICULAR ?t)
  1606.               (P ?w0 ?x ?y ?t))
  1607.          (<=> (NPED ?w0 ?x) (NPED ?w0 ?y))))
  1608.  
  1609. ; Ground Axioms
  1610. ;(A13)
  1611. (forall (?w0 ?x ?y ?z ?t)
  1612.      (=> (AND (WORLD ?w0)
  1613.               (PARTICULAR ?x)
  1614.               (PARTICULAR ?y)
  1615.               (PARTICULAR ?z)
  1616.               (PARTICULAR ?t)
  1617.               (P ?w0 ?x ?y ?t)
  1618.               (P ?w0 ?y ?z ?t))
  1619.          (P ?w0 ?x ?z ?t)))
  1620.  
  1621. ;(A14)
  1622. (forall (?w0 ?x ?y ?t)
  1623.      (=> (AND (WORLD ?w0)
  1624.               (PARTICULAR ?x)
  1625.               (PARTICULAR ?y)
  1626.               (PARTICULAR ?t)
  1627.               (ED ?w0 ?x)
  1628.               (ED ?w0 ?y)
  1629.               (PRE ?w0 ?x ?t)
  1630.               (PRE ?w0 ?y ?t)
  1631.               (NOT (P ?w0 ?x ?y ?t)))
  1632.          (exists (?z)
  1633.               (AND (PARTICULAR ?z)
  1634.                    (P ?w0 ?z ?x ?t)
  1635.                    (NOT (O ?w0 ?z ?y ?t))))))
  1636.  
  1637. ;(A15)
  1638. ;[see comment on (D19)]
  1639. (forall (?w0 ?f)
  1640.      (=> (AND (WORLD ?w0)
  1641.               (UNIVERSAL ?f)
  1642.               (exists (?x)
  1643.                  (AND (PARTICULAR ?x) (?f ?w0 ?x)))
  1644.               (forall (?x)
  1645.                       (=> (AND (PARTICULAR ?x) (?f ?w0 ?x))
  1646.                           (ED ?w0 ?x))))
  1647.          (exists (?y)
  1648.               (AND (PARTICULAR ?y) (sigma.t ?w0 ?f ?y)))))
  1649.  
  1650. ; Links With Other Primitives
  1651. ;(A16)
  1652. (forall (?w0 ?x ?t)
  1653.      (=> (AND (WORLD ?w0)
  1654.               (PARTICULAR ?x)
  1655.               (PARTICULAR ?t)
  1656.               (ED ?w0 ?x)
  1657.               (PRE ?w0 ?x ?t))
  1658.          (P ?w0 ?x ?x ?t)))
  1659.  
  1660. ;(A17)
  1661. (forall (?w0 ?x ?y ?t)
  1662.      (=> (AND (WORLD ?w0)
  1663.               (PARTICULAR ?x)
  1664.               (PARTICULAR ?y)
  1665.               (PARTICULAR ?t)
  1666.               (P ?w0 ?x ?y ?t))
  1667.          (AND (PRE ?w0 ?x ?t) (PRE ?w0 ?y ?t))))
  1668.  
  1669. ;(A18)
  1670. (forall (?w0 ?x ?y ?t ?u)
  1671.      (=> (AND (WORLD ?w0)
  1672.               (PARTICULAR ?x)
  1673.               (PARTICULAR ?y)
  1674.               (PARTICULAR ?t)
  1675.               (PARTICULAR ?u)
  1676.               (P ?w0 ?x ?y ?t)
  1677.               (P ?w0 ?u ?t))
  1678.          (P ?w0 ?x ?y ?u)))
  1679.  
  1680. ;(A19)
  1681. (forall (?w0 ?x ?y ?t)
  1682.      (=> (AND (WORLD ?w0)
  1683.               (PARTICULAR ?x)
  1684.               (PARTICULAR ?y)
  1685.               (PARTICULAR ?t)
  1686.               (PED ?w0 ?x)
  1687.               (P ?w0 ?x ?y ?t))
  1688.          (incl.S.t ?w0 ?x ?y ?t)))
  1689.  
  1690. ; Constitution
  1691. ; Argument restrictions
  1692. ;(A20)
  1693. (forall (?w0 ?x ?y ?t)
  1694.      (=> (AND (WORLD ?w0)
  1695.               (PARTICULAR ?x)
  1696.               (PARTICULAR ?y)
  1697.               (PARTICULAR ?t)
  1698.               (K ?w0 ?x ?y ?t))
  1699.          (AND (OR (ED ?w0 ?x) (PD ?w0 ?x))
  1700.               (OR (ED ?w0 ?y) (PD ?w0 ?y))
  1701.               (T ?w0 ?t))))
  1702.  
  1703. ;(A21)
  1704. (forall (?w0 ?x ?y ?t)
  1705.      (=> (AND (WORLD ?w0)
  1706.               (PARTICULAR ?x)
  1707.               (PARTICULAR ?y)
  1708.               (PARTICULAR ?t)
  1709.               (K ?w0 ?x ?y ?t))
  1710.          (<=> (PED ?w0 ?x) (PED ?w0 ?y))))
  1711.  
  1712. ;(A22)
  1713. (forall (?w0 ?x ?y ?t)
  1714.      (=> (AND (WORLD ?w0)
  1715.               (PARTICULAR ?x)
  1716.               (PARTICULAR ?y)
  1717.               (PARTICULAR ?t)
  1718.               (K ?w0 ?x ?y ?t))
  1719.          (<=> (NPED ?w0 ?x) (NPED ?w0 ?y))))
  1720.  
  1721. ;(A23)
  1722. (forall (?w0 ?x ?y ?t)
  1723.      (=> (AND (WORLD ?w0)
  1724.               (PARTICULAR ?x)
  1725.               (PARTICULAR ?y)
  1726.               (PARTICULAR ?t)
  1727.               (K ?w0 ?x ?y ?t))
  1728.          (<=> (PD ?w0 ?x) (PD ?w0 ?y))))
  1729.  
  1730. ; Ground Axioms
  1731. ;(A24)
  1732. (forall (?w0 ?x ?y ?t)
  1733.      (=> (AND (WORLD ?w0)
  1734.               (PARTICULAR ?x)
  1735.               (PARTICULAR ?y)
  1736.               (PARTICULAR ?t)
  1737.               (K ?w0 ?x ?y ?t))
  1738.          (NOT (K ?w0 ?y ?x ?t))))
  1739.  
  1740. ;(A25)
  1741. (forall (?w0 ?x ?y ?z ?t)
  1742.      (=> (AND (WORLD ?w0)
  1743.               (PARTICULAR ?x)
  1744.               (PARTICULAR ?y)
  1745.               (PARTICULAR ?z)
  1746.               (PARTICULAR ?t)
  1747.               (K ?w0 ?x ?y ?t)
  1748.               (K ?w0 ?y ?z ?t))
  1749.          (K ?w0 ?x ?z ?t)))
  1750.  
  1751. ; Links with other Primitives
  1752. ;(A26)
  1753. (forall (?w0 ?x ?y ?t)
  1754.      (=> (AND (WORLD ?w0)
  1755.               (PARTICULAR ?x)
  1756.               (PARTICULAR ?y)
  1757.               (PARTICULAR ?t)
  1758.               (K ?w0 ?x ?y ?t))
  1759.          (AND (PRE ?w0 ?x ?t) (PRE ?w0 ?y ?t))))
  1760.  
  1761. ;(A27)
  1762. (forall (?w0 ?x ?y ?t)
  1763.      (=> (AND (WORLD ?w0)
  1764.               (PARTICULAR ?x)
  1765.               (PARTICULAR ?y)
  1766.               (PARTICULAR ?t))
  1767.          (<=> (K ?w0 ?x ?y ?t)
  1768.               (forall (?u)
  1769.                   (=> (AND (PARTICULAR ?u) (P ?w0 ?u ?t))
  1770.                       (K ?w0 ?x ?y ?u))))))
  1771.  
  1772. ;(A28)
  1773. (forall (?w0 ?x ?y ?t)
  1774.      (=> (AND (WORLD ?w0)
  1775.               (PARTICULAR ?x)
  1776.               (PARTICULAR ?y)
  1777.               (PARTICULAR ?t)
  1778.               (PED ?w0 ?x)
  1779.               (K ?w0 ?x ?y ?t))
  1780.          (~.S.t ?w0 ?x ?y ?t)))
  1781.  
  1782. ;(A29)
  1783. (forall (?w0 ?x ?y ?y1 ?t)
  1784.      (=> (AND (WORLD ?w0)
  1785.               (PARTICULAR ?x)
  1786.               (PARTICULAR ?y)
  1787.               (PARTICULAR ?y1)
  1788.               (PARTICULAR ?t)
  1789.               (K ?w0 ?x ?y ?t)
  1790.               (P ?w0 ?y1 ?y ?t))
  1791.          (exists (?x1)
  1792.               (AND (PARTICULAR ?x1)
  1793.                    (P ?w0 ?x1 ?x ?t)
  1794.                    (K ?w0 ?x1 ?y1 ?t)))))
  1795.  
  1796. ; Links between Categories
  1797. ;(A30)
  1798. (forall (?w0) (=> (WORLD ?w0) (GK ?w0 NAPO M)))
  1799.  
  1800. ;(A31)
  1801. (forall (?w0) (=> (WORLD ?w0) (GK ?w0 APO NAPO)))
  1802.  
  1803. ;(A32)
  1804. (forall (?w0) (=> (WORLD ?w0) (GK ?w0 SC SAG)))
  1805.  
  1806. ; Participation
  1807. ; Argument restrictions
  1808. ;(A33)
  1809. (forall (?w0 ?x ?y ?t)
  1810.      (=> (AND (WORLD ?w0)
  1811.               (PARTICULAR ?x)
  1812.               (PARTICULAR ?y)
  1813.               (PARTICULAR ?t)
  1814.               (PC ?w0 ?x ?y ?t))
  1815.          (AND (ED ?w0 ?x) (PD ?w0 ?y) (T ?w0 ?t))))
  1816.  
  1817. ; Existential Axioms
  1818. ;(a34)
  1819. (forall (?w0 ?x ?t)
  1820.      (=> (AND (WORLD ?w0)
  1821.               (PARTICULAR ?x)
  1822.               (PARTICULAR ?t)
  1823.               (PD ?w0 ?x)
  1824.               (PRE ?w0 ?x ?t))
  1825.          (exists (?y)
  1826.               (AND (PARTICULAR ?y) (PC ?w0 ?y ?x ?t)))))
  1827.  
  1828. ;(a35)
  1829. (forall (?w0 ?x)
  1830.      (=> (AND (WORLD ?w0) (PARTICULAR ?x) (ED ?w0 ?x))
  1831.          (exists (?y ?t)
  1832.               (AND (PARTICULAR ?y) (PARTICULAR ?t) (PC ?w0 ?x ?y ?t)))))
  1833.  
  1834. ; Links with other Primitives
  1835. ;(a36)
  1836. (forall (?w0 ?x ?y ?t)
  1837.      (=> (AND (WORLD ?w0)
  1838.               (PARTICULAR ?x)
  1839.               (PARTICULAR ?y)
  1840.               (PARTICULAR ?t)
  1841.               (PC ?w0 ?x ?y ?t))
  1842.          (AND (PRE ?w0 ?x ?t) (PRE ?w0 ?y ?t))))
  1843.  
  1844. ;(a37)
  1845. (forall (?w0 ?x ?y ?t)
  1846.      (=> (AND (WORLD ?w0)
  1847.               (PARTICULAR ?x)
  1848.               (PARTICULAR ?y)
  1849.               (PARTICULAR ?t))
  1850.          (<=> (PC ?w0 ?x ?y ?t)
  1851.               (forall (?u)
  1852.                   (=> (AND (PARTICULAR ?u) (P ?w0 ?u ?t))
  1853.                       (PC ?w0 ?x ?y ?u))))))
  1854.  
  1855. ; Quality
  1856. ; Argument restrictions:
  1857. ;(a38)
  1858. (forall (?w0 ?x ?y)
  1859.      (=> (AND (WORLD ?w0)
  1860.               (PARTICULAR ?x)
  1861.               (PARTICULAR ?y)
  1862.               (qt ?w0 ?x ?y))
  1863.          (AND (Q ?w0 ?x)
  1864.               (OR (Q ?w0 ?y) (ED ?w0 ?y) (PD ?w0 ?y)))))
  1865.  
  1866. ;(a39)
  1867. (forall (?w0 ?x ?y)
  1868.      (=> (AND (WORLD ?w0)
  1869.               (PARTICULAR ?x)
  1870.               (PARTICULAR ?y)
  1871.               (qt ?w0 ?x ?y))
  1872.          (<=> (TQ ?w0 ?x)
  1873.               (OR (TQ ?w0 ?y) (PD ?w0 ?y)))))
  1874.  
  1875. ;(a40)
  1876. (forall (?w0 ?x ?y)
  1877.      (=> (AND (WORLD ?w0)
  1878.               (PARTICULAR ?x)
  1879.               (PARTICULAR ?y)
  1880.               (qt ?w0 ?x ?y))
  1881.          (<=> (PQ ?w0 ?x)
  1882.               (OR (PQ ?w0 ?y) (PED ?w0 ?y)))))
  1883.  
  1884. ;(a41)
  1885. (forall (?w0 ?x ?y)
  1886.      (=> (AND (WORLD ?w0)
  1887.               (PARTICULAR ?x)
  1888.               (PARTICULAR ?y)
  1889.               (qt ?w0 ?x ?y))
  1890.          (<=> (AQ ?w0 ?x)
  1891.               (OR (AQ ?w0 ?y) (NPED ?w0 ?y)))))
  1892.  
  1893. ; Ground Axioms:
  1894. ;(a42)
  1895. (forall (?w0 ?x ?y ?z)
  1896.      (=> (AND (WORLD ?w0)
  1897.               (PARTICULAR ?x)
  1898.               (PARTICULAR ?y)
  1899.               (PARTICULAR ?z)
  1900.               (qt ?w0 ?x ?y)
  1901.               (qt ?w0 ?y ?z))
  1902.          (qt ?w0 ?x ?z)))
  1903.  
  1904. ;(a43)
  1905. (forall (?w0 ?x ?y ?z)
  1906.      (=> (AND (WORLD ?w0)
  1907.               (PARTICULAR ?x)
  1908.               (PARTICULAR ?y)
  1909.               (PARTICULAR ?z)
  1910.               (qt ?w0 ?x ?y)
  1911.               (qt ?w0 ?x ?z))
  1912.          (= ?y ?z)))
  1913.  
  1914. ;(a44)
  1915. (forall (?w0 ?f ?x ?y ?z)
  1916.      (=> (AND (WORLD ?w0)
  1917.               (UNIVERSAL ?f)
  1918.               (PARTICULAR ?x)
  1919.               (PARTICULAR ?y)
  1920.               (PARTICULAR ?z)
  1921.               (qtf ?w0 ?f ?x ?y)
  1922.               (qtf ?w0 ?f ?z ?y))
  1923.          (= ?x ?z)))
  1924.  
  1925. ;(a45)
  1926. (forall (?w0 ?f ?g ?x ?y ?z)
  1927.      (=> (AND (WORLD ?w0)
  1928.               (UNIVERSAL ?f)
  1929.               (UNIVERSAL ?g)
  1930.               (PARTICULAR ?x)
  1931.               (PARTICULAR ?y)
  1932.               (PARTICULAR ?z)
  1933.               (qtf ?w0 ?f ?x ?y)
  1934.               (qtf ?w0 ?g ?y ?z))
  1935.          (DJ ?w0 ?f ?g)))
  1936.  
  1937. ; Existential Axioms:
  1938. ;(a46)
  1939. (forall (?w0 ?x)
  1940.      (=> (AND (WORLD ?w0) (PARTICULAR ?x) (TQ ?w0 ?x))
  1941.          (exists (?y)
  1942.               (AND (PARTICULAR ?y)
  1943.                    (qt ?w0 ?x ?y)
  1944.                    (PD ?w0 ?y)
  1945.                    (forall (?z)
  1946.                        (=> (AND (PARTICULAR ?z)
  1947.                                 (qt ?w0 ?x ?z)
  1948.                                 (PD ?w0 ?z))
  1949.                            (= ?z ?y)))))))
  1950.  
  1951. ;(a47)
  1952. (forall (?w0 ?x)
  1953.      (=> (AND (WORLD ?w0) (PARTICULAR ?x) (PQ ?w0 ?x))
  1954.          (exists (?y)
  1955.               (AND (PARTICULAR ?y)
  1956.                    (qt ?w0 ?x ?y)
  1957.                    (PED ?w0 ?y)
  1958.                    (forall (?z)
  1959.                        (=> (AND (PARTICULAR ?z)
  1960.                                 (qt ?w0 ?x ?z)
  1961.                                 (PED ?w0 ?z))
  1962.                            (= ?z ?y)))))))
  1963.  
  1964. ;(a48)
  1965. (forall (?w0 ?x)
  1966.      (=> (AND (WORLD ?w0) (PARTICULAR ?x) (AQ ?w0 ?x))
  1967.          (exists (?y)
  1968.               (AND (PARTICULAR ?y)
  1969.                    (qt ?w0 ?x ?y)
  1970.                    (NPED ?w0 ?y)
  1971.                    (forall (?z)
  1972.                        (=> (AND (PARTICULAR ?z)
  1973.                                 (qt ?w0 ?x ?z)
  1974.                                 (NPED ?w0 ?z))
  1975.                            (= ?z ?y)))))))
  1976.  
  1977. ;(a49)
  1978. (forall (?w0 ?x)
  1979.      (=> (AND (WORLD ?w0) (PARTICULAR ?x) (PD ?w0 ?x))
  1980.          (exists (?y)
  1981.               (AND (PARTICULAR ?y) (qtf ?w0 TL ?y ?x)))))
  1982.  
  1983. ;(a50)
  1984. (forall (?w0 ?x)
  1985.      (=> (AND (WORLD ?w0) (PARTICULAR ?x) (PED ?w0 ?x))
  1986.          (exists (?y)
  1987.               (AND (PARTICULAR ?y) (qtf ?w0 SL ?y ?x)))))
  1988.  
  1989. ;(a51)
  1990. (forall (?w0 ?x)
  1991.      (=> (AND (WORLD ?w0) (PARTICULAR ?x) (NPED ?w0 ?x))
  1992.          (exists (?f ?y)
  1993.               (AND (PARTICULAR ?y)
  1994.                    (UNIVERSAL ?f)
  1995.                    (SBL ?w0 AQ ?f)
  1996.                    (qtf ?w0 ?f ?y ?x)))))
  1997.  
  1998. ; Quale
  1999. ; Immediate Quale
  2000. ; Argument restrictions:
  2001. ;(A52)
  2002. (forall (?w0 ?x ?y)
  2003.      (=> (AND (WORLD ?w0)
  2004.               (PARTICULAR ?x)
  2005.               (PARTICULAR ?y)
  2006.               (ql ?w0 ?x ?y))
  2007.          (AND (TR ?w0 ?x) (TQ ?w0 ?y))))
  2008.  
  2009. ;(A53)
  2010. (forall (?w0 ?x ?y)
  2011.      (=> (AND (WORLD ?w0)
  2012.               (PARTICULAR ?x)
  2013.               (PARTICULAR ?y)
  2014.               (ql ?w0 ?x ?y)
  2015.               (TL ?w0 ?y))
  2016.          (T ?w0 ?x)))
  2017.  
  2018. ; Basic Axioms:
  2019. ;(A54)
  2020. (forall (?w0 ?x ?x1 ?y)
  2021.      (=> (AND (WORLD ?w0)
  2022.               (PARTICULAR ?x)
  2023.               (PARTICULAR ?x1)
  2024.               (PARTICULAR ?y)
  2025.               (ql ?w0 ?x ?y)
  2026.               (ql ?w0 ?x1 ?y))
  2027.          (= ?x ?x1)))
  2028.  
  2029. ; Existential Axioms:
  2030. ;(A55)
  2031. (forall (?w0 ?x)
  2032.      (=> (AND (WORLD ?w0)
  2033.               (PARTICULAR ?x)
  2034.               (TQ ?w0 ?x))
  2035.          (exists (?y)
  2036.               (AND (PARTICULAR ?y) (ql ?w0 ?y ?x)))))
  2037.  
  2038. ;(A56)
  2039. (forall (?w0 ?f ?x ?y ?r ?r1)
  2040.      (=> (AND (WORLD ?w0)
  2041.               (UNIVERSAL ?f)
  2042.               (PARTICULAR ?x)
  2043.               (PARTICULAR ?y)
  2044.               (PARTICULAR ?r)
  2045.               (PARTICULAR ?r1)
  2046.               (L.X ?w0 ?f)
  2047.               (?f ?w0 ?x)
  2048.               (?f ?w0 ?y)
  2049.               (ql ?w0 ?r ?x)
  2050.               (ql ?w0 ?r1 ?y))
  2051.          (exists (?g)
  2052.               (AND (UNIVERSAL ?g)
  2053.                    (L.X ?w0 ?g)
  2054.                    (?g ?w0 ?r)
  2055.                    (?g ?w0 ?r1)))))
  2056.  
  2057. ;(A57)
  2058. (forall (?w0 ?f ?x ?y ?r ?r1)
  2059.      (=> (AND (WORLD ?w0)
  2060.               (UNIVERSAL ?f)
  2061.               (PARTICULAR ?x)
  2062.               (PARTICULAR ?y)
  2063.               (PARTICULAR ?r)
  2064.               (PARTICULAR ?r1)
  2065.               (L.X ?w0 ?f)
  2066.               (?f ?w0 ?x)
  2067.               (NOT (?f ?w0 ?y))
  2068.               (ql ?w0 ?r ?x)
  2069.               (ql ?w0 ?r1 ?y))
  2070.          (NOT (exists (?g)
  2071.                  (AND (UNIVERSAL ?g)
  2072.                       (L.X ?w0 ?g)
  2073.                       (?g ?w0 ?r)
  2074.                       (?g ?w0 ?r1))))))
  2075.  
  2076. ; Temporary Quale
  2077. ; Argument restrictions:
  2078. ;(A58)
  2079. (forall (?w0 ?x ?y ?t)
  2080.      (=> (AND (WORLD ?w0)
  2081.               (PARTICULAR ?x)
  2082.               (PARTICULAR ?y)
  2083.               (PARTICULAR ?t)
  2084.               (ql ?w0 ?x ?y ?t))
  2085.          (AND (OR (PR ?w0 ?x) (AR ?w0 ?x))
  2086.               (OR (PQ ?w0 ?y) (AQ ?w0 ?y))
  2087.               (T ?w0 ?t))))
  2088.  
  2089. ;(A59)
  2090. (forall (?w0 ?x ?y ?t)
  2091.      (=> (AND (WORLD ?w0)
  2092.               (PARTICULAR ?x)
  2093.               (PARTICULAR ?y)
  2094.               (PARTICULAR ?t)
  2095.               (ql ?w0 ?x ?y ?t))
  2096.          (<=> (PR ?w0 ?x) (PQ ?w0 ?y))))
  2097.  
  2098. ;(A60)
  2099. (forall (?w0 ?x ?y ?t)
  2100.      (=> (AND (WORLD ?w0)
  2101.               (PARTICULAR ?x)
  2102.               (PARTICULAR ?y)
  2103.               (PARTICULAR ?t)
  2104.               (ql ?w0 ?x ?y ?t))
  2105.          (<=> (AR ?w0 ?x) (AQ ?w0 ?y))))
  2106.  
  2107. ;(A61)
  2108. (forall (?w0 ?x ?y ?t)
  2109.      (=> (AND (WORLD ?w0)
  2110.               (PARTICULAR ?x)
  2111.               (PARTICULAR ?y)
  2112.               (PARTICULAR ?t)
  2113.               (ql ?w0 ?x ?y ?t)
  2114.               (SL ?w0 ?y))
  2115.          (S ?w0 ?x)))
  2116.  
  2117. ; Existential Axioms:
  2118. ;(A62)
  2119. (forall (?w0 ?x)
  2120.      (=> (AND (WORLD ?w0)
  2121.               (PARTICULAR ?x)
  2122.               (OR (PQ ?w0 ?x) (AQ ?w0 ?x))
  2123.               (PRE ?w0 ?x ?t))
  2124.          (exists (?y)
  2125.               (AND (PARTICULAR ?y) (ql ?w0 ?y ?x ?t)))))
  2126.  
  2127. ;(A63)
  2128. (forall (?w0 ?f ?x ?y ?r ?r1 ?t)
  2129.      (=> (AND (WORLD ?w0)
  2130.               (UNIVERSAL ?f)
  2131.               (PARTICULAR ?x)
  2132.               (PARTICULAR ?y)
  2133.               (PARTICULAR ?r)
  2134.               (PARTICULAR ?r1)
  2135.               (PARTICULAR ?t)
  2136.               (L.X ?w0 ?f)
  2137.               (?f ?w0 ?x)
  2138.               (?f ?w0 ?y)
  2139.               (ql ?w0 ?r ?x ?t)
  2140.               (ql ?w0 ?r1 ?y ?t))
  2141.          (exists (?g)
  2142.               (AND (UNIVERSAL ?g)
  2143.                    (L.X ?w0 ?g)
  2144.                    (?g ?w0 ?r)
  2145.                    (?g ?w0 ?r1)))))
  2146.  
  2147. ;(A64)
  2148. (forall (?w0 ?f ?x ?y ?r ?r1 ?t)
  2149.      (=> (AND (WORLD ?w0)
  2150.               (UNIVERSAL ?f)
  2151.               (PARTICULAR ?x)
  2152.               (PARTICULAR ?y)
  2153.               (PARTICULAR ?r)
  2154.               (PARTICULAR ?r1)
  2155.               (PARTICULAR ?t)
  2156.               (L.X ?w0 ?f)
  2157.               (?f ?w0 ?x)
  2158.               (NOT (?f ?w0 ?y))
  2159.               (ql ?w0 ?r ?x ?t)
  2160.               (ql ?w0 ?r1 ?y ?t))
  2161.          (NOT (exists (?g)
  2162.                  (AND (UNIVERSAL ?g)
  2163.                       (L.X ?w0 ?g)
  2164.                       (?g ?w0 ?r)
  2165.                       (?g ?w0 ?r1))))))
  2166.  
  2167. ; Link with Parthood AND extension:
  2168. ;(A65)
  2169. (forall (?w0 ?x ?y ?t)
  2170.      (=> (AND (WORLD ?w0)
  2171.               (PARTICULAR ?x)
  2172.               (PARTICULAR ?y)
  2173.               (PARTICULAR ?t)
  2174.               (ql ?w0 ?x ?y ?t))
  2175.          (PRE ?w0 ?y ?t)))
  2176.  
  2177. ;(A66)
  2178. (forall (?w0 ?x ?y ?t)
  2179.      (=> (AND (WORLD ?w0)
  2180.               (PARTICULAR ?x)
  2181.               (PARTICULAR ?y)
  2182.               (PARTICULAR ?t))
  2183.          (<=> (ql ?w0 ?x ?y ?t)
  2184.               (forall (?u)
  2185.                       (=> (AND (PARTICULAR ?u) (P ?w0 ?u ?t))
  2186.                           (ql ?w0 ?x ?y ?u))))))
  2187.  
  2188. ; Dependence AND Spatial Dependence
  2189. ; Links between categories
  2190. ;(A67)
  2191. (forall (?w0) (=> (WORLD ?w0) (MSD ?w0 TQ PD)))
  2192.  
  2193. ;(A68)
  2194. (forall (?w0) (=> (WORLD ?w0) (MSD.S ?w0 PQ PED)))
  2195.  
  2196. ;(A69)
  2197. (forall (?w0) (=> (WORLD ?w0) (MSD ?w0 AQ NPED)))
  2198.  
  2199. ;(A70)
  2200. (forall (?w0) (=> (WORLD ?w0) (OGD ?w0 F NAPO)))
  2201.  
  2202. ;(A71)
  2203. (forall (?w0) (=> (WORLD ?w0) (OSD ?w0 MOB APO)))
  2204.  
  2205. ;(A72)
  2206. (forall (?w0) (=> (WORLD ?w0) (OGD ?w0 SAG APO)))
  2207.  
  2208. ;(A73)
  2209. (forall (?w0) (=> (WORLD ?w0) (OGD ?w0 NASO SC)))
  2210.  
  2211. ;(A74)
  2212. (forall (?w0) (=> (WORLD ?w0) (OD ?w0 NPED PED)))
  2213.  
  2214. ; Characterization of Categories
  2215. ; Perdurant
  2216. ; Conditions on Perdurant's Leaves
  2217. ;(A75)
  2218. (forall (?w0 ?f)
  2219.      (=> (AND (WORLD ?w0)
  2220.               (UNIVERSAL ?f)
  2221.               (PSBL ?w0 ACH ?f))
  2222.          (AND (NEP.S ?w0 ?f) (CM~ ?w0 ?f) (AT ?w0 ?f))))
  2223.  
  2224. ;(A76)
  2225. (forall (?w0 ?f)
  2226.      (=> (AND (WORLD ?w0)
  2227.               (UNIVERSAL ?f)
  2228.               (PSBL ?w0 ACC ?f))
  2229.          (AND (NEP.S ?w0 ?f) (CM~ ?w0 ?f) (AT~ ?w0 ?f))))
  2230.  
  2231. ;(A77)
  2232. (forall (?w0 ?f)
  2233.      (=> (AND (WORLD ?w0)
  2234.               (UNIVERSAL ?f)
  2235.               (PSBL ?w0 ST ?f))
  2236.          (AND (NEP.S ?w0 ?f) (CM ?w0 ?f) (HOM ?w0 ?f))))
  2237.  
  2238. ;(A78)
  2239. (forall (?w0 ?f)
  2240.      (=> (AND (WORLD ?w0)
  2241.               (UNIVERSAL ?f)
  2242.               (PSBL ?w0 PRO ?f))
  2243.          (AND (NEP.S ?w0 ?f) (CM ?w0 ?f) (HOM~ ?w0 ?f))))
  2244.  
  2245. ; Existential Axioms
  2246. ;(A79)
  2247.   (forall (?w0)
  2248.      (=> (WORLD ?w0)
  2249.          (exists (?f) (AND (UNIVERSAL ?f) (PSBL ?w0 ACH ?f)))))
  2250.  
  2251. ;(A80)
  2252.   (forall (?w0)
  2253.      (=> (WORLD ?w0)
  2254.          (exists (?f) (AND (UNIVERSAL ?f) (PSBL ?w0 ACC ?f)))))
  2255.  
  2256. ;(A81)
  2257.   (forall (?w0)
  2258.      (=> (WORLD ?w0)
  2259.          (exists (?f) (AND (UNIVERSAL ?f) (PSBL ?w0 ST ?f)))))
  2260.  
  2261. ;(A82)
  2262.   (forall (?w0)
  2263.      (=> (WORLD ?w0)
  2264.          (exists (?f) (AND (UNIVERSAL ?f) (PSBL ?w0 PRO ?f)))))
  2265. ; =========================================
  2266. ; THEOREMS
  2267. ; General Properties
  2268. ; (T1)
  2269.   (forall (?w0 ?x ?t)
  2270.      (=> (AND (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?t))
  2271.          (NOT (K ?w0 ?x ?x ?t))))
  2272.  
  2273. ; (T2)
  2274.   (forall (?w0 ?f ?g)
  2275.      (=> (AND (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (SK ?w0 ?f ?g))
  2276.          (SD ?w0 ?f ?g)))
  2277.  
  2278. ; (T3)
  2279.   (forall (?w0 ?f ?g)
  2280.      (=> (AND (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (GK ?w0 ?f ?g))
  2281.          (GD ?w0 ?f ?g)))
  2282.  
  2283. ; (T4)
  2284.   (forall (?w0 ?f ?g ?h)
  2285.      (=> (AND (WORLD ?w0)
  2286.               (UNIVERSAL ?f)
  2287.               (UNIVERSAL ?g)
  2288.               (UNIVERSAL ?h)
  2289.               (SK ?w0 ?f ?g)
  2290.               (SK ?w0 ?g ?h)
  2291.               (DJ ?w0 ?f ?h))
  2292.          (SK ?w0 ?f ?h)))
  2293.  
  2294. ; (T5)
  2295.   (forall (?w0 ?f ?g ?h)
  2296.      (=> (AND (WORLD ?w0)
  2297.               (UNIVERSAL ?f)
  2298.               (UNIVERSAL ?g)
  2299.               (UNIVERSAL ?h)
  2300.               (GK ?w0 ?f ?g)
  2301.               (GK ?w0 ?g ?h)
  2302.               (DJ ?w0 ?f ?h))
  2303.          (GK ?w0 ?f ?h)))
  2304.  
  2305. ; Ground Properties
  2306. ; (T6)
  2307.   (forall (?w0 ?x ?t)
  2308.      (=> (AND (WORLD ?w0) (PARTICULAR ?x) (PARTICULAR ?t))
  2309.          (NOT (PC ?w0 ?x ?x ?t))))
  2310.  
  2311. ; (T7)
  2312.   (forall (?w0 ?x ?t)
  2313.      (=> (AND (WORLD ?w0)
  2314.               (PARTICULAR ?x)
  2315.               (PARTICULAR ?y)
  2316.               (PARTICULAR ?t)
  2317.               (PC ?w0 ?x ?y ?t))
  2318.          (NOT (PC ?w0 ?y ?x ?t))))
  2319.  
  2320. ; (T8)
  2321.   (forall (?w0 ?x)
  2322.      (=> (AND (WORLD ?w0) (PARTICULAR ?x))
  2323.          (NOT (qt ?w0 ?x ?x))))
  2324.  
  2325. ; General properties
  2326. ; (T9)
  2327.   (forall (?w0 ?f ?g ?h)
  2328.      (=> (AND (WORLD ?w0)
  2329.               (UNIVERSAL ?f)
  2330.               (UNIVERSAL ?g)
  2331.               (UNIVERSAL ?h)
  2332.               (SD ?w0 ?f ?g)
  2333.               (SD ?w0 ?g ?h)
  2334.               (DJ ?w0 ?f ?h))
  2335.          (SD ?w0 ?f ?h)))
  2336.  
  2337. ; (T10)
  2338.   (forall (?w0 ?f ?g ?h)
  2339.      (=> (AND (WORLD ?w0)
  2340.               (UNIVERSAL ?f)
  2341.               (UNIVERSAL ?g)
  2342.               (UNIVERSAL ?h)
  2343.               (GD ?w0 ?f ?g)
  2344.               (GD ?w0 ?g ?h)
  2345.               (DJ ?w0 ?f ?h))
  2346.          (GD ?w0 ?f ?h)))
  2347.  
  2348. ; (T11)
  2349.   (forall (?w0 ?f ?g ?h)
  2350.      (=> (AND (WORLD ?w0)
  2351.               (UNIVERSAL ?f)
  2352.               (UNIVERSAL ?g)
  2353.               (UNIVERSAL ?h)
  2354.               (SD ?w0 ?f ?g)
  2355.               (GD ?w0 ?g ?h)
  2356.               (DJ ?w0 ?f ?h))
  2357.          (GD ?w0 ?f ?h)))
  2358.  
  2359. ; (T12)
  2360.   (forall (?w0 ?f ?g ?h)
  2361.      (=> (AND (WORLD ?w0)
  2362.               (UNIVERSAL ?f)
  2363.               (UNIVERSAL ?g)
  2364.               (UNIVERSAL ?h)
  2365.               (GD ?w0 ?f ?g)
  2366.               (SD ?w0 ?g ?h)
  2367.               (DJ ?w0 ?f ?h))
  2368.          (GD ?w0 ?f ?h)))
  2369.  
  2370. ; (T13)
  2371.   (forall (?w0 ?f ?g)
  2372.      (=> (AND (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (SD.S ?w0 ?f ?g))
  2373.          (SD ?w0 ?f ?g)))
  2374.  
  2375. ; (T14)
  2376.   (forall (?w0 ?f ?g)
  2377.      (=> (AND (WORLD ?w0) (UNIVERSAL ?f) (UNIVERSAL ?g) (GD.S ?w0 ?f ?g))
  2378.          (GD ?w0 ?f ?g)))
  2379.  
  2380. ; Being Present
  2381. ; (T15)
  2382.   (forall (?w0 ?x)
  2383.      (=> (AND (WORLD ?w0)
  2384.               (PARTICULAR ?x)
  2385.               (OR (ED ?w0 ?x) (PD ?w0 ?x) (Q ?w0 ?x)))
  2386.          (exists (?t)
  2387.               (AND (PARTICULAR ?t) (PRE ?w0 ?x ?t)))))
  2388.  
  2389. ; (T16)
  2390.   (forall (?w0 ?x ?t)
  2391.      (=> (AND (WORLD ?w0)
  2392.               (PARTICULAR ?x)
  2393.               (PARTICULAR ?t)
  2394.               (OR (PED ?w0 ?x) (PQ ?w0 ?x))
  2395.               (PRE ?w0 ?x ?t))
  2396.          (exists (?s)
  2397.               (AND (PARTICULAR ?s) (PRE ?w0 ?s ?x ?t)))))
  2398.  
  2399. ; (T17)
  2400.   (forall (?w0 ?x ?t ?t1)
  2401.      (=> (AND (WORLD ?w0)
  2402.               (PARTICULAR ?x)
  2403.               (PARTICULAR ?t)
  2404.               (PARTICULAR ?t1)
  2405.               (PRE ?w0 ?x ?t)
  2406.               (P ?w0 ?t1 ?t))
  2407.          (PRE ?w0 ?x ?t1)))
  2408.  
  2409. ; (T18)
  2410.   (forall (?w0 ?x ?s ?t)
  2411.      (=> (AND (WORLD ?w0)
  2412.               (PARTICULAR ?x)
  2413.               (PARTICULAR ?s)
  2414.               (PARTICULAR ?t)
  2415.               (PRE ?w0 ?s ?x ?t))
  2416.          (PRE ?w0 ?x ?t)))
  2417.  
  2418. IST Project 2001-33052 WonderWeb:
  2419. Ontology Infrastructure FOR the Semantic Web
  2420.         12
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!