The problem of \(\Pi_{2}\)-cut-introduction. (English) Zbl 1423.03240
Summary: We describe an algorithmic method of proof compression based on the introduction of \(\Pi_2\)-cuts into a cut-free LK-proof. The current approach is based on an inversion of Gentzen’s cut-elimination method and extends former methods for introducing \(\Pi_1\)-cuts. The Herbrand instances of a cut-free proof \(\pi\) of a sequent \(S\) are described by a grammar \(G\) which encodes substitutions defined in the elimination of quantified cuts. We present an algorithm which, given a grammar \(G\), constructs a \(\Pi_2\)-cut formula \(A\) and a proof \(\pi\)’ of \(S\) with one cut on \(A\). It is shown that, by this algorithm, we can achieve an exponential proof compression.
MSC:
| 03F07 | Structure of proofs |
| 03F05 | Cut-elimination and normal-form theorems |
| 03B35 | Mechanization of proofs and logical operations |
| 03F20 | Complexity of proofs |
References:
| [1] | Afshari, B.; Hetzl, S.; Leigh, G. E., Herbrand disjunctions, cut elimination and context-free tree grammars, (13th International Conference on Typed Lambda Calculi and Applications. 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland (2015)), 1-16 · Zbl 1366.03235 |
| [2] | Baaz, M.; Egly, U.; Leitsch, A., Normal form transformations, (Handbook of Automated Reasoning (in 2 Volumes) (2001), Elsevier), 273-333 · Zbl 1005.03013 |
| [3] | Bundy, A., The automation of proof by mathematical induction, (Voronkov, A.; Robinson, J. A., Handbook of Automated Reasoning, vol. 1 (2001), Elsevier), 845-911 · Zbl 0994.03007 |
| [4] | Bundy, A.; Basin, D.; Hutter, D.; Ireland, A., Rippling: Meta-Level Guidance for Mathematical Reasoning, Cambridge Tracts in Theoretical Computer Science (2005), Cambridge University Press · Zbl 1095.68108 |
| [5] | Chomsky, N., Three models for the description of language, IRE Trans. Inf. Theory, 2, 3, 113-124 (1956) · Zbl 0156.25401 |
| [6] | Colton, S., Automated Theory Formation in Pure Mathematics (2001), University of Edinburgh, PhD thesis |
| [7] | Colton, S., Automated Theory Formation in Pure Mathematics (2002), Springer · Zbl 1219.68141 |
| [8] | D’Agostino, M.; Finger, M.; Gabbay, D., Cut-based abduction, Log. J. IGPL, 16, 537-560 (2008) · Zbl 1156.03032 |
| [9] | D’Agostino, M.; Finger, M.; Gabbay, D., Semantics and proof-theory of depth-bounded boolean logics, Theoret. Comput. Sci., 480, 43-68 (2013) · Zbl 1315.03107 |
| [10] | Ebner, G.; Hetzl, S.; Reis, G.; Riener, M.; Wolfsteiner, S.; Zivota, S., System description: GAPT 2.0, (8th International Joint Conference on Automated Reasoning, IJCAR (2016)) · Zbl 1475.68433 |
| [11] | Finger, M.; Gabbay, D., Equal rights for the cut: computable non-analytic cuts in cut-based proofs, Log. J. IGPL, 15, 5-6, 553-575 (2007) · Zbl 1159.03038 |
| [12] | Gentzen, G., Untersuchungen über das logische Schließen, Math. Z., 39, 176-210 (1935), 405-431 · Zbl 0010.14501 |
| [13] | Gentzen, G., Die Widerspruchsfreiheit der reinen Zahlentheorie, Math. Ann., 112, 493-565 (1935) · Zbl 0014.38801 |
| [14] | Hähnle, R., Tableaux and related methods, (Handbook of Automated Reasoning (in 2 volumes) (2001), Elsevier), 100-178 · Zbl 1011.68125 |
| [15] | Hetzl, S., Applying tree languages in proof theory, (Dediu, A.-H.; Martìn-Vide, C., Language and Automata Theory and Applications (2012), Springer), 301-312 · Zbl 1350.68170 |
| [16] | Hetzl, S.; Leitsch, A.; Reis, G.; Weller, D., Algorithmic introduction of quantified cuts, Theoret. Comput. Sci., 549, 1-16 (2014) · Zbl 1393.03050 |
| [17] | Ireland, A.; Bundy, A., Productive use of failure in inductive proof, J. Automat. Reason., 16, 1-2, 79-111 (1996) · Zbl 0847.68103 |
| [18] | Leitsch, A., On proof mining by cut-elimination, Math. Logic Found., 55, 173-200 (2015) · Zbl 1431.03074 |
| [19] | Takeuti, G., Proof Theory, Studies in Logic and the Foundations of Mathematics, vol. 81 (1987), North-Holland · Zbl 0609.03019 |
| [20] | Troelstra, A. S.; Schwichtenberg, H., Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, vol. 43 (1996), Cambridge University Press: Cambridge University Press Cambridge, United Kingdom · Zbl 0868.03024 |
| [21] | Vyskočil, J.; Stanovský, D.; Urban, J., Automated proof compression by invention of new definitions, (Clark, E. M.; Voronkov, A., Logic for Programming, Artifical Intelligence and Reasoning. Logic for Programming, Artifical Intelligence and Reasoning, LPAR-16. Logic for Programming, Artifical Intelligence and Reasoning. Logic for Programming, Artifical Intelligence and Reasoning, LPAR-16, Lecture Notes in Computer Science, vol. 6355 (2010), Springer), 447-462 · Zbl 1253.68293 |
| [22] | Woltzenlogel Paleo, B., Atomic cut introduction by resolution: proof structuring and compression, (Clark, E. M.; Voronkov, A., Logic for Programming, Artifical Intelligence and Reasoning. Logic for Programming, Artifical Intelligence and Reasoning, LPAR-16. Logic for Programming, Artifical Intelligence and Reasoning. Logic for Programming, Artifical Intelligence and Reasoning, LPAR-16, Lecture Notes in Computer Science, vol. 6355 (2010), Springer), 463-480 · Zbl 1253.03085 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
