Wolfgang Schwarz

TPG2a

Last week the RSI got worse, and this week I've spent some more time on the tree prover. Here's the current version. It works in Mozilla and (slower) Opera on Linux, and doesn't work in Konqueror. I don't have any other browsers here, so feedback on how it behaves especially in Safari and Internet Explorer is welcome.

The prover is generally faster and more stable than the old one. But it still does badly on some formulas, like ((x(PxRx)y(QySy))(zPzzQz)xy((PxQy)(RxSy))). There are some improvements (e.g. merging) under the hood that would improve the performance, but are currently turned off because they make it very hard to translate the resulting free-variable tableau into a sentence tableau. My plan is to turn these features on automatically when a proof search takes too long, and not to display a tree in that case. I'm also thinking about trying to find simpler proofs after a first proof has been found: the tableau for the above formula doesn't look like it's the smallest possible proof.

To improve the detection of invalid formulas, I've added a very simple countermodel finder. What it does is simply check all possible interpretations of the root formula on the sets { 0 }, { 0,1 }, etc. This works surprisingly well since many interesting invalid formulas have a countermodel with a very small domain. The countermodels are currently not displayed, but that will change soon.