A Generic Tableau Prover and its Integration with Isabelle

Lawrence C. Paulson (Computer Laboratory, University of Cambridge, England)

Abstract: A generic tableau prover has been implemented and integrated with Isabelle (Paulson, 1994). Compared with classical first-order logic provers, it has numerous extensions that allow it to reason with any supplied set of tableau rules. It has a higher-order syntax in order to support user-defined binding operators, such as those of set theory. The unification algorithm is first-order instead of higher-order, but it includes modifications to handle bound variables. The proof, when found, is returned to Isabelle as a list of tactics. Because Isabelle verifies the proof, the prover can cut corners for efficiency's sake without compromising soundness. For example, the prover can use type information to guide the search without storing type information in full.

Categories: F.4, I.1