Superdeduction in Lambda-Bar-Mu-Mu-Tilde
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 supe...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2011-01-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1101.5443v1 |
| _version_ | 1818233210583121920 |
|---|---|
| author | Clément Houtmann |
| author_facet | Clément Houtmann |
| author_sort | Clément Houtmann |
| collection | DOAJ |
| description | 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 the computational content of Christian Urban's calculus is not directly related to the (lambda-calculus based) Curry-Howard correspondence. In contrast the Lambda bar mu mu tilde calculus is a lambda-calculus for classical sequent calculus. This short paper is a first step towards a further exploration of the computational content of superdeduction proofs, for we extend the Lambda bar mu mu tilde calculus in order to obtain a proofterm langage together with a cut-elimination reduction for superdeduction. We also prove strong normalisation for this extension of the Lambda bar mu mu tilde calculus. |
| first_indexed | 2024-12-12T11:18:34Z |
| format | Article |
| id | doaj.art-66579203a1a04915a360fe6704376f96 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-12T11:18:34Z |
| publishDate | 2011-01-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-66579203a1a04915a360fe6704376f962022-12-22T00:26:06ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802011-01-0147Proc. CL&C 2010344310.4204/EPTCS.47.5Superdeduction in Lambda-Bar-Mu-Mu-TildeClément HoutmannSuperdeduction 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 the computational content of Christian Urban's calculus is not directly related to the (lambda-calculus based) Curry-Howard correspondence. In contrast the Lambda bar mu mu tilde calculus is a lambda-calculus for classical sequent calculus. This short paper is a first step towards a further exploration of the computational content of superdeduction proofs, for we extend the Lambda bar mu mu tilde calculus in order to obtain a proofterm langage together with a cut-elimination reduction for superdeduction. We also prove strong normalisation for this extension of the Lambda bar mu mu tilde calculus.http://arxiv.org/pdf/1101.5443v1 |
| spellingShingle | Clément Houtmann Superdeduction in Lambda-Bar-Mu-Mu-Tilde Electronic Proceedings in Theoretical Computer Science |
| title | Superdeduction in Lambda-Bar-Mu-Mu-Tilde |
| title_full | Superdeduction in Lambda-Bar-Mu-Mu-Tilde |
| title_fullStr | Superdeduction in Lambda-Bar-Mu-Mu-Tilde |
| title_full_unstemmed | Superdeduction in Lambda-Bar-Mu-Mu-Tilde |
| title_short | Superdeduction in Lambda-Bar-Mu-Mu-Tilde |
| title_sort | superdeduction in lambda bar mu mu tilde |
| url | http://arxiv.org/pdf/1101.5443v1 |
| work_keys_str_mv | AT clementhoutmann superdeductioninlambdabarmumutilde |