Counter-Models and Free-Variable Tableau Systems
I'm half-way into programming a more efficient tree prover, based on free-variable tableaux. But now I'm not sure any more if this is really what I want.
The basic idea in free-variable tableaux is that you use dummy constants
to instantiate universally quantified formulas, and only replace these
dummy constants by real constants if this allows you to close a branch. In
automatised tableaux, this dramatically decreases the steps required for
certain proofs. For example, my old tree prover internally creates an
860-node tree to prove 
xy(Fxy 
zFzz) 
x y Fxy x Fxx, whereas a free-variable
system only needs 12 nodes.
However, I'm not a mathematician, and it's not the primary goal of my
prover to show, say, the derivability of Fermat's theorem from the Peano
axioms. I just want it to find nice tableau proofs for easy examples like
those used in philosophy textbooks. The main practical problem with my
algorithm (apart from bugs) is not that it's slow at proving valid
sentences, but that it's bad at recognizing invalid ones: If there is a
universally quantified formula on a branch that can't be closed, the script
only terminates if the formula can't be instantiated any more with an
individual constant that already occurs on the branch (or with 'a' if there
is no constant on the branch). So it terminates on x y
Fxy, but not on x y Fxy.
And this problem gets much worse in free-variable tableaux: As
far as I know, there is no similar rule here that would legitimate
terminating after some instantiations of a universally quantified formula.
So even on x Fx the tableaux construction never stops.
This makes me wonder whether the free-variable system is really better in
efficiently tackling the decision problem. I don't know if this can
be quantified, but trading a significant improvement on the positive side
of that problem (detecting validity within bounded resources) by a
significant step backwards on the negative side (detecting invalidity
within bounded resources) doesn't look very attractive to me.
Should I now add a separate counter-model detector to the tableau system to compensate for this weakness? This sounds like a very odd thing to do because I always thought the tableau system itself was basically a counter-model detector.