User interfaces for theorem provers : informal proceedings of the workshop, Eindhoven University of Technology, 13-15 July 1998
RC Roland Backhouse · TU/e Research Portal · 1998
In this document, we briefly present a program called the Predicate Prover (for short PP).This program essentially offers four functionalities, which are the following: A decision procedure for Propositional Calculus. A partial semi-decision procedure for First-Order Predicate Calculus. A systematic translation of Set-Theoretic Predicates. A coherent treatment of Linear Arithmetic statements.In what follows, we shall quickly present these features in turn.We then show how PP is integrated within the B-Technology' [1] [2], as implemented by Atelier B' [3].In the last section, we comment on a number of rationales and concepts that have been used in the design of PP.Finally, an appendix contains some problems solved by PP and shown in a demo. A Propositional Calculus Decision Procedure. PP essentially first contains an implementation of the decision procedure of PropositionalCalculus, which is presented in the B-Book [1].This procedure is very close to what is elsewhere proposed under the technical name of Semantic Tableaux [4].It is a Sequent Calculus.Next is a sample of a classical proposition proved by PP: I-((a b) c) (a (b c)) * Supported by STERIA, SNCF, RATP and INRETS. 1 B is a model oriented method used in industry to develop safety critical (and other) software systems. 2 Atelier B is the set of industrial tools associated with the B Method. The Integration of the Predicate Prover within the B-Technology.In this section, we present the genesis of PP, we show how it has become one of the pieces of the B-Technology, and we explain how it is integrated within Atelier B. The Prover of Atelier B (for short PB), which constitutes a distinct project from that of PP presented above, works according to two modes: automatic and interactive (the interactive mode being just, in first approximation, a way of manually pulling the various strings offered by PB).We remind the reader that a typical B development resulting in n lines of code, demands the proof of approximatively n/2 lemmas.At the moment, the behavior of PB corresponds to the following typical figure, which is valid for an entirely proved industrial project (say, 50,000 lines of ADA code): 80% of the proofs is discharged automatically by PB, versus 20% interactively.In this case then, approximately 5,000 lemmas have been proved interactively (less, in fact, because the user of PB can take advantage of the systematic discovery of certain proof sequences, which can then be incorporated into some tactics able to be called automatically).This figure has oriented the way PB has been designed.Automatization is indeed indispensable but, as the interactive part of the proof effort is also not negligible, both aspects of the proof technology must be implemented with great care.The main part of PB is based on a number of rules (more than 2,000) that have been introduced gradually during the multi-year construction of this prover.It also contains certain proof mechanisms that may be handled by the user in an automatic or interactive way.Finally, the user might himself introduce some new rules and new tactics that may also be handled automatically or interactively.As can be seen, the process by which PB has been constructed is essentially a pragmatic one.As time passes, we were confronted (under the pressure of some industrial users) with the problem of the correctness of the rules of PB.This is indeed a very serious problem that cannot be treated by means of some reassuring (hand-waving kind of) discourses.This is how PP has started, essentially as an extraneous project to be used in order to validate PB.The result has been more or less what we feared: a number of rules of PB were slightly erroneous (less than 5% however, but still not 0%).In order to keep the construction of PP under control, we choose an incremental design that followed the incremental construction of Mathematics that is presented in the B-Book.This allowed us to use PP to validate PB in an incremental fashion.In other words, as soon as some stage of PP were finished, we used it to validate the corresponding rules of PP.The incremental design of PP resulted in an incremental validation of PB.More serious even than the possibility of erroneous rules in PB is the possibility of the user introducing some erroneous rules during the proof of a B design.In order to cope with this problem we had no choice but to integrate PP within PB.Thanks to this integration, a user-defined rule can thus be validated (proved) before being used.The practice of proving user-defined rules within PB pretty soon induced the idea of sometimes using PP directly on the problem at hand rather than first proving a necessarily ad-hoc rule and then instructing PB to use it.This results in a deeper integration of PP within PB.This process is still under way.o.'1. APPENDIX, Sample Problems Solved by PP.The formulae presented below are written with a certain classical mathematical setting through LATEX.Of course, they are not entered as such in PP.However, the general structure of the formulae given to PP is almost exactly the same, the operators being conventionally represented in ASCII by means of one or more symbols.Propositional Calculus. Generalized Set Operations.