Skip to Main content Skip to Navigation
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

https://hal.inria.fr/inria-00498744
Contributor : Clement Houtmann <>
Submitted on : Thursday, July 8, 2010 - 12:46:39 PM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM
Long-term archiving on: : Thursday, December 1, 2016 - 5:45:54 AM

File

LbmmtPlus.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

316

Files downloads

342