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

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?

Yup.

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

Cheers,

Miles
```

 News | XML in Industry | Calendar | XML Registry Marketplace | Resources | MyXML.org | Sponsors | Privacy Statement Copyright 2001 XML.org. This site is hosted by OASIS