Principles of Superdeduction

10 years 10 months ago
Principles of Superdeduction
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 cutelimination 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 t...
Paul Brauner, Clément Houtmann, Claude Kirc
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where LICS
Authors Paul Brauner, Clément Houtmann, Claude Kirchner
Comments (0)