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 metadatas

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/inria-00563331
Contributor : Clement Houtmann <>
Submitted on : Friday, February 4, 2011 - 3:40:04 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM
Long-term archiving on : Tuesday, November 6, 2012 - 1:32:11 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00563331, version 1

Collections

Citation

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

Share

Metrics

Record views

420

Files downloads

218