Axiom directed Focusing - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2009

Axiom directed Focusing

Résumé

Superdeduction and deduction modulo are methods specially designed to ease the use of first-order theories in predicate logic. Superdeduction modulo, which combines both, enables the user to make a distinct use of computational and reasoning axioms. Although soundness is ensured, using superdeduction and deduction modulo to extend deduction with awkward theories can jeopardize essential properties of the extended system such as cut-elimination or completeness \wrt~predicate logic. Therefore one has to design criteria for theories which can safely be used through superdeduction and deduction modulo. In this paper we revisit the superdeduction paradigm by comparing it with the focusing approach. In particular we prove a focalization theorem for cut-free superdeduction modulo: we show that permutations of inference rules can transform any cut-free proof in deduction modulo into a cut-free proof in superdeduction modulo and conversely, provided that some hypotheses on the synchrony of reasoning axioms are verified. It implies that cut-elimination for deduction modulo and for superdeduction modulo are equivalent. Since several criteria have already been proposed for theories that do not break cut-elimination of the corresponding deduction modulo system, these criteria also imply cut-elimination of the superdeduction modulo system, provided our synchrony hypotheses hold. Finally we design a tableaux method for superdeduction modulo which is sound and complete provided cut-elimination holds.
Fichier principal
Vignette du fichier
paper.pdf (308.43 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00212059 , version 1 (22-01-2008)
inria-00212059 , version 2 (10-04-2008)
inria-00212059 , version 3 (02-07-2008)

Identifiants

Citer

Clément Houtmann. Axiom directed Focusing. Types for Proofs and Programs, International Conference, TYPES 2008, Mar 2008, Torino, Italy. pp.169-185, ⟨10.1007/978-3-642-02444-3_11⟩. ⟨inria-00212059v3⟩
107 Consultations
180 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More