Better trees, big trees
Sometime before christmas, Greg Restall spotted a bug in my tree prover and noticed that it didn't work with Internet Explorer on MacOS X. These problems should now be fixed. I've also started working on an implementation of proofs with identity and function symbols, but I'm not sure if I'll ever finish it.
I actually wrote the tree prover to check the results of another script, which is what I vaguely talk about in the Feedback section. This is what that other script would calculate if I'd ever get it done:
Let L(S) be the length of the shortest tableau proof of sentence S, where length is number of nodes, and let P(N) be the maximum of L(S) for all sentences S with complexity N. So P(N) is the maximum length of the shortest tableau proof of a sentence with complexity N. The script I'd like to write would estimate the first couple of values of P.
Of course, in predicate logic, P is not recursive. Moreover, and what makes it interesting, is that there is no recursive upper bound for it, I think, since otherwise that would provide a decision procedure for predicate logic: To determine whether S is provable, simply go through all proofs with length <= upper_bound(complexity(S)). I'm not even sure if there are any interesting recursive lower bounds.
Also interesting would be the initial values of the function Q(x) that returns the least y such that P(y) = x, that is, the length of the shortest sentence the shortest proof of which has length x.