W3C home > Mailing lists > Public > www-rdf-logic@w3.org > September 2003

Re: evidence for forall? [was: test based on OWL guide...]

From: Jos De_Roo <jos.deroo@agfa.com>
Date: Fri, 26 Sep 2003 01:01:02 +0200
To: "Dan Connolly <connolly" <connolly@w3.org>
Cc: Pat Hayes <phayes@ai.uwf.edu>, www-rdf-logic@w3.org
Message-ID: <OF17605BB2.78D96AE2-ONC1256DAC.007C175F-C1256DAC.007E75AE@agfa.be>


DanC wrote:
> Ouch; my brain hurts...

well, mine too (but for another reason - severe headache - I took
an aspirin and it's now better...)

> On Thu, 2003-09-25 at 16:41, Jos De_Roo wrote:
> [...]
> > no need for quantifiers in a language of logic of proof;
> > they belong to the object language of predicate logic
> > and they are for instance explicitly mentioned in proof
> > term
> > -->term<--
> >  { { [ iw:Variable "?X" ] = :socrates.
> >      [ iw:Variable "?X" ] a :Man } =>
> >    { :socrates a :Man } }  =>
> > { :socrates a :Mortal }.
> > which is a proof of
> > -->:formula<--
> > :socrates a :Mortal.
> >
> > hmm...
>
> hmm... is that term a proof of { :socrates a :Mortal } from
> no premises? Or is the proof term a sort of function
> that takes a proof of
>  { ?X a :Man } => { ?X a :Mortal }.
> and a proof of
>  :socrates a :Man.
> and returns a proof of
>  :socrates a :Mortal.
> ?

Actually we always add a uri rule identifier to the premises
e.g. { :rule123. ?X a :Man } => { ?X a :Mortal }.
and so make the connection that way in the proof term
 {
  :rule123.
   {[iw:Variable "?X"] = :socrates.
    [iw:Variable "?X"] a :Man} =>
  {:socrates a :Man}}  =>
{:socrates a :Mortal}.

which is intended to mean
given
  :rule123.
and (appying unification)
  :socrates a :Man.
then we *resolved* (applying resolution)
  :socrates a :Mortal.

Maybe we should be more explicit...


--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Thursday, 25 September 2003 19:01:23 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:52:47 GMT