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.

• Type: Conference
• Year: 2007
• Where: BIRTHDAY
• Authors: Paul Brauner, Clément Houtmann, Claude Kirchner
• Keywords: Applied Computing, BIRTHDAY 2007, Proof Term Language, Sequent Calculus, Systematic Way