ontolog-forum
[Top] [All Lists]

## Re: [ontolog-forum] CLIF as a sorted logic?

 To: "[ontolog-forum] " Pat Hayes Wed, 11 Aug 2010 23:37:42 -0500
 ```Sorry for the delay in responding (due to a delay in reading).    (01) Guarded quantification has the form - let me stick to just the existential to keep things simple - (exists (x)(and (g x ...)(S x ...))) where the 'guard' expression (g x ...) must contain *all the variables that are free in S*, even if they aren't bound by the quantifier.    (02) A restricted quantifier is simpler: it has the form (exists (x)(and (r x)(S x ...))) where the restriction (r x) needs only mention the variable being quantified.    (03) So for example, this sentence is restricted:    (04) (forall (x)(if (Human x)(exists (y)(and (Human y)(Mother x y))) ))    (05) and indeed is the 'expansion' of the restricted-quantifier version    (06) (forall ((x Human))(exists ((y Human))(Mother x y))    (07) but it is not guarded. In order to make it a guarded sentence, you would have to replace the 'inner' Human by a two-argument relation of some kind to act as a guard, such as:    (08) (forall (x)(if (Human x)(exists (y)(and (SameGenus x y)(Mother x y))) ))    (09) As Chris points out, guarded logic (logic with all the quantifiers guarded) have all kinds of fascinating properties (they are decideable, for a start) and connections with modal, temporal and hybrid logics, and are a huge topic of current (well, no more than a decade old) research in logic. Restricted quantification, by contrast, is old, boring and suitable for standardization.    (010) Pat    (011) On Aug 5, 2010, at 4:47 AM, Christopher Menzel wrote:    (012) > On Aug 3, 2010, at 5:29 PM, Obrst, Leo J. wrote: >> John, Chris, >> >> Is this the same as guarded quantification? > > It's sort of a limiting case. The term "guarded quantification" is > usually used in the context of rather advanced studies in modal > logic, finite model theory, etc where the issue of complexity vs > expressibility comes to the fore. The idea in these contexts is > typically to add guarded quantifiers to some fragment of first-order > logic (yielding a so-called "guarded fragment" of FOL) and explore > its computational and model theoretic properties. In the definition > of typed quantification that I gave, I put no restrictions on the > formulas that can serve as the "guard" F in a guarded quantifier. > In the study of guarded fragments, the complexity of the guard F is > highly relevant. In some contexts, for example, the guards might be > restricted to atomic formulas. > > There has been a great deal of research recently on guarded > fragments in the study of modal logic (which, recall, can be > represented as fragments of FOL), which has made them quite relevant > to the study of OWL (as OWL can itself be represented as a modal > logic). > > Pat did some work on guarded fragments a while ago and might be able > to add more here. > > -chris > > > _________________________________________________________________ > Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/ > Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/ > Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx > Shared Files: http://ontolog.cim3.net/file/ > Community Wiki: http://ontolog.cim3.net/wiki/ > To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J > To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx > >    (013) ------------------------------------------------------------ IHMC (850)434 8903 or (650)494 3973 40 South Alcaniz St. (850)202 4416 office Pensacola (850)202 4440 fax FL 32502 (850)291 0667 mobile phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes    (014) _________________________________________________________________ Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/ Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/ Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx Shared Files: http://ontolog.cim3.net/file/ Community Wiki: http://ontolog.cim3.net/wiki/ To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (015) ```
 Current Thread Re: [ontolog-forum] owl2 and cycL/cycML, (continued) Re: [ontolog-forum] owl2 and cycL/cycML, Adrian Walker [ontolog-forum] CLIF as a sorted logic?, Adam Pease Re: [ontolog-forum] CLIF as a sorted logic?, Christopher Menzel Re: [ontolog-forum] CLIF as a sorted logic?, John F. Sowa Re: [ontolog-forum] CLIF as a sorted logic?, Jawit Kien Re: [ontolog-forum] CLIF as a sorted logic?, Obrst, Leo J. Re: [ontolog-forum] CLIF as a sorted logic?, Christopher Menzel Re: [ontolog-forum] CLIF as a sorted logic?, John F. Sowa Re: [ontolog-forum] CLIF as a sorted logic?, Rick Murphy Re: [ontolog-forum] CLIF as a sorted logic?, John F. Sowa Re: [ontolog-forum] CLIF as a sorted logic?, Pat Hayes <= [ontolog-forum] Reasoning in Reality - was owl2 and cycL/cycML, Rich Cooper Re: [ontolog-forum] Reasoning in Reality - was owl2 and cycL/cycML, Adrian Walker Re: [ontolog-forum] Reasoning in Reality - was owl2 and cycL/cycML, Rich Cooper Re: [ontolog-forum] Reasoning in Reality - was owl2 and cycL/cycML, Adrian Walker Re: [ontolog-forum] Reasoning in Reality - was owl2 and cycL/cycML, Adrian Walker Re: [ontolog-forum] owl2 and cycL/cycML, doug foxvog Re: [ontolog-forum] owl2 and cycL/cycML, Rich Cooper Re: [ontolog-forum] owl2 and cycL/cycML, Zhuk, Yefim Re: [ontolog-forum] owl2 and cycL/cycML, Ian Horrocks Re: [ontolog-forum] owl2 and cycL/cycML, John F. Sowa