- From: Sandro Hawke <sandro@w3.org>
- Date: Tue, 22 Apr 2003 23:14:39 -0400
- To: www-rdf-logic@w3.org
I've been looking over TimBL's implementation of "--why" in cwm, which
instructs cwm to present an explanation of its process. The
explanation is currently in the form of an RDF description of the
proof tree cwm develops using its normal forward-chaining process.
The vocabulary, with some documentation is at
http://www.w3.org/2000/10/swap/reason
There's a related issue of how you describe the RDF graphs/formulas
being related by proof steps. By default cwm uses its {...} formula
literals, but this clearly is not RDF. This implementation
uses a bit of
http://www.w3.org/2000/10/swap/reify
to provide referencial opacity, and could use one of the
implementations of --flatten cwm has had from time to time. I know of
other work on reifying FOL formulas for transmission via RDF by
McDermott & Dou, Deborah McGuinness, and myself; I'm hoping Common
Logic will provide a form for unifying that area.
Anyway, I've attached some demonstration runs below. The output is
IMHO quite hard to read (and I'm pretty comfortable with N3). This
is not an explanation for end-users yet, but I think we're more
interested in proof exchange for machine consumption (verification)
right now anyway.
I know McGuinness et al have done some work in this area [1], and I'm
hoping to coordinate with them more. Is anyone else working in this
area?
-- sandro
[1] http://www.ksl.stanford.edu/software/IW/
---------
Script started on Tue 22 Apr 2003 07:54:34 PM EDT
bash-2.05b$ cwm rules-simple.n3
#Processed by Id: cwm.py,v 1.129 2003/04/08 16:12:43 timbl Exp
# using base file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3
# Notation3 generation by
# notation3.py,v 1.137 2003/04/08 16:12:44 timbl Exp
# Base was: file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3
@prefix : <#> .
@prefix daml: <http://www.daml.org/2001/03/daml+oil#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .
this log:forAll :X .
:Joe :likes :easterEggs .
{
:Joe :likes :X .
} log:implies {:X :madeof :chocolate .
} .
#ENDS
bash-2.05b$ cwm rules-simple.n3 --why
#Processed by Id: cwm.py,v 1.129 2003/04/08 16:12:43 timbl Exp
# using base file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3
@@@@@@@ Proof of 0_work is <why.FormulaReason instance at 0x8361f5c>
@@@@@@ notation3 167 loading file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3 <why.BecauseOfCommandLine instance at 0x8379254> 0_work
Now: 169 <why.BecauseOfCommandLine instance at 0x8379254> <why.FormulaReason instance at 0x8361f5c> 0_work
# Notation3 generation by
# notation3.py,v 1.137 2003/04/08 16:12:44 timbl Exp
# Base was: file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3
@prefix : <#> .
@prefix daml: <http://www.daml.org/2001/03/daml+oil#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix n3: <http://www.w3.org/2000/10/swap/reify#> .
@prefix reason: <http://www.w3.org/2000/10/swap/reason#> .
@prefix run: <.run-1051055701.352555p22427#> .
this log:forSome :_g0 .
[ a reason:Conjunction,
reason:Proof;
reason:component [
a reason:Extraction;
reason:because :_g0;
reason:gives {this log:forAll :X .
{
:Joe :likes :X .
} log:implies {:X :madeof :chocolate .
} .
} ],
[
a reason:Extraction;
reason:because :_g0;
reason:gives {:Joe :likes :easterEggs .
} ];
reason:gives {this log:forAll :X .
:Joe :likes :easterEggs .
{
:Joe :likes :X .
} log:implies {:X :madeof :chocolate .
} .
};
reason:universal "file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3#X" ].
:_g0 a reason:Parsing;
reason:source <> .
#ENDS
bash-2.05b$ cwm rules-simple.n3 --why
#Processed by Id: cwm.py,v 1.129 2003/04/08 16:12:43 timbl Exp
# using base file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3
# Notation3 generation by
# notation3.py,v 1.137 2003/04/08 16:12:44 timbl Exp
# Base was: file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3
@prefix : <#> .
@prefix daml: <http://www.daml.org/2001/03/daml+oil#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .
this log:forAll :X .
:Joe :likes :easterEggs .
:easterEggs :madeof :chocolate .
{
:Joe :likes :X .
} log:implies {:X :madeof :chocolate .
} .
#ENDS
bash-2.05b$ cwm rules-simple.n3 --think --why
#Processed by Id: cwm.py,v 1.129 2003/04/08 16:12:43 timbl Exp
# using base file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3
@@@@@@@ Proof of 0_work is <why.FormulaReason instance at 0x8382c44>
@@@@@@ notation3 167 loading file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3 <why.BecauseOfCommandLine instance at 0x8382c6c> 0_work
Now: 169 <why.BecauseOfCommandLine instance at 0x8382c6c> <why.FormulaReason instance at 0x8382c44> 0_work
# Notation3 generation by
# notation3.py,v 1.137 2003/04/08 16:12:44 timbl Exp
# Base was: file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3
@prefix : <http://www.w3.org/2000/10/swap/reason#> .
@prefix daml: <http://www.daml.org/2001/03/daml+oil#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix n3: <http://www.w3.org/2000/10/swap/reify#> .
@prefix run: <.run-1051055714.734827p22429#> .
this log:forSome <#_g0> .
[ a :Conjunction,
:Proof;
:component [
a :Extraction;
:because [
a :Inference;
:binding [
:boundTo [
n3:uri "file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3#easterEggs" ];
:variable [
n3:uri "file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3#X" ] ];
:evidence [
a :Extraction;
:because <#_g0>;
:gives {<#Joe> <#likes> <#easterEggs> .
} ];
:rule [
a :Extraction;
:because <#_g0>;
:gives {this log:forAll <#X> .
{
<#Joe> <#likes> <#X> .
} log:implies {<#X> <#madeof> <#chocolate> .
} .
} ] ];
:gives {<#easterEggs> <#madeof> <#chocolate> .
} ],
[
a :Extraction;
:because <#_g0>;
:gives {this log:forAll <#X> .
{
<#Joe> <#likes> <#X> .
} log:implies {<#X> <#madeof> <#chocolate> .
} .
} ],
[
a :Extraction;
:because <#_g0>;
:gives {<#Joe> <#likes> <#easterEggs> .
} ];
:gives {this log:forAll <#X> .
<#Joe> <#likes> <#easterEggs> .
<#easterEggs> <#madeof> <#chocolate> .
{
<#Joe> <#likes> <#X> .
} log:implies {<#X> <#madeof> <#chocolate> .
} .
};
:universal "file:/home/sandro/cvs/cvs.w3c.org/WWW/2000/10/swap/test/rules-simple.n3#X" ].
<#_g0> a :Parsing;
:source <> .
#ENDS
bash-2.05b$
Script done on Tue 22 Apr 2003 07:55:16 PM EDT
http://lists.w3.org/Archives/Public/www-tag/2002Jul/0128.html
Received on Tuesday, 22 April 2003 23:14:41 UTC