Sciweavers

BIRTHDAY
2007
Springer

Superdeduction at Work

13 years 9 months ago
Superdeduction at Work
Superdeduction is a systematic way to extend a deduction system like the sequent calculus by new deduction rules computed from the user theory. We show how this could be done in a systematic, correct and complete way. We prove in detail the strong normalisation of a proof term language that models appropriately superdeduction. We finaly examplify on several examples, including equality and noetherian induction, the usefulness of this approach which is implemented in the lemuridæ system, written in TOM.
Paul Brauner, Clément Houtmann, Claude Kirc
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where BIRTHDAY
Authors Paul Brauner, Clément Houtmann, Claude Kirchner
Comments (0)