- From: Jos De_Roo <jos.deroo@agfa.com>
- Date: Fri, 25 Apr 2003 09:50:19 +0200
- To: "Sandro Hawke <sandro" <sandro@w3.org>
- Cc: www-rdf-logic@w3.org, www-rdf-logic-request@w3.org
Sandro, in the "euler proof mechanism" we actually
just use existing = and => vocabulary to construct a
proof tree/argument/sequent (= for the bindings and
=> for the implications and, as it's all grounded, it's quite
straightforward to validate those). You can find examples in
http://eulersharp.sourceforge.net/2003/03swap/etc5-proof.n3
but that's indeed a rather implicit way and swap's
http://www.w3.org/2000/10/swap/reason.n3
vocabulary looks great!
-- ,
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Sandro Hawke
<sandro@w3.org> To: www-rdf-logic@w3.org
Sent by: cc:
www-rdf-logic-requ Subject: "explanations" in cwm, vocabulary for proof exchange
est@w3.org
2003-04-23 05:14
AM
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 Friday, 25 April 2003 03:50:31 UTC