A Generic Tableau Prover and Its Integration with Isabelle
University of Cambridge, Computer Laboratory, 1997 - Automatic theorem proving - 16 pages
Abstract: "A generic tableau prover has been implemented and integrated with Isabelle . It is based on leantap  but is much more complicated, with numerous modifications to allow it to reason with any supplied set of tableau rules. It has a higher-order syntax in order to support the binding operators of set theory; unification is first-order (extended for bound variables in obvious ways) instead of higher-order, for simplicity. When a proof is found, it 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, it knows almost nothing about types."
What people are saying - Write a review
We haven't found any reviews in the usual places.
7-formula 7-rules 8.1 The Translation a-rule allow backtracking application domains Blast.tac bound variable branch is closed choice points close the branch closing a branch complicated current formula depth-first search DESIGNING THE PROVER example expanded Fast.tac first-order logic first-order tableau five Prolog clauses free variables higher-order logic higher-order syntax higher-order unification inferences instantiates variables INTEGRATION WITH ISABELLE interactive tools Isabelle proofs Isabelle rules Isabelle's meta-logic Isabelle's proof engine Isabelle's tableau prover Isabelle/ZF iterative deepening leantap liberalized J-rules literals multiple goal formulas natural deduction outer formula overloaded constants probably instantiate Proof reconstruction occasionally Proofs to Isabelle prover can expect prover cannot easily queue reconstruction occasionally fails replaces rules to tableau search space search strategy security protocols 18 Set theory problems Skolem function Skolem term stack discipline subgoals Suc(n tableau methods tableau proof tableau rules tableau theorem-proving Theorem Prover translation of Isabelle unifiable universal quantifier UNIVERSITY OF CAMBRIDGE