cwm makes bad proofs out of reverse built-ins

I found another bug. This time I isolated it to a test case:

cwm can run log:uri as a reverse built-in to bind ?X in:

{
  ?X log:uri "http://example#abc"
} => { ?X owl:differentFrom ?X }.

but with --why, the corresponding proof step is borked:

                         [
                                 a :Fact;
                                 :gives {<test/reason/revfunc.n3#X>
log:uri exa:abc .
                                } ] 

the ?X shouldn't stay in the proof; it should
get replaced by the result of the reverse function,
<http://example#abc>.

I checked in a test case:

swap$ python2.5 cwm.py test/reason/revfunc.n3 --think
--filter=test/reason/contradiction.n3 --why >,pf.n3
swap$ PYTHONPATH=.. python2.5 check.py ,pf.n3
                             Proof failed:  Built-in fact does not give
correct results: predicate: log:uri subject: X object: exa:abc result:
None 
   Proof invalid: Built-in fact does not give correct results:
predicate: log:uri subject: X object: exa:abc result: None 


looks to me like the problem is around
query.py line 1713:


                                return [(nb1, diag.tracking and
BecauseBuiltIn(con, subj, pred, result))
                                        for nb1, env3 in
subj.unify(result, Env(), Env(), self.neededToRun[SUBJ])]


subj is getting passed to BecauseBuiltIn, but what should
get passed is the result of unification.

That's as far as I got; I tried to figure out what unify()
returns in order to pass it to BecauseBuiltIn, but I got
lost in the code.

My kingdom for more doctests! (see check.py for at least
some examples.)


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

Received on Thursday, 17 December 2009 03:55:38 UTC