Principles of Superdeduction

Paul Brauner 1 Clement Houtmann 1 Claude Kirchner 1, 2
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In predicate logic, the proof that a theorem P holds in a theory Th is typically conducted in natural deduction or in the sequent calculus using all the information contained in the theory in a uniform way. Introduced ten years ago, Deduction modulo allows us to make use of the computational part of the theory Th for true computations modulo which deductions are performed. Focussing on the sequent calculus, this paper presents and studies the dual concept where the theory is used to enrich the deduction system with new deduction rules in a systematic, correct and complete way. We call such a new deduction system "superdeduction''. We introduce a proof-term language and a cut-elimination procedure both based on Christian Urban's work on classical sequent calculus. Strong normalisation is proven under appropriate and natural hypothesis, therefore ensuring the consistency of the embedded theory and of the deduction system. The proofs obtained in such a new system are much closer to the human intuition and practice. We consequently show how superdeduction along with deduction modulo can be used to ground the formal foundations of new extendible proof assistants. We finally present lemuridae, our current implementation of superdeduction modulo.
Type de document :
Communication dans un congrès
Twenty-Second Annual IEEE Symposium on Logic in Computer Science - LiCS 2007, Jul 2007, Wroclaw, Poland. IEEE Computer Society, 2007, <10.1109/LICS.2007.37>
Liste complète des métadonnées


https://hal.inria.fr/inria-00133557
Contributeur : Clement Houtmann <>
Soumis le : mardi 15 mai 2007 - 11:59:04
Dernière modification le : mardi 25 octobre 2016 - 17:01:14
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 15:51:30

Fichier

superdeduction.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Paul Brauner, Clement Houtmann, Claude Kirchner. Principles of Superdeduction. Twenty-Second Annual IEEE Symposium on Logic in Computer Science - LiCS 2007, Jul 2007, Wroclaw, Poland. IEEE Computer Society, 2007, <10.1109/LICS.2007.37>. <inria-00133557v3>

Partager

Métriques

Consultations de
la notice

158

Téléchargements du document

113