Abstract
We describe a method for abbreviating an analytic proof in classical first-order logic by the introduction of a lemma. Our algorithm is based on first computing a compressed representation of the terms present in the analytic proof and then a cut-formula that realizes such a compression. This method can be applied to the output of automated theorem provers, which typically produce analytic proofs.
This work was supported by a Marie Curie Intra European Fellowship within the 7th European Community Framework Programme and by the projects P-22028-N13 and I-603 N18 of the Austrian Science Fund (FWF).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Finger, M., Gabbay, D.: Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs. Logic Journal of the IGPL 15(5–6), 553–575 (2007)
Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39, 176–210, 405–431 (1934–1935)
Hetzl, S.: Describing proofs by short tautologies. Annals of Pure and Applied Logic 159(1–2), 129–145 (2009)
Hetzl, S.: Applying Tree Languages in Proof Theory. In: Dediu, A.-H., Martín-Vide, C. (eds.) LATA 2012. LNCS, vol. 7183, pp. 301–312. Springer, Heidelberg (2012)
Hetzl, S., Leitsch, A., Weller, D.: Towards Algorithmic Cut-Introduction. technical report, http://www.logic.at/people/hetzl/
Hetzl, S., Leitsch, A., Weller, D., Woltzenlogel Paleo, B.: Herbrand Sequent Extraction. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC/Calculemus/MKM 2008. LNCS (LNAI), vol. 5144, pp. 462–477. Springer, Heidelberg (2008)
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)
Orevkov, V.P.: Lower bounds for increasing complexity of derivations after cut elimination. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta 88, 137–161 (1979)
Pudlák, P.: The Lengths of Proofs. In: Buss, S. (ed.) Handbook of Proof Theory, pp. 547–637. Elsevier (1998)
Statman, R.: Lower bounds on Herbrand’s theorem. Proceedings of the American Mathematical Society 75, 104–107 (1979)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (2000)
Vyskočil, J., Stanovský, D., Urban, J.: Automated Proof Compression by Invention of New Definitions. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 447–462. Springer, Heidelberg (2010)
Woltzenlogel Paleo, B.: Atomic Cut Introduction by Resolution: Proof Structuring and Compression. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 463–480. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hetzl, S., Leitsch, A., Weller, D. (2012). Towards Algorithmic Cut-Introduction. In: Bjørner, N., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2012. Lecture Notes in Computer Science, vol 7180. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28717-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-28717-6_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28716-9
Online ISBN: 978-3-642-28717-6
eBook Packages: Computer ScienceComputer Science (R0)