Atomic Cut Introduction by Resolution: Proof Structuring and Compression

  • Bruno Woltzenlogel Paleo
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)


The careful introduction of cut inferences can be used to structure and possibly compress formal sequent calculus proofs. This paper presents CIRes, an algorithm for the introduction of atomic cuts based on various modifications and improvements of the CERes method, which was originally devised for efficient cut-elimination. It is also demonstrated that CIRes is capable of compressing proofs, and the amount of compression is shown to be exponential in the length of proofs.


Atomic Formula Sequent Calculus Complete Binary Tree Proof Structure Clause Form 
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. 1.
    Baaz, M., Ciabattoni, A., Fermüller, C.: Cut elimination for first order gödel logic by hyperclause resolution. In: Logic for Programming, Artificial Intelligence, and Reasoning, pp. 451–466 (2008)Google Scholar
  2. 2.
    Baaz, M., Egly, U., Leitsch, A.: Normal form transformations. In: Voronkov, A., Robinson, A. (eds.) Handbook of Automated Reasoning, pp. 275–333. Elsevier, Amsterdam (2001)Google Scholar
  3. 3.
    Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: Cut-Elimination: Experiments with CERES. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 481–495. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  4. 4.
    Baaz, M., Leitsch, A.: Cut-elimination and Redundancy-elimination by Resolution. Journal of Symbolic Computation 29(2), 149–176 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Baaz, M., Leitsch, A.: Comparing the complexity of cut-elimination methods. Proof Theory in Computer Science, 49–67 (2001)Google Scholar
  6. 6.
    Baaz, M., Leitsch, A.: Ceres in many-valued logics. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 1–20. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  7. 7.
    Baaz, M., Leitsch, A.: Methods of Cut-Elimination (2009) (to appear)Google Scholar
  8. 8.
    Baaz, M., Zach, R.: Algorithmic structuring of cut-free proofs. In: Martini, S., Börger, E., Kleine Büning, H., Jäger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 29–42. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  9. 9.
    Cook, S., Reckhow, R.: On the lengths of proofs in the propositional calculus (preliminary version). In: STOC 1974: Proceedings of the Sixth Annual ACM Symposium on Theory of Computing, pp. 135–148. ACM, New York (1974)CrossRefGoogle Scholar
  10. 10.
    Egly, U., Genther, K.: Structuring of computer-generated proofs by cut introduction. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1997. LNCS, vol. 1289, pp. 140–152. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  11. 11.
    Finger, M., Gabbay, D.M.: Equal rights for the cut: Computable non-analytic cuts in cut-based proofs. Logic Journal of the IGPL 15(5-6), 553–575 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Hetzl, S.: Proof Fragments, Cut-Elimination and Cut-Introduction (manuscript)Google Scholar
  13. 13.
    Hetzl, S.: Proof Profiles. Characteristic Clause Sets and Proof Transformations. VDM (2008)Google Scholar
  14. 14.
    Hetzl, S., Leitsch, A., Weller, D., Paleo, B.W.: Herbrand sequent extraction. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS (LNAI), vol. 5144, pp. 462–477. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  15. 15.
    Miller, D., Nigam, V.: Incorporating tables into proofs. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 466–480. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  16. 16.
    Nigam, V.: Using tables to construct non-redundant proofs. In: CiE 2008: Abstracts and extended abstracts of unpublished papers (2008)Google Scholar
  17. 17.
    Orevkov, V.P.: Lower bounds for increasing complexity of derivations after cut-elimination (translation). Journal Sov. Math. (1982), 2337–2350 (1979)Google Scholar
  18. 18.
    Statman, R.: Lower bounds on Herbrand’s theorem. Proceedings of the American Mathematical Society 75, 104–107 (1979)MathSciNetzbMATHGoogle Scholar
  19. 19.
    Urquhart, A.: The complexity of propositional proofs. Bulletin of Symbolic Logic 1(4), 425–467 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Weller, D.: Skolemization Problems and Cut-elimination (In Preparation). PhD thesis, Technische Universitaet Wien (Vienna University of Technology) (2009)Google Scholar
  21. 21.
    Paleo, B.W.: A General Analysis of Cut-Elimination by CERes. PhD thesis, Vienna University of Technology (2009)Google Scholar
  22. 22.
    Paleo, B.W.: Physics and proof theory. In: International Workshop on Physics and Computation (2010)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Bruno Woltzenlogel Paleo
    • 1
    • 2
  1. 1.Institut für ComputersprachenVienna University of TechnologyAustria
  2. 2.INRIA, LORIANancyFrance

Personalised recommendations