Skip to Main content Skip to Navigation
Conference papers

Axiom directed Focusing

Clément Houtmann 1
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/inria-00212059
Contributor : Clement Houtmann <>
Submitted on : Wednesday, July 2, 2008 - 9:39:02 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM
Long-term archiving on: : Saturday, November 26, 2016 - 12:31:16 AM

File

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

277

Files downloads

204