Superdeduction in Lambda-bar-mu-mu-tilde

Clement Houtmann 1
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Superdeduction is a method specially designed to ease the use of first-order theories in predicate logic. The theory is used to enrich the deduction system with new deduction rules in a systematic, correct and complete way. A proof-term language and a cut-elimination reduction already exist for superdeduction, both based on Christian Urban's work on classical sequent calculus. However Christian Urban's calculus is not directly related to the Curry-Howard correspondence contrarily to the lbmmt-calculus which relates straightaway to the lambda-calculus. This short paper is my first step towards a further exploration of the computational content of superdeduction proofs, for I extend the lbmmt-calculus in order to obtain a proofterm langage together with a cut-elimination reduction for superdeduction. I also prove strong normalisation for this extension of the blmmt-calculus.
Type de document :
Communication dans un congrès
Steffen van Bakel and Stefano Berardi and Ulrich Berger. Classical Logic and Computation 2010, Aug 2010, Brno, Czech Republic. 47, pp.33-43, 2011, Proceedings Third International Workshop on Classical Logic and Computation. 〈10.4204/EPTCS.47.5〉
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00498744
Contributeur : Clement Houtmann <>
Soumis le : jeudi 8 juillet 2010 - 12:46:39
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : jeudi 1 décembre 2016 - 05:45:54

Fichier

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

Identifiants

Collections

Citation

Clement Houtmann. Superdeduction in Lambda-bar-mu-mu-tilde. Steffen van Bakel and Stefano Berardi and Ulrich Berger. Classical Logic and Computation 2010, Aug 2010, Brno, Czech Republic. 47, pp.33-43, 2011, Proceedings Third International Workshop on Classical Logic and Computation. 〈10.4204/EPTCS.47.5〉. 〈inria-00498744〉

Partager

Métriques

Consultations de la notice

221

Téléchargements de fichiers

127