- From: pat hayes <phayes@ai.uwf.edu>
- Date: Wed, 29 Aug 2001 16:00:13 -0700
- To: jos.deroo.jd@belgium.agfa.com
- Cc: w3c-rdfcore-wg@w3.org
>Hi Pat,
>
> > > > In danger of making another mistake ....
> > > >
> > > > I didn't quite see how the interpolation lemma worked when the LHS has
> > > > anonymous nodes.
> > > >
> > > > How does it get the following entailment
> > > >
> > > >
> > > > _:x <b> <c> .
> > > >
> > > >
> > > > entails
> > > >
> > > > _:y <b> <c> .
> > >
> > >I just see that we have a bug in our stuff...
> > >for
> > > _:x <b> <c>. |=> _:y <b> <c>.
> > >we assert LHS and query it with RHS
> > >and i think we should query with
> > > {_:y <b> <c>} log:forAll _:y.
> > >and then there is a match found with
> > > {_:x <b> <c>} log:forSome _:x.
> > >(i have to think about that, and try...)
> >
> > That seems right to me. The log:forAll on the RHS tells the reasoner
> > it is free to substitute anything for the variable, right?
>
>Well I think I was wrong with that forAll
>that entailment doesn't seem to make sense
>We have it now like
Right. Sorry, I was thinking in theorem-proving mode (my native
language) where one thinks of the consequent as pre-negated, as it
were, so everything is inverted (forall <--> exists, and<-->or).
Never mind......
>
>and BTW for so called 'variable' predicates we find
>your MT thing/extension distinction really wonderful!
Yes, thats why we used it in the 'new KIF' , so we could quantify
over relations freely. Its wonderfully liberating, you can do about
anything in the syntax and it always makes reasonable sense. Chris
Menzel calls it 'wild west syntax'. You can write things like (P (P
P)) which is a relation applied to a function applied to an object,
all the same thing! You can even write things like ((P P) P) and
(exists (?x)((?x ?x)(?x ?x))) which would make anyone with a
traditional logical upbringing have nightmares.
Pat
---------------------------------------------------------------------
(650)859 6569 w
(650)494 3973 h (until September)
phayes@ai.uwf.edu
http://www.coginst.uwf.edu/~phayes
Received on Wednesday, 29 August 2001 18:59:11 UTC