Orthogonality and Boolean Algebras for Deduction Modulo

  • Aloïs Brunel
  • Olivier Hermant
  • Clément Houtmann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)


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.


Boolean Algebra Classical Logic Linear Logic Sequent Calculus Model Interpretation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Abr91]
    Abrusci, V.M.: Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic. Journal of Symbolic Logic 56(4), 1403–1451 (1991)CrossRefzbMATHGoogle Scholar
  2. [Cou09]
    Cousineau, D.: Complete reducibility candidates. In: PSTT 2009 (2009)Google Scholar
  3. [CT06]
    Ciabattoni, A., Terui, K.: Towards a semantic characterization of cut-elimination. Studia Logica 82(1), 95–119 (2006)CrossRefzbMATHGoogle Scholar
  4. [DH07]
    Dowek, G., Hermant, O.: A simple proof that super-consistency implies cut elimination. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 93–106. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. [DHK03]
    Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning 31(1), 33–72 (2003)CrossRefzbMATHGoogle Scholar
  6. [Dow06]
    Dowek, G.: Truth values algebras and proof normalization. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 110–124. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. [Dow10]
    Dowek, G.: Fondements des systèmes de preuve. Course notes (2010)Google Scholar
  8. [DW03]
    Dowek, G., Werner, B.: Proof normalization modulo. Journal of Symbolic Logic 68(4), 1289–1316 (2003)CrossRefzbMATHGoogle Scholar
  9. [Gim09]
    Gimenez, S.: Programmer, Calculer et Raisonner avec les Réseaux de la Logique Linéaire. PhD thesis, Université Paris 7 (2009)Google Scholar
  10. [Gir72]
    Girard, J.-Y.: Interprétation Fonctionnelle et Élimination des Coupures de l’Arithmétique dOrdre Supérieur. PhD thesis, Université Paris 7 (1972)Google Scholar
  11. [Gir87]
    Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)CrossRefzbMATHGoogle Scholar
  12. [Kri09]
    Krivine, J.-L.: Realizability in classical logic. Panoramas et synthèses 27, 197–229 (2009)zbMATHGoogle Scholar
  13. [LM08]
    Lengrand, S., Miquel, A.: Classical F [omega], orthogonality and symmetric candidates. Annals of Pure and Applied Logic 153(1-3), 3–20 (2008)CrossRefzbMATHGoogle Scholar
  14. [Oka99]
    Okada, M.: Phase semantic cut-elimination and normalization proofs of first-and higher-order linear logic. Theoretical Computer Science 227(1-2), 333–396 (1999)CrossRefzbMATHGoogle Scholar
  15. [Oka02]
    Okada, M.: A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. Theoretical Computer Science 281(1-2), 471–498 (2002)CrossRefzbMATHGoogle Scholar
  16. [Tai75]
    Tait, W.W.: A realizability interpretation of the theory of species. In: Parikh, R.J. (ed.) Logic Colloquium, pp. 240–251. Springer, Heidelberg (1975)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Aloïs Brunel
    • 1
  • Olivier Hermant
    • 2
  • Clément Houtmann
    • 3
  1. 1.ENS de LyonFrance
  2. 2.ISEPFrance
  3. 3.INRIA SaclayFrance

Personalised recommendations