rule application proof step and existentials

Back in September,
http://lists.w3.org/Archives/Public/public-cwm-talk/2006JulSep/0009.html

I pointed out something wierd with this case:
---8<---
@prefix : <gmpbnode#>.
@keywords is, of, a.

dan home [ in Texas ].

{ ?WHO home ?WHERE.
  ?WHERE in ?REGION } => { ?WHO homeRegion ?REGION }.

---8<---

Yosi fixed that problem, today, we think. (Yay!)

But while he was at it, he came up with this twist:

--8<--
@prefix : <gmpbnode#>.
@keywords is, of, a.
dan a Man; home [].
{ ?WHO home ?WHERE.
  ?WHERE in ?REGION } => { ?WHO homeRegion ?REGION }.
{ dan home ?WHERE} => {?WHERE in Texas} . 
--8<--

"What should the proof look like?" He asked me. I thought
I knew the answer:

1. ... by parsing.
2. dan home [], by extraction from 1
3. { dan home ?WHERE} => {?WHERE in Texas} . by extraction.
4. dan home [ in Texas] by rule on 3 applied to 2
5. ... => { ?WHO homeRegion ?REGION }. by extraction from 1
6. dan homeRegion Texas by rule from line 5 applied to 4
QED.


But it's more subtle than that.

We're pretty sure the proof can't actually be expressed
using the structures we've been working with so far.

I'm curious about what Euler does in this case.

What follows is a trace that Yosi generated today with his
new cwm bits, and then a transcript of our actual discussion.

syosi@mr-burns:~/cvs-trunk/WWW/2000/10/swap/test/reason$
python ../../check.py --report /tmp/2.pf
1: @forAll :REGION, :WHERE, :WHO. @forSome foo:_g2 . gmp:dan a gmp:Man;
gmp:home foo:_g2 . { gmp:dan gmp:home :WHERE . } log:implies {:WHERE
gmp:in gmp:Texas . } . { :WHERE gmp:in :REGION . :WHO
gmp:home :WHERE . } log:implies {:WHO gmp:homeRegion :REGION . } .
 [by parsing <double.n3>]

2: @forSome foo:_g2 . :dan :home foo:_g2 .
 [by erasure from step 1]

3: @forSome foo:_g2 . :dan :home foo:_g2 .
 [by erasure from step 1]

4: @forAll dou:WHERE . { :dan :home dou:WHERE . } log:implies
{dou:WHERE :in :Texas . } .
 [by erasure from step 1]

5: ...
 [by rule from step 4 applied to steps [3]
  with bindings {'WHERE': '[...]'}]

6: @forSome foo:_g2 . foo:_g2 :in :Texas .
 [by erasure from step 5]

7: @forAll :REGION, :WHERE, :WHO . { :WHERE gmp:in :REGION . :WHO
gmp:home :WHERE . } log:implies {:WHO gmp:homeRegion :REGION . } .
 [by erasure from step 1]

8: :dan :homeRegion :Texas .
 [by rule from step 7 applied to steps [2, 6]
  with bindings {'REGION':
'<file:///home/syosi/cvs-trunk/WWW/2000/10/swap/test/reason/gmpbnode#Texas>', 'WHO': '<file:///home/syosi/cvs-trunk/WWW/2000/10/swap/test/reason/gmpbnode#dan>', 'WHERE': '[...]'}]

9: @forAll dou:REGION, dou:WHERE, dou:WHO. @forSome foo:_g2 . :dan
a :Man; :home foo:_g2; :homeRegion :Texas . foo:_g2 :in :Texas .
{ :dan :home dou:WHERE . } log:implies {dou:WHERE :in :Texas . } .
{ dou:WHERE :in dou:REGION . dou:WHO :home dou:WHERE . } log:implies
{dou:WHO :homeRegion dou:REGION . } .
 [by conjoining steps [8, 1, 5]]

     @prefix :
<file:///home/syosi/cvs-trunk/WWW/2000/10/swap/test/reason/double.n3#> .
    @prefix gmp:
<file:///home/syosi/cvs-trunk/WWW/2000/10/swap/test/reason/gmpbnode#> .
    @prefix log: <http://www.w3.org/2000/10/swap/log#> .

     @forAll :REGION,
                :WHERE,
                :WHO.
         @forSome :_g_L3C17 .

    :_g_L3C17     gmp:in gmp:Texas .

    gmp:dan     a gmp:Man;
         gmp:home :_g_L3C17;
         gmp:homeRegion gmp:Texas .
    {
        gmp:dan     gmp:home :WHERE .

        }     log:implies {:WHERE     gmp:in gmp:Texas .
        } .
    {
        :WHERE     gmp:in :REGION .
        :WHO     gmp:home :WHERE .

        }     log:implies {:WHO     gmp:homeRegion :REGION .
        } .



