Skip to Main content Skip to Navigation
New interface
Preprints, Working Papers, ...

Orthogonality and Boolean Algebras for Deduction Modulo

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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download
Contributor : Clement Houtmann Connect in order to contact the contributor
Submitted on : Friday, February 4, 2011 - 3:40:04 PM
Last modification on : Friday, January 21, 2022 - 4:13:07 AM
Long-term archiving on: : Tuesday, November 6, 2012 - 1:32:11 PM


Files produced by the author(s)


  • HAL Id : inria-00563331, version 1


Alois Brunel, Olivier Hermant, Clement Houtmann. Orthogonality and Boolean Algebras for Deduction Modulo. {date}. ⟨inria-00563331⟩



Record views


Files downloads