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