Thinking Clearly .

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:

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:

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.

Whilst preparing to lecture on resolution, I found an amusing example resolution proof based on the “She’s a witch” scene from Monty Python and the Holy Grail. The SAMEWEIGHT predicate is clearly a lame bit of modeling, but c’mon. It’s a cool example!

I converted their coding to an OWL ontology, but it seems that Swoop’s pretty printing is really all messed up. Sigh. I tweaked it by hand and fought a bit with WordPress into something a bit more accurate.

If you run it through the Pellet demo (with the right settings), you’ll see that Girl is, in fact, inferred to be an instance of Witch.

If you uncomment the the bit which asserts that Girl is an instance of the complement of Witch, you’ll get an inconsistent ontology.

To really match up with the original example, I should work out the tableau based proof. Maybe in another post.

Getting away from the original example, I suppose I should make weight a datatype property. However, I don’t think I can then encode the sameness of weight in OWL or even OWL 1.1, since that would require me to relate data values from two different individuals. This goes beyond the expressivity of datatype properties in OWL and into full “concrete domains”. Again, a subject for another post!

(Sigh. We need a good ontology repository here at C&P, as well as getting a new version of the online Pellet demo up and running.)

In the spirit of burning, I point you to Zoe’s Welcome In Another Year. I don’t think there’s a recording of her covering Susanna Martin, but the Touchstone version is just dandy.

“Merry war on Xmas” is my new season’s greeting. I love it.

However, this morning it occured to me that two classic “general” season’s greeting phrase, “Happy Holidays” and “Season’s Greetings” had a rather amusing logical structure.

Happy Holidays = For all x, if x is a holiday, then (may) x be happy for you.

Season’s Greetings = For all x, if x is a greetingOfTheSeason, then I greet you with x

I’m not really happy with the quantification of “Season’s Greetings”. I suspect it might be substitutional rather than objectual. I.e., that instead of committing me to a domain with all the greetings in it, it might only commit me to saying all the greetings. In other words, “Season’s Greetings” is more like a macro.

(Ok, Zoe thought it was funny! What’s wrong with the rest of you!)

(No tagline for this one…it was stolen by the Christmas Ninjas. “Make lots of money through stealth in shadow.” should be the new motto of this company.)