Re: [closed] pfps-05

From: pat hayes <phayes@ai.uwf.edu>
Subject: Re: [closed] pfps-05
Date: Fri, 30 May 2003 17:34:35 -0500

> >From: "Jos De_Roo" <jos.deroo@agfa.com>
> >Subject: Re: [closed] pfps-05
> >Date: Fri, 30 May 2003 13:21:49 +0200
> >
> >>
> >>  [removed www-rdf-comments from the cc and added w3c-rdfcore-wg]
> >>
> >>  > For example, I am currently unable to determine whether the following
> >>  > entailment
> >>  >
> >  > >      ex:foo ex:prop "a"^^foo:bar  .
> >>  >
> >>  >          entails

		^^^ implies in the RDF closure rules

> >>  >      ex:foo ex:prop _:x  .
> >>  >      _:x rdf:type rdfs:Resource .
> >>
> >>  Using appropriate namespace prefixes
> >>
> >>  @prefix ex: <http://example.org/ex#>.
> >>  @prefix foo: <http://example.org/foo#>.
> >>
> >>  I have found that entailment working
> >>
> >>  ex:foo ex:prop "a"^^foo:bar.
> >>  "a"^^foo:bar rdf:type rdfs:Resource.
> >>
> >>  --
> >>  Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
> >
> >I am *not* asking whether some piece of software produces the result.  I am
> >instead asking whether an entailment holds.
                             ^^^^ inference

> Sigh. The entailment is trivial:
> 
> ex:foo ex:prop "a"^^foo:bar  .
> ex:foo ex:prop _:x .		by rule se1
> _:x rdf:type rdfs:Resource  .	by rule rdfs4a

This is not an application of rule rdfs4a.

> Similar entailments follow a similar route.  The SE rules apply to 
> any literal form.
> 
> However, I doubt if this will satisfy you, since there are infinitely 
> many other entailments you might fail to be convinced of, and you are 
> apparently unwilling to accept that entailments might be checkable by 
> software.
> 
> Pat

On the contrary, software is an excellent method for determining if an
inference follows, so long as the software emits a proof that can then be
checked.  Software is also an excellent method for determining if an
entailment does not hold, so long as the software emits a counterexample.
The situation is somewhat different when the proofs and counterexamples
become very large, but we are certainly nowhere near that stage yet.

For other purposes, software is much less suitable, although, with
appropriate safeguards, it is possible to actually use software to
determine that an inference does not follow or an entailment holds.

Peter F. Patel-Schneider
Bell Labs Research 
Lucent Technologies

Received on Saturday, 31 May 2003 10:30:43 UTC