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.
Type de document :
Communication dans un congrès
Stefano Berardi and Ferruccio Damiani and Ugo de'Liguoro. Types for Proofs and Programs, International Conference, TYPES 2008, Mar 2008, Torino, Italy. Springer, 5497, pp.169-185, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02444-3_11〉
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00212059
Contributeur : Clement Houtmann <>
Soumis le : mercredi 2 juillet 2008 - 09:39:02
Dernière modification le : jeudi 11 janvier 2018 - 01:49:21
Document(s) archivé(s) le : samedi 26 novembre 2016 - 00:31:16

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Clément Houtmann. Axiom directed Focusing. Stefano Berardi and Ferruccio Damiani and Ugo de'Liguoro. Types for Proofs and Programs, International Conference, TYPES 2008, Mar 2008, Torino, Italy. Springer, 5497, pp.169-185, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02444-3_11〉. 〈inria-00212059v3〉

Partager

Métriques

Consultations de la notice

226

Téléchargements de fichiers

100