Proof generation / visualization for {:dan :homeRegion :Texas}

[Chimezie]

I have some experimental code for generating PML proof structures from
evaluated RETE-UL networks, The wiki below has a diagram of the proof
tree and the network used (both generated automatically). However, I'
m having a hard time reverse-engineering the reason.n3 -> PML rules in
order to serialize it to the reason.n3 format for check.py. Any
insights?

http://code.google.com/p/python-dlp/wiki/DanHomeProof

[jos....@agfa.com]

Hi Chime,

Am trying to refresh my memory first and was putting this case at
and retested it with EulerLibrary.java 1506

curl http://localhost/.euler52+--prolog+http%3A%2F%2Feulersharp.sourceforge.net%2F2007%2F07test%2Fgmpbnode.n3+--query+http%3A%2F%2Feulersharp.sourceforge.net%2F2007%2F07test%2FgmpbnodeF.n3 > gmpbnodeE1.n3

python check.py --report http://eulersharp.sourceforge.net/2007/07test/gmpbnodeE1.n3
seems to be happy with it

1: ...
[by parsing <gmpbnode.n3>]

2: @forSome var:e236762_12_ . :dan :home var:e236762_12_ .
[by erasure from step 1]

3: ...
[by parsing <gmpbnode.n3>]

4: @forSome var:e236762_12_ . var:e236762_12_ :in :Texas .
[by erasure from step 3]

5: ...
[by parsing <gmpbnode.n3>]

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

7: :dan :homeRegion :Texas .
[by rule from step 6 applied to steps [2, 4]
 with bindings {'REGION': u'<http://eulersharp.sourceforge.net/2007/07test/gmpbnode#Texas>', 'WHO': u'<http://eulersharp.sourceforge.net/2007/07test/gmpbnode#dan>', 'WHERE': '[...]'}]

8: :dan :homeRegion :Texas .
[by erasure from step 7]

9: ...
[by parsing <gmpbnodeF.n3>]

10: @forAll :REGION, :WHO . { :WHO gmp:homeRegion :REGION . } log:implies {:WHO gmp:homeRegion :REGION . } .
[by erasure from step 9]

11: :dan :homeRegion :Texas .
[by rule from step 10 applied to steps [8]
 with bindings {'REGION': u'<http://eulersharp.sourceforge.net/2007/07test/gmpbnode#Texas>', 'WHO': u'<http://eulersharp.sourceforge.net/2007/07test/gmpbnode#dan>'}]

12: :dan :homeRegion :Texas .
[by conjoining steps [11]]

     @prefix : <http://eulersharp.sourceforge.net/2007/07test/gmpbnode#> .
   
   :dan     :homeRegion :Texas .
   

I also tested with the e:true rule based version

curl http://localhost/.euler52+--prolog-bchain+http%3A%2F%2Feulersharp.sourceforge.net%2F2007%2F07test%2Fgmpbnode.n3+--query+http%3A%2F%2Feulersharp.sourceforge.net%2F2007%2F07test%2FgmpbnodeF.n3 > gmpbnodeE2.n3

but that is an experimental proof as we need different proof
possibilities (using bchain only) for the same conclusions
(http://eulersharp.sourceforge.net/GUIDE.html and
http://eulersharp.sourceforge.net/2006/02swap/etc5a.ref)

Jos

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

 
Chimezie <chim...@gmail.com>
Sent by: public-cwm-...@w3.org
2007-09-09 13:34 GMT

To: fuxi-discussion <fuxi-di...@googlegroups.com>
cc: public-...@w3.org
bcc: Jos De Roo/AMDUS/AGFA
Subject: Proof generation / visualization for {:dan :homeRegion :Texas}