Click'n'Prove: Interactive Proofs Within Set Theory

Jean-Raymond Abrial , Dominique Cansell (1)

1 MOSEL - Proof-oriented development of computer-based systems

In this article, we first briefly present a proof assistant called the Predicate Prover, which essentially offers two functionalities: (1) an automatic semi-decision procedure for First Order Predicate Calculus, and (2) a systematic translation of statements written within Set Theory into equivalent ones in First Order Predicate Calculus. We then show that the automatic usage of this proof assistant is limited by several factors. We finally present (and this is the main part of this article) the principles that we have used in the construction of a {\em proactive} interface aiming at circumventing these limitations. Such principles are based on our practical experience in doing many interactive proofs (within Set Theory).

Mots clés: set theory; prouveur automatique; automatic prover; interactive prover; prouveur interactif; séquent; théorie des ensembles

Domaines: Autre [cs.OH]

Jean-Raymond Abrial, Dominique Cansell. Click'n'Prove: Interactive Proofs Within Set Theory. 16th International Conference on Theorem Proving in Higher Order Logics - TPHOLs'2003, 2003, Rome, Italy, pp.1-24. ⟨inria-00099836⟩