<yosi_s> DanC, I think I have cwm not splitting bNodes in proofs
<yosi_s> tests are running
<DanC> ooh!
<DanC> very timely
<DanC> I just checked in some xml/xpath related stuff. I wasn't as
careful as perhaps I should have been about running tests before I
checked it in
<yosi_s> the problem was that there was no preexissting way in cwm to
get a formula containing a specific set of triples
<yosi_s> which is what was needed
<yosi_s> this has now been changed
<yosi_s> it is, perhaps, not perfect
* yosi_s thinks about how to break it
<yosi_s> hmm...
<yosi_s> [[
<yosi_s> @prefix : <gmpbnode#>.
<yosi_s> @keywords is, of, a.
<yosi_s> dan a Man; home [].
<yosi_s> { ?WHO home ?WHERE.
<yosi_s>   ?WHERE in ?REGION } => { ?WHO homeRegion ?REGION }.
<yosi_s> { dan home ?WHERE} => {?WHERE in Texas} . 
<yosi_s> ]]
<yosi_s> what should the proof look like?
<yosi_s> DanC?
* DanC tunes in...
<DanC> 1. parsing. 2. dan home [], by extraction from 1
<DanC> 3. { dan home ?WHERE} => {?WHERE in Texas} . by extraction. 4.
dan home [ in Texas] by rule on 3 applied to 2
<DanC> 5. ... { ?WHO homeRegion ?REGION }. by extraction from 1
<DanC> 6. dan homeRegion Texas by rule from line 5 applied to 4
<DanC> QED.
<yosi_s> ok. Here we have a problem. Cwm will generate: 4. [ in Texas ]
<DanC> well, that's clearly bogus...
<DanC> ... does it have dan home [] in evidence at step 6?
* DanC wonders if that question is at all clear
* yosi_s is trying to find a way to send the output of check --report
<yosi_s> http://pastebin.ca/354204
<yosi_s> yes DanC, it does have that in evidence
* DanC sees http://pastebin.ca/354204
<DanC> lines 2 and 6 are split, bogusly
<DanC> #
<DanC> 8: :dan :homeRegion :Texas .
<DanC> #
<DanC>  [by rule from step 7 applied to steps [2, 6
<DanC> ew... is cwm's reasoning unsound altogether?
<DanC> lines 2 and 6 have different justifications, which suggests they
_should_ be split.
<yosi_s> that was my point
<DanC> is this a case of one triple having 2 justifications, and cwm
getting confused as a result?
<yosi_s> no
<yosi_s> every triple has one justification in this example
<yosi_s> but the fact that dan lives somewhere, and that that somewhere
is in Texas, have different justifications
* DanC thinks about what the proof should be a little harder...
<DanC> the rule { dan home ?WHERE} => {?WHERE in Texas} can't conclude 2
triples on my line 4, can it.
<DanC> ouch. my head is exploding.
<yosi_s> welocome to my world
<yosi_s> welcome
<DanC> there's some wierd skolemization going on somewhere in cwm's
reasoning... or something.
<yosi_s> the problem is not the reasoning
<yosi_s> the problem is the expressivity of the proof format
<DanC> I think this example goes beyond the proof structures we have so
far. right.
<yosi_s> I don't see how to fix this --- n3 is not sufficiently
introspective
<DanC> cwm should probably throw an exception when asked to generate a
proof in this case, for now. file a bug or something.
<DanC> meanwhile, the code you've got is no worse than what we had
before, and in some cases better, yes?
<DanC> agenda+ moving from cvs to hg
<DanC> agenda+ moving swap from cvs to hg
<yosi_s> yes
<yosi_s> I had introduced a bug
<yosi_s> rerunning tests
<DanC> how does cwm know/decide to unify the conclusion of { dan
home ?WHERE} => {?WHERE in Texas} with dan home []? that has me puzzled.
--> [DiG]Tratonis (n=odintg@i577A94A0.versanet.de) has joined #dig
<DanC> I bet it has to re-open a formula to do that.
<yosi_s> that was not hard at all for cwm
<yosi_s> the bNode is a constant
<yosi_s> it simply does the right thing
<yosi_s> we only run into a problem because cwm is trying to represent a
bNode with a bNode in the proof, and it's not working
<DanC> "the bNode is a constant" <- that's skolemization, in a nutshell.
<yosi_s> yes
<yosi_s> -- committed



-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E

Received on Wednesday, 14 February 2007 02:33:37 UTC