Efficient Representation and Computation of Tableaux Proofs

The current first-order automatic prover FAUST, embedded in HOL, is based on a sequent calculus which is quite slow and memory intensive. In this paper, an improved version of FAUST using a modified form of tableau calculus called Tableau Graph Calculus is presented which overcomes the well-known inefficiencies of the traditional tableau calculus to a large extent. This calculus works on a compact representation of analytic tableaux called tableau graphs which are obtained by a preprocessing step which covers most of the rule applications of usual tableau calculus. This representation retains the clarity of the input formula and furthermore, its size is linear with respect to the length of the input formula. As a result of this preprocessing, our calculus has only one single rule which is repeatedly applied to obtain a proof. Many optimizations for the rule applications to effectively prune the search space are presented as well and are currently being implemented in a new version of F..