Orthogonality and Boolean Algebras for Deduction Modulo

Alois Brunel 1 Olivier Hermant 2 Clement Houtmann 3
3 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : Originating from automated theorem proving, deduction modulo removes computational arguments from proofs by interleaving rewriting with the deduction process. From a proof-theoretic point of view, deduction modulo defines a generic notion of cut that applies to any first-order theory presented as a rewrite system. In such a setting, one can prove cut-elimination theorems that apply to many theories, provided they verify some generic criterion. Pre-Heyting algebras are a generalization of Heyting algebras which are used by Dowek to provide a semantic intuitionistic criterion called superconsistency for generic cut-elimination. This paper uses pre-Boolean algebras (generalizing Boolean algebras) and biorthogonality to prove a generic cut-elimination theorem for the classical sequent calculus modulo. It gives this way a novel application of reducibility candidates techniques, avoiding the use of proof-terms and simplifying the arguments.
Type de document :
Pré-publication, Document de travail
Liste complète des métadonnées

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

Contributeur : Clement Houtmann <>
Soumis le : vendredi 4 février 2011 - 15:40:04
Dernière modification le : jeudi 10 mai 2018 - 02:06:48
Document(s) archivé(s) le : mardi 6 novembre 2012 - 13:32:11


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00563331, version 1



Alois Brunel, Olivier Hermant, Clement Houtmann. Orthogonality and Boolean Algebras for Deduction Modulo. 2011. 〈inria-00563331〉



Consultations de la notice


Téléchargements de fichiers