MadMode

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.