Michael Jones, PhD

From Dominique's TPHOLs 2003 paper: " The prover pp is more elaborate than pb, it is based on a firmer theoretical background: it is essentially a prover for First Order Predicate Calculus with Equality (and some Arithmetic) together with a Translator from Set Theory to First Order Predicate Calculus. "

This is an interesting statement from the same paper:

In no way is pp constructed from a meta-prover able to be parameterized by a variety of distinct logics. This contrasts with what can be seen in academic circles where extremely powerful general purpose Proof Systems are usually offered: HOL [8], Isabelle [12], PVS [11], Coq [5], etc. Our approach is quite different. It is rather similar to that used in the development of some industrial programs handling symbolic data. For instance, a good C compiler is not a meta-compiler specialized to C; likewise, a good chess-playing program is not a general purpose game-playing program specialized by the rules and strategies of the game of chess.

We think that it is important to completely separate these two functions in two distinct tools: again, this is what is done in Atelier B where you have the, so-called, Proof Obligation Generator based on a weakest pre-condition analysis of formal texts and which delivers the statements to be proved (it tells you the “what-to-prove”), and, as a distinct tool, the Prover which is supposed to discharge the previous statements (it tells you thus the “how-to-prove”). Our view is that, whatever the logic of system development you decide to use, it will generate some final lemmas that are, inevitably, to be proved within classical logic.

Moreover, we do not think at all that the usage of Set Theory restricts you to the expression of elementary mathematical facts only: it is quite possible to encode within Set Theory mathematical statements that are clearly belonging to what is called higher order logic [1] (another example is given in Appendix 2).

Some more details on the predicate prover: "The prover pp essentially first contains a decision procedure for Propositional Calculus. This procedure is very close to what is elsewhere proposed under the technical name of Semantic Tableaux [7]. "

The prover has two steps that are repeated. First, rewrite terms involving universal quantifiers into terms that have a contradiction on the right side of the sequent. If that fails, then you have to instantiate some universally quantified terms to get a contradiction with the literals. That's next. Second, do some instantation of the quantified variables to derrive a contradiction. This is done using something like the "set of support" method in Otter[10]. There's an example in the paper.

The main limitations of the prover are that... 0. Its sensitive to useless hypotheses. For good or bad. 1. its not good at abstracting a statement into a previously proven but more general statement. 2. doesn't manage equality very well. 3. Isn't good at things where you have to creatively make a decision on how to proceede with the proof. This is endemic to automatic provers everywhere.

References:
[1] J.-R. Abrial, D. Cansell, and G. Lafitte. "Higher-Order" Mathematics in B. In ZB’2002 – Formal Specification and Development in Z and B, number LNCS 2272 in Lecture Notes in Computer Science, pages 370–393, 2002.
[7] M. Fitting. First-order logic and automated theorem proving (2nd ed.). Springer-Verlag New York, Inc., 1996.