Search Results

Documents authored by Reis, Giselle

Towards CERes in intuitionistic logic

Authors: Alexander Leitsch, Giselle Reis, and Bruno Woltzenlogel Paleo

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (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.

Cite as

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)

Copy BibTex To Clipboard

  author =	{Leitsch, Alexander and Reis, Giselle and Woltzenlogel Paleo, Bruno},
  title =	{{Towards CERes in intuitionistic logic}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{485--499},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-36922},
  doi =		{10.4230/LIPIcs.CSL.2012.485},
  annote =	{Keywords: cut-elimination, resolution, LJ}
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