OASIS Mailing List ArchivesView the OASIS mailing list archive below
or browse/search using MarkMail.


Help: OASIS Mailing Lists Help | MarkMail Help



   Re: [xml-dev] Semantic Web and First Order Logic

[ Lists Home | Date Index | Thread Index ]

Thomas B. Passin wrote,
> [Miles Sabin]
> > This is easy to express in second-order logic, or in first-order
> > logic plus set theory (the "plus set theory" bit means that you can
> > forget about decidability). Not so easy in plain first-order logic.
> Hmm, it depends on your definition of FOL, I suppose, and it also
> depends on how you model things.  I assumed that FOL includes types
> and your "plus set" stuff

Those'd be first-order theories (ie. they're expressed in first-order 
logic) but they're not first-order logic. And they're not necessarily 
decidable (a type theory might be, set theory isn't).

> (but a set of individuals is a kind of quantifier over individuals, is
> it not?).

In first-order set-theory a set of individuals is an individual in it's 
own right, not a quantifier.

> I take it that in FOL, quantifiers range over individuals while in
> second order logic, quantifiers can range over predicates and
> relations. Is that what you understand?

More or less.

> Applying this to your example,  if you used Red(widget), then your
> statement would be about the predicate (ie., Red), and therefore
> second order, right?


> But the redness can be modeled in other ways.

Oh, sure. I mentioned one: first-order logic plus set-theory.

> For example, we could say Color(x,red) and IsPrimaryColor(red).  Then
> your example could be stated something like this -
> {for all x,y| Widget(x) and Color(x,y) and IsPrimaryColor(y)}==>
> Surcharge(x,5%)
> {Widget(x) and Color(x,red)}
> {IsPrimaryColor(red)}
> Now we are only making statements about the arguments, and they are
> individuals, not predicates or relations.  So it is FOL, right? And
> an SQL query could extract the surcharge from a database.

It's a first-order _theory_, but it's not first-order _logic_. Chances 
are that the first-order theory of widget-colour-surchages will be 
decidable, but that's not true of first-order theories in general: viz. 
arithmetic, set-theory ...

And this is where the constraint that Len was complaining about bites: 
the base-level logical frameworks being considered for the SW insist on 
decidability, and that excludes many practically useful, tho' formally 
undecidable first-order theories.

Here's something else you might try to first-orderize nicely,

  Some widgets attach only to one another

You can express this is second-order logic,

  {exists P | 
    {exists x | Px } and
    {for all x | 
      Px ==>
        Widget(x) and {for all y | attach(x, y) ==> Py } } }

and you can express it in first-order set theory,

  {exists X |
    {exists x | member(x, X) } and
    {for all x |
      member(x, X) ==>
        Widget(x) and {for all y | attach(x, y) ==> member(y, X) } } }

but neither second-order logic nor first-order set theory are decidable, 
so neither of these renderings is compatible with the frameworks touted 
for the SW which respect the decidability constraint. Can you come up 
with a rendering which is?

OTOH, can you persuade me that this kind of assertion is irrelevant to 
business applications? All it's doing is saying that there's a binary 
relation ("attach" in the example) which partitions the domain of 
widgets in a particular way. That seems like a useful kind of thing to 
be able to say.




News | XML in Industry | Calendar | XML Registry
Marketplace | Resources | MyXML.org | Sponsors | Privacy Statement

Copyright 2001 XML.org. This site is hosted by OASIS