She's a witch and I have the proof (in N3)

Submitted by connolly on Tue, 2007-01-02 22:28. :: |

A while back, somebody turned the Monty Python Burn the Witch sketch into an example resolution proof. Bijan and Kendall had some fun turning it into OWL.

I'm still finding bugs pretty regularly, but the cwm/n3 proof stuff is starting to mature; it works for a few PAW demo scenarios. Ralph asked me to characterize the set of problems it works for. I don't have a good handle on that, but this witch example seems to be in the set.

Transcribing the example resolution FOL KB to N3 is pretty straightforward; the original is preserved in the comments: 


@prefix : <witch#>.
@keywords is, of, a.

#[1] 	BURNS(x) /\ WOMAN(x)	 	=>	WITCH(x)

{ ?x a BURNS. ?x a WOMAN } => { ?x a WITCH }.

#[2]	WOMAN(GIRL)
GIRL a WOMAN.

#[3]	\forall x, ISMADEOFWOOD(x)	=>	BURNS(x)
{ ?x a ISMADEOFWOOD. } => { ?x a BURNS. }.

#[4]	\forall x, FLOATS(x) 		=>	ISMADEOFWOOD(x)
{ ?x a FLOATS } => { ?x a ISMADEOFWOOD }.

#[5]	FLOATS(DUCK)

DUCK a FLOATS.

#[6]	\forall x,y FLOATS(x) /\ SAMEWEIGHT(x,y) =>	FLOATS(y)

{ ?x a FLOATS. ?x SAMEWEIGHT ?y } => { ?y a FLOATS }.

# and, by experiment
# [7]	SAMEWEIGHT(DUCK,GIRL)

DUCK SAMEWEIGHT GIRL.

Then we run cwm to generate the proof and then run the proof checker in report mode: 

$ cwm.py witch.n3  --think --filter=witch-goal.n3  --why >witch-pf.n3
$ check.py --report witch-pf.n3 >witch-pf.txt

The report is plain text; I'll enrich it just a bit here. Note that in the N3 proof format, some formulas are elided. It makes some sense not to repeat the whole formula you get by parsing an input file, but I'm not sure why cwm elides results of rule application. It seems to give the relevant formula on the next line, at least:

  1. ...
    [by parsing <witch.n3>]

  2. :GIRL a :WOMAN .
    [by erasure from step 1]

  3. :DUCK :SAMEWEIGHT :GIRL .
    [by erasure from step 1]

  4. :DUCK a :FLOATS .
    [by erasure from step 1]

  5. @forAll :x, :y . { :x a wit:FLOATS; wit:SAMEWEIGHT :y . } log:implies {:y a wit:FLOATS . } .
    [by erasure from step 1]

  6. ...
    [by rule from step 5 applied to steps [3, 4]
    with bindings {'y': '<witch#GIRL>', 'x': '<witch#DUCK>'}]

  7. :GIRL a :FLOATS .
    [by erasure from step 6]

  8. @forAll :x . { :x a wit:FLOATS . } log:implies {:x a wit:ISMADEOFWOOD . } .
    [by erasure from step 1]

  9. ...
    [by rule from step 8 applied to steps [7]
    with bindings {'x': '<witch#GIRL>'}]

  10. :GIRL a :ISMADEOFWOOD .
    [by erasure from step 9]

  11. @forAll :x . { :x a wit:ISMADEOFWOOD . } log:implies {:x a wit:BURNS . } .
    [by erasure from step 1]

  12. ...
    [by rule from step 11 applied to steps [10]
    with bindings {'x': '<witch#GIRL>'}]

  13. :GIRL a :BURNS .
    [by erasure from step 12]

  14. @forAll witch:x . { witch:x a :BURNS, :WOMAN . } log:implies {witch:x a :WITCH . } .
    [by erasure from step 1]

  15. ...
    [by rule from step 14 applied to steps [2, 13]
    with bindings {'x': '<witch#GIRL>'}]

  16. :GIRL a :WITCH .
    [by erasure from step 15]


All the files are in the swap/test/reason directory: witch.n3, witch-goal.n3, witch-pf.n3, witch-pf.txt. Enjoy.

connolly's blog | login to post comments

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.
testing witch case with euler5
Submitted by http://josd.myo... (OpenID: http://josd.myopenid.com/) on Mon, 2007-04-02 15:24.
Hi Dan,

With (local) euler5 codd proof service
wget -q -O- http://localhost/witch?why=think

where
service.witch = .euler5 http://localhost/.euler+--prolog+--@@@why@@@+http%3A%2F%2Fwww.w3.org%2F2000%2F10%2Fswap%2Ftest%2Freason%2Fwitch.n3+--filter+http%3A%2F%2Fwww.w3.org%2F2000%2F10%2Fswap%2Ftest%2Freason%2Fwitch-goal.n3

the proof output is

#Processed by Id: euler.yap,v 1.162 2007/04/02 19:00:46 josd Exp

