Superdeduction at work - Archive ouverte HAL Access content directly
Conference Papers Year : 2007

Superdeduction at work

(1) , (1) , (1, 2)
1
2

Abstract

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.
Fichier principal
Vignette du fichier
atwork-jpj07.pdf (384.09 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00141672 , version 1 (13-04-2007)
inria-00141672 , version 2 (25-06-2007)

Identifiers

Cite

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⟩
89 View
198 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More