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