(cl:comment 'TRANSLATION OF DOLCE 2.1 DELIVERABLE D17(V2.1) May 2003 INTO THE CLIF DIALECT OF ISO COMMON LOGIC AS SPECIFIED. NOTE THAT SOME DETAILS OF CLIF SYNTAX MAY BE CHANGED IN FORTHCOMING CORRIGENDA, IN PARTICULAR "cl-comment" WILL REPLACE "cl:comment".
FOR COMMENTS OR QUESTIONS, CONTACT PHAYES@IHMC.US')
(cl:comment 'THIS IS BASED ON THE KIF TRANSLATION, USING QUANTIFICATION OVER POSSIBLE WORLDS IN PLACE OF THE S5+BARCAN MODAL LOGIC. THIS VERSION USES SOME CL DEVICES TO ORGANIZE AND SHORTEN SOME OF THE AXIOMS, AND SIMPLIFIES THEM SOMEWHAT.
FOR EASE OF CROSS-REFERENCE, THE AXIOM LABELS CORRESPOND WHERE POSSIBLE TO THOSE USED IN THE KIF DOCUMENT.
THIS VERSION IS NOT YET COMPLETE
')
(cl:comment 'Since we are assuming S5 modality, all possible words are mutually accessible, so there is no need to introduce an explicit world-accessibility relation "wldr". If it were needed, a module would be the efficient way to define it in CL:
(cl-module World
(forall (x)(wldr x x))
(forall (x y)(if (wldr x y)(wldr y x)))
(forall (x y z)(if (and (wldr x y)(wldr y z))(wldr x z)))
)
(cl-import World)
The basic mapping of S5 into quantificational logic takes a simple atomic assertion (R a1 ... an) into the equivalent assertion make in the 'real' world (R Thisw a1 ... an) and a necessity operator into a simple universal quantifier over the world-parameter (which, following the KIF axioms, is here always the first argument.) This simplification also means that several of the axioms which quantify over an "origin world", usually indicated by w0, can be simplified, and some world-arguments omitted, for example in the definitions D1-12.
This also means that we can use a 'world-free' convention for SOME simple assertions, defined in the next axiom.')
(cl:comment 'no-world convention axiom'
(forall ((f Universal) x ...y)(if (not (World x))(iff (f x ...y)(f Thisw x ...y)) ))
)
(cl:comment 'ND1 and ND2 are included in the KIF for reasons which suggest that they are not needed in CL, but are included here for completeness. Note that these axioms actually prohibit any other universals, eg boolean combinations of these primitives. This is probably not intended, and can be overcome by modifying these axioms.
However, the purpose of having these 'explicit list' axioms is unclear. The authors of DOLCE seem to be under the impression that they are necessary for the logic of KIF to work, but this is certainly not the case for CL. I would suggest that the role of these axioms be carefully re-evaluated before use.
(forall (x)(iff (U x)(X f)))
(forall (x)(iff (X f)
(or (= f ALL)(= f AB)(= f R)(= f Tr)(= f T)(= f PR)(= f S)(= f AR)(= f Q)(= f TQ)(= f TL)(= f PQ)(= f SL)(= f AQ)(= f ED)(= f M)(= f PED)(= f F)(= f POB)(= f APO)(= f NAPO)(= f NPED)(= f NPOB)(= f MOB)(= f SOB)(= f ASO)(= f SAG)(= f SC)(= f NASO)(= f AS)(= f PD)(= f AV)(= f ACH)(= f ACC)(= f STV)(= f ST)(= f PRO) ) ))
')
(cl:comment 'The classifiers Particular, World and Universal apply to all their arguments, a useful convention which we can define as a "meta-property" in CLIF'
(forall (x)(if (Distributive x)(and (x)(forall y ...z)(if (x y ...z)(and (x y)(x ...z))))) ))
)
(Distributive Distributive)
(Distributive Particular Universal World)
(cl:comment 'To avoid needless typing, we will use shorter names. The name "P" is already reserved for the part-of relation.'
(= Particular Th)(= World W)(= Universal U)
(cl:comment 'ND6-12'
(forall (r w ...x)(if (and (r w ...x) (or (= r P)(= r K)(= r PC)(= r qt)(= r ql)))
(and (W w)(Th ...x))
))
)
(cl:comment 'NA1' (forall (x)(or (Th x)(U x)(W x))) )
(cl:comment 'NA2'
(forall (x)(and
(iff (Th x)
(not (or (U x)(W x))) )
(iff (U x)
(not (or (Th x)(W x))) )
(iff (W x)
(not (or (U x)(Th x))) )
))
)
(cl:comment 'NA14 & 15'
(forall ((w W)(f U))(and (NEP w f)) (if (X f)(RG w f)) ))
)
(cl:comment 'NA 16'
(forall ((w W)) (and (PT w ALL ED PD Q AB)
(PT w ED PED NPED AS)
(PT w PED M F POB)
(PT w POB APO NAPO)
(PT w NPOB MOB SOB)
(PT w SOB ASO NASO)
(PT w ASO SAG SC)
(PT w PD EV STV)
(PT w EV ACH ACC)
(PT w STV ST PRO)
(PT w Q TQ PQ AQ)
(PT w R TR PR AR) ))
)
(cl:comment 'NA17'
(forall ((w W)) (and (SB w ALL ED) (SB w ALL PD) (SB w ALL Q) (SB w ALL AB)
(SB w ED PED) (SB w ED NPED) (SB w ED AS)
(SB w PED M) (SB w PED F) (SB w PED POB)
(SB w POB APO) (SB w POB NAPO)
(SB w NPED NPOB)
(SB w NPOB MOB) (SB w NPOB SOB)
(SB w SOB ASO) (SB w SOB NASO)
(SB w ASO SAG) (SB w ASO SC)
(SB w PD EV) (SB w PD STV)
(SB w EV ACH) (SB w EV ACC)
(SB w STV ST) (SB w STV PRO)
(SB w Q TQ) (SB w Q PQ) (SB w Q AQ)
(SB w TQ TL)
(SB w PQ SL)
(SB w AB FACT) (SB w AB SET) (SB w AB R)
(SB w R TR) (SB w R PR) (SB w R AR)
(SB w TR T)
(SB w PR S)))
)
(cl:comment 'NA 18 - 21 are not needed as we use functional notation.')
(cl:comment 'D1-12 are simplified in a uniform way, by omitting the w0 "origin world", which is not needed, cf earlier comment. Note this removes one argument. All these relations are now relations on universals, a fact which we can state explicitly in a single axiom.'
(forall (f ...x y)(if
(and (f ...x)(or (= f RG)(= f NEP)(= f DJ)(= f SB)(= f EQ)(= f L)(= f SBL)(= f PSBL)(= f (L. y))(= f (SBL. y)(= f (PSBL. y)))
(U ...x)
)
)
(cl:comment 'D1 Rigid Universal'
(forall (f) (iff (RG f)(forall ((w W)(x Th))(if (f w x)(forall ((u W))(f u x)))) ))
)
(cl:comment 'D2 Nonempty Universal'
(forall (f)(iff (NEP f)(forall ((w W))(exists ((y Th))(f w y))) ))
)
(cl:comment 'D3 Disjoint Universals'
(forall (f g)(iff (DJ f g)
(forall ((w W)(x Th))(not (and (f w x)(g w x))))
))
)
(cl:comment 'D4 Subsumption'
(forall (f g)(iff (SB f g)
(forall ((w W)(x Th))(if (g w x)(f w x)))
))
)
(cl:comment 'D5 Equal Universal'
(forall (f g)(iff (EQ f g)(and (SB f g)(SB g f)) ))
)
(cl:comment 'D6 Proper SB'
(forall (f g)(iff (PSB f g)(and (SB f g)(not (SB g f))) ))
)
(cl:comment 'D7 Leaf Universal'
(forall (f )(iff (L f) (forall ((g U))(if (SB f g)(EQ f g)) ) ))
)
(cl:comment 'D8 Leaf Subsume'
(forall (f g)(iff (SBL f g)(and (SB f g)(L g)) ))
)
(cl:comment 'D9 Leaf Proper Subsume'
(forall (f g)(iff (PSBL f g)(and (PSB f g)(L g)) ))
)
(cl:comment 'The KIF axioms "cheat" by using an external-to-KIF dot convention to represent subscripting a relation name with a parameter. CL can do this honestly by using a function from parameters to relations. We will write (SBL. X) - that is, the function SBL. applied to the argument X - instead of SBL.X, therefore, and similarly with the other two "dotted" conventions.')
(cl:comment 'D10 Leaf In Set X'
(forall (f X)(iff ((L. X) f)(and (X f)(forall ((g U))(if (and (SB f g)(X g))(EQ f g))) ))
)
(cl:comment 'D11 SBL.'
(forall (f g X)(iff ((SBL. X) f)(and (SB f g)((L. X) g) )))
)
(cl:comment 'I think this and the previous axiom may be wrong, but they are here transcribed as written. The SB and PSB assertions are not here relativized to the set X, and the meaning would change if they were.'
(cl:comment 'D12 PSBL.'
(forall (f g X)(iff ((PSBL. X) f)(and (PSB f g)((L. X) g) )))
)
)
(cl:comment 'D13, included for comparison. The KIF version is almost certainly incorrect as written, but the intention is clear. This version is based directly on the modal version of the axiom.'
(forall (f ...g)(iff (PT f ...g)
(and (Exclusive ...g)(forall (x (w W))(if (f w x)((OneOf ...g) w x))) )
))
)
(cl:comment 'auxiliary defns for D13'
(forall (x y ...z)(and (Exclusive x)
(iff (Exclusive x y ...z)(and (not (= x y))(Exclusive x ...z)(Exclusive y ...z)))
))
(forall (f ...g ...a)(and (not ((OneOf) ...a))
(iff ((OneOf f ...g) ...a)(or (f ...a)((OneOf ...g) ...a)))
))
)
(cl:comment 'MEREOLOGY')
(cl:comment 'The mereology axioms in FOL are written as simple (non-modal) definitions, but the KIF versions universally quantify the world-parameter, which makes them into necessary truths rather than simple axioms. Here we follow the KIF.')
(cl:comment 'D14 Proper Part'
(forall ((x Th)(y Th)(w W))(iff (PP w x y)(and (P w x y)(not (P w y x))) ))
)
(cl:comment 'D15 Overlap'
(forall ((x Th)(y Th)(w W))(iff (O w x y)(exists (z)(and (P w z y) (P w z x)) ))
)
(cl:comment 'D16 Atom'
(forall ((x Th)(w W))(iff (At w x)(not (exists (y)(PP w y x))) ))
)
(cl:comment 'D17 AtomicPart'
(forall ((x Th)(y Th)(w W))(iff (AtP w x y)(and (At w x)(P w x y)) ))
)
(cl:comment 'D18 Binary Sum is here treated as a function, which avoids the need to state uniqueness explicitly.'
(forall ((w W)(x Th)(y Th)(u Th))(iff (O w (+ w x y) u)(or (O w x u)(O w y u)) ))
)
(cl:comment 'D18a To allow the use of the relational form, add a conversion axiom.
(forall ((w W)(x Th)(y Th)(z Th))(iff (= z (+ w x y)) (+ w x y z) ))
)
(cl:comment 'D19 General Sum. General sum is here described as a function on a predicate, rather than as a variable-binding operator.'
(forall ((w W)(x Th)(f U))(iff (O w (sigma f) x)(exists (y)(and (O w y x)(f y))) ))
)
(cl:comment 'D20-23 temporary mereology. This axioms could be combined with D14-D17 using a sequence marker, but we will here follow the KIF form.'
(forall ((x Th)(y Th)(w W)(t Th))(iff (PP w x y t)(and (P w x y t)(not (P w y x t))) ))
(forall ((x Th)(y Th)(w W)(t Th))(iff (O w x y t)(exists (z)(and (P w z y t) (P w z x t)) ))
(forall ((x Th)(w W)(t Th))(iff (At w x t)(not (exists (y)(PP w y x t))) ))
(forall ((x Th)(y Th)(w W)(t Th))(iff (AtP w x y t)(and (At w x t)(P w x y t)) ))
)
(cl:comment 'D24 Coincidence.'
(forall ((x Th)(y Th)(w W)(t Th))(iff (equal.t w x y t)(and (P w x y t)(P w y x t)) ))
)
(cl:comment 'D25 Constant Part'
(forall ((w W)(x Th)(y Th))(iff (CP w x y)
(and (exists ((t Th))(PRE w y t))
(forall ((t Th))(if (PRE w y t)(P w x y t)))
) ))
)
(cl:comment 'D26 is the temporal version of binary sum, and again is treated here as a function.'
(forall ((w W)(x Th)(y Th)(u Th)(t Th))(iff (O w (+.t w x y t) u t)(or (O w x u t)(O w y u t)) ))
)
(cl:comment 'D27 similarly follows D19.'
(forall ((w W)(x Th)(f U)(t Th))(iff (O w (sigma.t f t) x t)(exists (y)(and (O w y x t)(f y))) ))
)
(cl:comment 'D28 Direct Quality'
(forall ((x Th)(y Th)(w W))(iff (dqt w x y)(not (exists ((z Th))(and (qt w x z)(qt w y z)))) ))
)
(cl:comment 'D29 Quality of type'
(forall ((x Th)(y Th)(f U))(iff (qtf w f x y)(and (qt w x y)(f w x)((SBL. X) w Q f)) ))
)
(cl:comment 'D30 Temporal/spatial Quale'
(cl:comment 'I have absolutely no idea what this is supposed to mean or how it relates the philosophical notion of "quale" (which has to do with perception and phenomenology).'
(forall ((t Th)(x Th)(w W)(iff (ql.T.PD w t x)(and (PD w x)(exists ((z Th))(and (qtf w TL z x)(ql w t z)))) ))
)
)
(cl:comment 'D31. THIS AXIOM IS OMITTED as the version in the KIF text makes no sense. I suspect that the parameter ?t has been omitted from an argument somewhere, but have no way to reconstruct the correct version.')
(cl:comment 'END OF CURRENT DRAFT, INCOMPLETE')