@prefix str: <http://www.w3.org/2000/10/swap/string#>.
@prefix var: <http://localhost/var#>.
@prefix q: <http://www.w3.org/2004/ql#>.
@prefix list: <http://www.w3.org/2000/10/swap/list#>.
@prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>.
@prefix fn: <http://www.w3.org/2006/xpath-functions#>.
@prefix xsd: <http://www.w3.org/2001/XMLSchema#>.
@prefix : <http://www.w3.org/2000/10/swap/test/reason/witch#>.
@prefix time: <http://www.w3.org/2000/10/swap/time#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix n3: <http://www.w3.org/2004/06/rei#>.
@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix owl: <http://www.w3.org/2002/07/owl#>.
@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.

[ a r:Proof, r:Conjunction;
r:component [ a r:Inference; r:gives {:GIRL rdf:type :WITCH}; r:evidence (
[ a r:Extraction; r:gives {:GIRL rdf:type :WITCH}; r:because [ a r:Inference; r:gives {:GIRL rdf:type :WITCH}; r:evidence (
[ a r:Extraction; r:gives {:GIRL rdf:type :BURNS}; r:because [ a r:Inference; r:gives {:GIRL rdf:type :BURNS}; r:evidence (
[ a r:Extraction; r:gives {:GIRL rdf:type :ISMADEOFWOOD}; r:because [ a r:Inference; r:gives {:GIRL rdf:type :ISMADEOFWOOD}; r:evidence (
[ a r:Extraction; r:gives {:GIRL rdf:type :FLOATS}; r:because [ a r:Inference; r:gives {:GIRL rdf:type :FLOATS}; r:evidence (
[ a r:Extraction; r:gives {:DUCK rdf:type :FLOATS}; r:because [ a r:Parsing; r:source <http://www.w3.org/2000/10/swap/test/reason/witch.n3>]]
[ a r:Extraction; r:gives {:DUCK :SAMEWEIGHT :GIRL}; r:because [ a r:Parsing; r:source <http://www.w3.org/2000/10/swap/test/reason/witch.n3>]]);
r:binding [ r:variable [ n3:uri "http://localhost/var#x"]; r:boundTo [ n3:uri "http://www.w3.org/2000/10/swap/test/reason/witch#DUCK"]];
r:binding [ r:variable [ n3:uri "http://localhost/var#y"]; r:boundTo [ n3:uri "http://www.w3.org/2000/10/swap/test/reason/witch#GIRL"]];
r:rule [ a r:Extraction; r:gives {@forAll var:x,var:y. {var:x a :FLOATS. var:x :SAMEWEIGHT var:y} => {var:y a :FLOATS}. }; r:because [ a r:Parsing; r:source <http://www.w3.org/2000/10/swap/test/reason/witch.n3>]]]]);
r:binding [ r:variable [ n3:uri "http://localhost/var#x"]; r:boundTo [ n3:uri "http://www.w3.org/2000/10/swap/test/reason/witch#GIRL"]];
r:rule [ a r:Extraction; r:gives {@forAll var:x. {var:x a :FLOATS} => {var:x a :ISMADEOFWOOD}. }; r:because [ a r:Parsing; r:source <http://www.w3.org/2000/10/swap/test/reason/witch.n3>]]]]);
r:binding [ r:variable [ n3:uri "http://localhost/var#x"]; r:boundTo [ n3:uri "http://www.w3.org/2000/10/swap/test/reason/witch#GIRL"]];
r:rule [ a r:Extraction; r:gives {@forAll var:x. {var:x a :ISMADEOFWOOD} => {var:x a :BURNS}. }; r:because [ a r:Parsing; r:source <http://www.w3.org/2000/10/swap/test/reason/witch.n3>]]]]
[ a r:Extraction; r:gives {:GIRL rdf:type :WOMAN}; r:because [ a r:Parsing; r:source <http://www.w3.org/2000/10/swap/test/reason/witch.n3>]]);
r:binding [ r:variable [ n3:uri "http://localhost/var#x"]; r:boundTo [ n3:uri "http://www.w3.org/2000/10/swap/test/reason/witch#GIRL"]];
r:rule [ a r:Extraction; r:gives {@forAll var:x. {var:x a :BURNS. var:x a :WOMAN} => {var:x a :WITCH}. }; r:because [ a r:Parsing; r:source <http://www.w3.org/2000/10/swap/test/reason/witch.n3>]]]]);
r:rule [ a r:Extraction; r:gives {@forAll . {:GIRL a :WITCH} => {:GIRL a :WITCH}. }; r:because [ a r:Parsing; r:source <http://www.w3.org/2000/10/swap/test/reason/witch-goal.n3>]]];
r:gives {
:GIRL rdf:type :WITCH.}].

#ENDS 4 msec.


and the check.py is happy with that but is actually in 26 steps

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

2: :DUCK a :FLOATS .
[by erasure from step 1]

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

4: :DUCK :SAMEWEIGHT :GIRL .
[by erasure from step 3]

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

6: @forAll :x, :y . { :x a witch:FLOATS; witch:SAMEWEIGHT :y . } log:implies {:y a witch:FLOATS . } .
[by erasure from step 5]

7: :GIRL a :FLOATS .
[by rule from step 6 applied to steps [2, 4]
with bindings {'y': '<http://www.w3.org/2000/10/swap/test/reason/witch#GIRL>', 'x': '<http://www.w3.org/2000/10/swap/test/reason/witch#DUCK>'}]

8: :GIRL a :FLOATS .
[by erasure from step 7]

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

10: @forAll :x . { :x a witch:FLOATS . } log:implies {:x a witch:ISMADEOFWOOD . } .
[by erasure from step 9]

11: :GIRL a :ISMADEOFWOOD .
[by rule from step 10 applied to steps [8]
with bindings {'x': '<http://www.w3.org/2000/10/swap/test/reason/witch#GIRL>'}]

12: :GIRL a :ISMADEOFWOOD .
[by erasure from step 11]

13: ...
[by parsing <witch.n3>]

14: @forAll :x . { :x a witch:ISMADEOFWOOD . } log:implies {:x a witch:BURNS . } .
[by erasure from step 13]

15: :GIRL a :BURNS .
[by rule from step 14 applied to steps [12]
with bindings {'x': '<http://www.w3.org/2000/10/swap/test/reason/witch#GIRL>'}]

16: :GIRL a :BURNS .
[by erasure from step 15]

17: ...
[by parsing <witch.n3>]

18: :GIRL a :WOMAN .
[by erasure from step 17]

19: ...
[by parsing <witch.n3>]

20: @forAll :x . { :x a witch:BURNS, witch:WOMAN . } log:implies {:x a witch:WITCH . } .
[by erasure from step 19]

21: :GIRL a :WITCH .
[by rule from step 20 applied to steps [16, 18]
with bindings {'x': '<http://www.w3.org/2000/10/swap/test/reason/witch#GIRL>'}]

22: :GIRL a :WITCH .
[by erasure from step 21]

23: ...
[by parsing <witch-goal.n3>]

24: { :GIRL a :WITCH . } log:implies {:GIRL a :WITCH . } .
[by erasure from step 23]

25: :GIRL a :WITCH .
[by rule from step 24 applied to steps [22]
with bindings {}]

26: :GIRL a :WITCH .
[by conjoining steps [25]]

@prefix : <http://www.w3.org/2000/10/swap/test/reason/witch#> .

:GIRL a :WITCH .


Thanks and kind regards,
Jos
login to post comments
Errors when using the --why option
Submitted by http://andrea.v... (OpenID: http://andrea.videntity.org/) on Thu, 2007-03-22 04:52.

Hi, Dan.

I tried the "witch" example, but I encountered an error when using the --why option.

Now, when I run

$ cwm.py witch.n3 --think --filter=witch-goal.n3

Cwm returns, correctly:

************************************************************

#Processed by Id: cwm.py,v 1.164 2004/10/28 17:41:59 timbl Exp
# using base file:/<path>/witch.n3

# Notation3 generation by
# notation3.py,v 1.166 2004/10/28 17:41:59 timbl Exp

# Base was: file:/<path>/witch.n3
@prefix : <witch#> .

:GIRL a :WITCH .

#ENDS

************************************************************

By contrast, if I run

$ cwm.py witch.n3 --think --filter=witch-goal.n3

Cwm returns:

************************************************************

#Processed by Id: cwm.py,v 1.164 2004/10/28 17:41:59 timbl Exp
# using base file:/<path>/witch.n3
@@@@@@@ Proof of {} is <swap.why.FormulaReason instance at 0x00CBE8F0>
@@@@@@ notation3 167 loading file:/<path>/witch.n3 None {}
Now: 169 None <swap.why.FormulaReason instance at 0x00CBE8F0> {}
Traceback (most recent call last):
File "<path>\cwm-1.0.0\cwm.py", line 650, in ? doCommand()
File "<path>\cwm-1.0.0\cwm.py", line 563, in doCommand
think(workingContext, mode=option_flags["think"])
File "<path>\cwm-1.0.0\swap\query.py", line 60, in think
File "<path>\cwm-1.0.0\swap\query.py", line 220, in run
File "<path>\cwm-1.0.0\swap\query.py", line 208, in runSmart
File "<path>\cwm-1.0.0\swap\query.py", line 349, in run
File "<path>\cwm-1.0.0\swap\query.py", line 441, in once
File "<path>\cwm-1.0.0\swap\query.py", line 585, in resolve
File "<path>\cwm-1.0.0\swap\query.py", line 822, in unify
File "<path>\cwm-1.0.0\swap\query.py", line 706, in unify
NameError: global name 'Error' is not defined

************************************

Any idea of the reason why this happens?

Andrea

login to post comments
proof stuff is pretty new
Submitted by connolly (OpenID: http://www.w3.org/People/Connolly/) on Fri, 2007-03-23 20:11.

You seem to be using a version of cwm from 2004; much of the proof work is newer than that. We're overdue for a release; meanwhile, see the instructions for checking out the latest development version.

(I gave pretty much the same answer in reply to your cwm-talk message.)

login to post comments