×

Extraction of expansion trees. (English) Zbl 1468.68296

Summary: We define a new method for proof mining by CERES (cut-elimination by resolution) that is concerned with the extraction of expansion trees in first-order logic [D. A. Miller, Stud. Log. 46, 347–370 (1987; Zbl 0644.03033)] with equality. In the original CERES method expansion trees can be extracted from proofs in normal form (proofs without quantified cuts) as a post-processing of cut-elimination. More precisely they are extracted from an ACNF, a proof with at most atomic cuts. We define a novel method avoiding proof normalization and show that expansion trees can be extracted from the resolution refutation and the corresponding proof projections. We prove that the new method asymptotically outperforms the standard method (which first computes the ACNF and then extracts an expansion tree). Finally we compare an implementation of the new method with the old one; it turns out that the new method is also more efficient in our experiments.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B35 Mechanization of proofs and logical operations
03F05 Cut-elimination and normal-form theorems
68V20 Formalization of mathematics in connection with theorem provers

Citations:

Zbl 0644.03033

Software:

ProofTool; GAPT; CERES
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: Cut-elimination: experiments with ceres. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 481-495. Springer (2005) · Zbl 1108.03305
[2] Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: Proof transformation by CERES. In: Proceedingsof 5th International Conference on Mathematical Knowledge Management, MKM 2006, Wokingham, UK, August 11-12, 2006, pp. 82-93 (2006) · Zbl 1125.03012
[3] Baaz, M., Leitsch, A.: On skolemization and proof complexity. Fundam. Inf. 20(4), 353-379 (1994) · Zbl 0815.03003
[4] Baaz, M., Leitsch, A.: Cut-elimination and redundancy-elimination by resolution. J. Symb. Comput. 29(2), 149-177 (2000) · Zbl 0976.03059 · doi:10.1006/jsco.1999.0359
[5] Baaz, M., Leitsch, A.: Towards a clausal analysis of cut-elimination. J. Symb. Comput. 41(3), 381-410 (2006) · Zbl 1125.03013 · doi:10.1016/j.jsc.2003.10.005
[6] Baaz, M., Leitsch, A.: Methods of Cut-Elimination, vol. 34. Springer, Berlin (2011) · Zbl 1225.03075
[7] Baaz, M., Leitsch, A.: Cut-elimination: syntax and semantics. Stud. Log. 102(6), 1217-1244 (2014) · Zbl 1354.03086 · doi:10.1007/s11225-014-9563-2
[8] Berger, U., Berghofer, S., Letouzey, P., Schwichtenberg, H.: Program extraction from normalization proofs. Stud. Log. 82(1), 25-49 (2006) · Zbl 1095.03016 · doi:10.1007/s11225-006-6604-5
[9] Berger, U., Buchholz, W., Schwichtenberg, H.: Refined program extraction from classical proofs. Ann. Pure Appl. Log. 114(1), 3-25 (2002) · Zbl 0992.03070 · doi:10.1016/S0168-0072(01)00073-2
[10] Buss, S.R.: On Herbrand’s theorem. In: Leivant, D. (ed.) Logical and Computational Complexity. Selected Papers. Logic and Computational Complexity, International Workshop LCC ’94, Indianapolis, Indiana, USA, 13-16 October 1994. Lecture Notes in Computer Science, vol. 960, pp. 195-209. Springer (1994)
[11] Dunchev, C., Leitsch, A., Libal, T., Riener, M., Rukhaia, M., Weller, D., Woltzenlogel-Paleo, B.: Prooftool: a gui for the gapt framework. arXiv preprint arXiv:1307.1942 (2013)
[12] Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S., Zivota, S.: System description: Gapt 2.0. In: International Joint Conference on Automated Reasoning, pp. 293-301. Springer (2016) · Zbl 1475.68433
[13] Fürstenberg, H.: On the infinitude of the primes. Am. Math. Mon. 62, 353 (1955) · Zbl 1229.11009 · doi:10.2307/2307043
[14] Fürstenberg, H.: Topological dynamics and combinatorial number theory. J. Anal. Math. 34(1), 61-85 (1978) · Zbl 0425.54023 · doi:10.1007/BF02790008
[15] Gentzen, G.: Untersuchungen über das logische Schließen. Math. Z. 39, 176-210, 405-431 (1934-35) · Zbl 0010.14601
[16] Girard, J.Y.: Proof Theory and Logical Complexity, vol. 1. Biblopolis, Napoli (1987) · Zbl 0635.03052
[17] Gödel, K.: Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12(3-4), 280-287 (1958) · Zbl 0090.01003 · doi:10.1111/j.1746-8361.1958.tb01464.x
[18] Herbrand, J.: Recherches sur la théorie de la démonstration. PhD thesis, Université de Paris (1930) · JFM 56.0824.02
[19] Hetzl, S., Leitsch, A., Weller, D.: Ceres in higher-order logic. Ann. Pure Appl. Log. 162(12), 1001-1034 (2011) · Zbl 1259.03071 · doi:10.1016/j.apal.2011.06.005
[20] Hetzl, S., Leitsch, A., Weller, D., Paleo, B.W.: Herbrand sequent extraction. In: Autexier, S., Campbell, J.A., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) Proceedings of Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, 28 July-1 August 2008. Lecture Notes in Computer Science, vol. 5144, pp. 462-477. Springer (2008) · Zbl 1166.68347
[21] Hetzl, S., Libal, T., Riener, M., Rukhaia, M.: Understanding resolution proofs through Herbrands theorem. In: Galmiche, D., Larchey-Wendling, D. (eds.) Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Nancy, France, 16-19 September 2013. Lecture Notes in Computer Science, vol. 8123, pp. 157-171. Springer (2013) · Zbl 1401.03038
[22] Hetzl, S., Weller, D.: Expansion trees with cut. arXiv preprint arXiv:1308.0428 (2013) · Zbl 1456.03085
[23] Miller, D.A.: A compact representation of proofs. Stud. Log. 46(4), 347-370 (1987) · Zbl 0644.03033 · doi:10.1007/BF00370646
[24] Pfenning, F.: Analytic and non-analytic proofs. In: 7th International Conference on Automated Deduction, pp. 394-413. Springer (1984) · Zbl 0547.03032
[25] Reis, G.: Importing SMT and connection proofs as expansion trees. arXiv preprint arXiv:1507.08715 (2015)
[26] Urban, C.: Classical logic and computation. PhD thesis, University of Cambridge (2000)
[27] Van der Waerden, B.L.: Beweis einer Baudetschen Vermutung. Nieuw Arch. Wiskd. 15(2), 212-216 (1927) · JFM 53.0073.12
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.