Skip to Main content Skip to Navigation
New interface
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Clement Houtmann Connect in order to contact the contributor
Submitted on : Thursday, July 8, 2010 - 12:46:39 PM
Last modification on : Saturday, June 25, 2022 - 7:45:45 PM
Long-term archiving on: : Thursday, December 1, 2016 - 5:45:54 AM


Files produced by the author(s)




Clement Houtmann. Superdeduction in Lambda-bar-mu-mu-tilde. Classical Logic and Computation 2010, Aug 2010, Brno, Czech Republic. pp.33-43, ⟨10.4204/EPTCS.47.5⟩. ⟨inria-00498744⟩



Record views


Files downloads