A Generic Tableau Prover and Its Integration with Isabelle

Front Cover
University of Cambridge, Computer Laboratory, 1997 - Automatic theorem proving - 16 pages
0 Reviews
Abstract: "A generic tableau prover has been implemented and integrated with Isabelle [14]. It is based on leantap [3] 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."

From inside the book

What people are saying - Write a review

We haven't found any reviews in the usual places.

Common terms and phrases

Bibliographic information