Click'n'Prove: Interactive Proofs Within Set Theory

Jean-Raymond Abrial Dominique Cansell 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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).
Type de document :
Communication dans un congrès
David Basin et Burkhart Wolff. 16th International Conference on Theorem Proving in Higher Order Logics - TPHOLs'2003, 2003, Rome, Italy, Springer, 2758, pp.1-24, 2003, Lecture notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00099836
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:41:40
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Identifiants

  • HAL Id : inria-00099836, version 1

Collections

Citation

Jean-Raymond Abrial, Dominique Cansell. Click'n'Prove: Interactive Proofs Within Set Theory. David Basin et Burkhart Wolff. 16th International Conference on Theorem Proving in Higher Order Logics - TPHOLs'2003, 2003, Rome, Italy, Springer, 2758, pp.1-24, 2003, Lecture notes in Computer Science. 〈inria-00099836〉

Partager

Métriques

Consultations de la notice

187