Witchly interlude: SPASSing out
by Bijan Parsia
I see Dan has converted the Witch argument to N3 and used its proof generation tools to output a proof (btw, Dan, the OWL version was a solo effort by me and I guess you’ll have to come to our actual weblog to see who I am :)). (BTW, even though I linked to it, I should mention explicitly that the original is due to John Ioannidis.)
I’m jotting up the tableau version of the proof (but it’s a bit tricky, pedagogically since if I use a linear proof format, then it doesn’t really correspond to what, e.g., Pellet does, but if I use a completion graph approach I gotta go graphical). However, Dan’s post reminded me that SPASS (and MSPASS) will generate (roughly, resolution based) proofs and have web interfaces. (These proofs are meant, I think, to be checkable.)
So, following the SPASS tutorial, I got this:
begin_problem(Burn_the_Witch_Argument).
list_of_descriptions.
name({*Burn the Witch Argument <strong>}).
author({</strong> Bijan Parsia <strong>}).
status(unsatisfiable).
description({</strong> Formalization of the Burn the Witch Argument*}).
end_of_list.
list_of_symbols.
functions[(girl,0), (duck,0)].
predicates[(Burns,1),(Woman,1),(Witch,1),(IsMadeOfWood,1),(Floats,1),(SameWeight,2)].
end_of_list.
list_of_formulae(axioms).
formula(forall([X], implies(and(Burns(X), Woman(X)), Witch(X))), 1).
formula(Woman(girl),2).
formula(forall([X],implies(IsMadeOfWood(X), Burns(X))),3).
formula(forall([X],implies(Floats(X), IsMadeOfWood(X))),4).
formula(Floats(duck),5).
formula(forall([X,Y],implies(and(Floats(X), SameWeight(X, Y)), Floats(Y))),6).
formula(SameWeight(duck, girl), 7).
end_of_list.
list_of_formulae(conjectures).
formula(Witch(girl),8).
end_of_list.
end_problem.
If you paste this into the SPASS interactive web form, and add -DocProof in the options field, you’ll get a bunch of stuff including the proof:
Here is a proof with depth 3, length 15 :
1[0:Inp] || -> Floats(duck)*.
2[0:Inp] || -> Woman(girl)*.
3[0:Inp] || -> SameWeight(duck,girl)*.
4[0:Inp] || Witch(girl)*+ -> .
5[0:Inp] Floats(U) || -> IsMadeOfWood(U)*.
6[0:Inp] IsMadeOfWood(U) || -> Burns(U)*.
7[0:Inp] Burns(U) Woman(U) || -> Witch(U)*.
8[0:Inp] Floats(U) || SameWeight(U,V)*+ -> Floats(V).
9[0:Res:7.2,4.0] Woman(girl) Burns(girl) || -> .
10[0:MRR:9.0,2.0] Burns(girl) || -> .
17[0:SoR:10.0,6.1] IsMadeOfWood(girl) || -> .
18[0:SoR:17.0,5.1] Floats(girl) || -> .
20[0:Res:3.0,8.1] Floats(duck) || -> Floats(girl)*.
21[0:SSi:20.0,1.0] || -> Floats(girl)*.
22[0:MRR:21.0,18.0] || -> .
Formulae used in the proof : 5 2 7 8 4 3 1 6
Neat!
SPASS is a full first order logic theorem prover. Our translation into OWL DL (ALC really) shows that we don’t need full FOL for this. MSPASS tweaks SPASS so that it effects a decision procedure for (various) DLs. I did a MSPASS DL variant of the argument as well (wish I had an tool to convert to that format from OWL; oh, if you want to save it to disk, you should strip off the ”.txt” and put a dot before the “dfg”.). You can test it with the MSPASS web interface (which will show you the various translations back to FOL).
Philosophically, I’m remain skeptical about the general value of proof generation (at least for exchange, e.g., for PCA like tasks), especially for scalable, decidable logics. Basically, the proofs can be expontential in the size of the input, and the input can be large. For decidable logics with optimized reasoners, for many things, an asserted justification (i.e., a minimal set of axioms from the KB sufficient to entail the conclusion) might be more than sufficient. There’s a complex story here, of course, but if your proof checker isn’t reliable (Dan said he was still finding bugs :)), then even using it to verify is a bit tricky. Proof checkers aren’t always easier.
January 3rd, 2007 at 7:42 pm
I’d be curious to see how a tableau proof compares to a resolution-based proof. “AI: A Modern Approach” has a nice unification heuristic [1] (in python as well) for a backward chaining algorithm which is similar to how prolog unifies and the basis for Deroo’s euler-enhanced resolution mechanism for proof and backward chaining.
I’ve recently pondered hooking up the python RETE-UL [2] implementation I’ve been playing with a means to track a non-circular path through the RETE network as an alternative proof generation mechanism for large rulesets and factbases. I wonder if there is some metric for comparing the application of LP heuristics to DLP reasoning against (more traditional) resolution and tableux-based heuristics for the same KR.
Generated proofs, whether or not they are truely valuable, bring about a certain unmatchable satisfaction to a logician =)
[1] http://aima.cs.berkeley.edu/python/logic.html
[2] http://reports-archive.adm.cs.cmu.edu/anon/1995/CMU-CS-95-113.pdf
January 3rd, 2007 at 10:55 pm
I’ll be using a ground semantic calculus, since that’s what’s most commonly used in DL reasoners. I suppose I could do a free variable one as well, which will pop in unification.
RETE and LP (by which I presume you mean logic programming) don’t most naturally conflate in my lexicon. The bog standard framework for LP is resolution, from Prolog and Datalog to disjunctive datalog and answer set programming.
But the most natural metric would be performance, I would think :)
And do you mean “optimizations” by “heuristics”? Many optimizations are not heuristic, at least not in how I understand “heuristic”.