Towards CERes in intuitionistic logic

Authors Alexander Leitsch, Giselle Reis, Bruno Woltzenlogel Paleo

Thumbnail PDF


  • Filesize: 444 kB
  • 15 pages

Document Identifiers

Author Details

Alexander Leitsch
Giselle Reis
Bruno Woltzenlogel Paleo

Cite AsGet BibTex

Alexander Leitsch, Giselle Reis, and Bruno Woltzenlogel Paleo. Towards CERes in intuitionistic logic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 485-499, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Cut-elimination, introduced by Gentzen, plays an important role in automating the analysis of mathematical proofs. The removal of cuts corresponds to the elimination of intermediate statements (lemmas), resulting in an analytic proof. CERes is a method of cut-elimination by resolution that relies on global proof transformations, in contrast to reductive methods, which use local proof-rewriting transformations. By avoiding redundant operations, it obtains a speed-up over Gentzen's traditional method (and its variations). CERes has been successfully implemented and applied to mathematical proofs, and it is fully developed for classical logic (first and higher order), multi-valued logics and Gödel logic. But when it comes to mathematical proofs, intuitionistic logic also plays an important role due to its constructive characteristics and computational interpretation. This paper presents current developments on adapting the CERes method to intuitionistic sequent calculus LJ. First of all, we briefly describe the CERes method for classical logic and the problems that arise when extending the method to intuitionistic logic. Then, we present the solutions found for the mentioned problems for the subclass LJ- (the class of intuitionistic proofs of an end-sequent containing no strong quantifiers and no formula on the right). In addition, we explain, with an example, some ideas for improving the method and covering a bigger fragment of LJ proofs. Finally, we summarize the results and point the direction for future research.
  • cut-elimination
  • resolution
  • LJ


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail