Superdeduction at work

Paul Brauner (1) , Clément Houtmann (1) , Claude Kirchner (1, 2)

1 PROTHEO - Constraints, automatic deduction and software properties proofs
2 INRIA Lorraine

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 normalization of a proof term language that models appropriately superdeduction. We finaly examplify on several examples, includ- ing equality and noetherian induction, the usefulness of this approach which is implemented in the lemuridæ system, written in TOM.

Mots clés: Superdeduction; Sequent Calculus; Cut elimination; Strong normalization; Proofterms; Curry-Howard; Deduction modulo

Domaines: Logique en informatique [cs.LO]

Paul Brauner, Clément Houtmann, Claude Kirchner. Superdeduction at work. Colloquium in honor of Jean-Pierre Jouannaud, Jun 2007, Cachan, France. pp.132-166, ⟨10.1007/978-3-540-73147-4⟩. ⟨inria-00141672v2⟩