×

zbMATH — the first resource for mathematics

Scalable fine-grained proofs for formula processing. (English) Zbl 1468.68278
Summary: We present a framework for processing formulas in automatic theorem provers, with generation of detailed proofs. The main components are a generic contextual recursion algorithm and an extensible set of inference rules. Clausification, Skolemization, theory-specific simplifications, and expansion of “let” expressions are instances of this framework. With suitable data structures, proof generation adds only a linear-time overhead, and proofs can be checked in linear time. We implemented the approach in the SMT solver veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced, which is important for independent checking and reconstruction in proof assistants. To validate the framework, we implemented proof reconstruction in Isabelle/HOL.

MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI Link
References:
[1] Barbosa, Haniel; Fontaine, Pascal; Reynolds, Andrew, Congruence Closure with Free Variables, Tools and Algorithms for the Construction and Analysis of Systems, 214-230 (2017), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[2] Besson, F., Fontaine, P., Théry, L.: A flexible proof format for SMT: a proposal. In: Fontaine, P., Stump, A. (eds.) PxTP 2011, pp. 15-26 (2011)
[3] Armand, M.; Faure, G.; Grégoire, B.; Keller, C.; Théry, L.; Werner, B.; Jouannaud, Jp; Shao, Z., A modular integration of SAT/SMT solvers to Coq through proof witnesses, CPP 2011, LNCS, 135-150 (2011), Berlin: Springer, Berlin · Zbl 1350.68223
[4] Blanchette, Jc; Böhme, S.; Fleury, M.; Smolka, Sj; Steckermeier, A., Semi-intelligible Isar proofs from machine-generated proofs, J. Autom. Reason., 56, 2, 155-200 (2016) · Zbl 1356.68178
[5] Ebner, Gabriel; Hetzl, Stefan; Reis, Giselle; Riener, Martin; Wolfsteiner, Simon; Zivota, Sebastian, System Description: GAPT 2.0, Automated Reasoning, 293-301 (2016), Cham: Springer International Publishing, Cham · Zbl 06623268
[6] Böhme, S.; Weber, T.; Kaufmann, M.; Paulson, L., Fast LCF-style proof reconstruction for Z3, ITP 2010, LNCS, 179-194 (2010), Berlin: Springer, Berlin · Zbl 1291.68328
[7] Barbosa, H.; Blanchette, Jc; Fontaine, P.; De Moura, L., Scalable fine-grained proofs for formula processing, CADE-26, LNCS (2017), Berlin: Springer, Berlin · Zbl 06778417
[8] Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.5. Technical Report, University of Iowa (2015). http://smt-lib.org/
[9] Sutcliffe, Geoff; Schulz, Stephan; Claessen, Koen; Baumgartner, Peter, The TPTP Typed First-Order Form with Arithmetic, Logic for Programming, Artificial Intelligence, and Reasoning, 406-419 (2012), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1352.68217
[10] Gordon, Mjc; Melham, Tf, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic (1993), Cambridge: Cambridge University Press, Cambridge
[11] De Nivelle, H., Translation of resolution proofs into short first-order proofs without choice axioms, Inf. Comput., 199, 1-2, 24-54 (2005) · Zbl 1081.03014
[12] Paulson, Lc; Susanto, Kw; Schneider, K.; Brandt, J., Source-level proof reconstruction for interactive theorem proving, TPHOLs 2007, LNCS, 232-245 (2007), Berlin: Springer, Berlin · Zbl 1144.68364
[13] Nonnengart, A.; Weidenbach, C.; Robinson, A.; Voronkov, A., Computing small clause normal forms, Handbook of Automated Reasoning, 335-367 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 0992.03018
[14] Barrett, C.; De Moura, L.; Fontaine, P.; Woltzenlogel Paleo, B.; Delahaye, D., Proofs in satisfiability modulo theories, All About Proofs, Proofs for All, Mathematical Logic and Foundations, 23-44 (2015), New York: College Publications, New York
[15] Déharbe, D.; Fontaine, P.; Merz, S.; Woltzenlogel Paleo, B.; Bjørner, N.; Sofronie-Stokkermans, V., Exploiting symmetry in SMT problems, CADE-23, LNCS, 222-236 (2011), Berlin: Springer, Berlin · Zbl 1341.68187
[16] Bouton, T.; De Oliveira, Dcb; Déharbe, D.; Fontaine, P.; Schmidt, Ra, veriT: an open, trustable and efficient SMT-solver, CADE-22, LNCS, 151-156 (2009), Berlin: Springer, Berlin
[17] Nipkow, T.; Paulson, Lc; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-order Logic, LNCS (2002), Berlin: Springer, Berlin · Zbl 0994.68131
[18] Gordon, Mjc; Milner, R.; Wadsworth, Cp, Edinburgh LCF: A Mechanised Logic of Computation, LNCS (1979), Berlin: Springer, Berlin
[19] Böhme, S.: Proving theorems of higher-order logic with SMT solvers. Ph.D. Thesis, Technische Universität München (2012)
[20] Baaz, M.; Egly, U.; Leitsch, A.; Robinson, Ja; Voronkov, A., Normal form transformations, Handbook of Automated Reasoning, 273-333 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 1005.03013
[21] Reger, G., Suda, M., Voronkov, A.: New techniques in clausal form generation. In: Benzmüller, C., Sutcliffe, G., Rojas, R. (eds.) GCAI 2016, EPiC Series in Computing, vol. 41, pp. 11-23. EasyChair (2016)
[22] Kotelnikov, E., Kovács, L., Suda, M., Voronkov, A.: A clausal normal form translation for FOOL. In: Benzmüller, C., Sutcliffe, G., Rojas, R. (eds.) GCAI 2016, EPiC Series in Computing, vol. 41, pp. 53-71. EasyChair (2016)
[23] Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP data-exchange formats for automated theorem proving tools. In: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, Frontiers in Artificial Intelligence and Applications, vol. 112, pp. 201-215. IOS Press, Amsterdam (2004)
[24] Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A., (eds.) LPAR-19, LNCS, vol. 8312, pp. 735-743. Springer, Berlin (2013) · Zbl 1407.68442
[25] Kovács, Laura; Voronkov, Andrei, First-Order Theorem Proving and Vampire, Computer Aided Verification, 1-35 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[26] Weidenbach, Christoph; Dimova, Dilyana; Fietzke, Arnaud; Kumar, Rohit; Suda, Martin; Wischnewski, Patrick, SPASS Version 3.5, Automated Deduction - CADE-22, 140-145 (2009), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[27] de Moura, L.M., Bjørner, N.: Proofs and refutations, and Z3. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) LPAR 2008 Workshops, CEUR Workshop Proceedings, vol. 418. CEUR-WS.org (2008)
[28] Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. In: LICS’87, pp. 194-204. IEEE Computer Society (1987) · Zbl 0778.03004
[29] Stump, A., Proof checking technology for satisfiability modulo theories, Electron. Notes Theor. Comput. Sci., 228, 121-133 (2009)
[30] Katz, G.; Barrett, Cw; Tinelli, C.; Reynolds, A.; Hadarean, L.; Piskac, R.; Talupur, M., Lazy proofs for DPLL(T)-based SMT solvers, FMCAD 2016, 93-100 (2016), New York: IEEE Computer Society, New York
[31] Hadarean, L.; Barrett, Cw; Reynolds, A.; Tinelli, C.; Deters, M.; Davis, M.; Fehnker, A.; Mciver, A.; Voronkov, A., Fine grained SMT proofs for the theory of fixed-width bit-vectors, LPAR-20, LNCS, 340-355 (2015), Berlin: Springer, Berlin · Zbl 1471.68143
[32] Moskal, M.: Rocket-fast proof checking for SMT solvers. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 486-500. Springer, Berlin (2008) · Zbl 1134.68492
[33] Barendregt, H.; Wiedijk, F., The challenge of computer mathematics, Philos. Trans. R. Soc. Lond. Ser. A, 363, 1835, 2351-2375 (2005) · Zbl 1152.03304
[34] Berghofer, S.; Nipkow, T.; Aagaard, M.; Harrison, J., Proof terms for simply typed higher order logic, TPHOLs 2000, LNCS, 38-52 (2000), Berlin: Springer, Berlin · Zbl 0974.03013
[35] Cousineau, D.; Dowek, G.; Rocca, Srd, Embedding pure type systems in the lambda-Pi-calculus modulo, TLCA 2007, LNCS, 102-117 (2007), Berlin: Springer, Berlin · Zbl 1215.03021
[36] Guglielmi, A., A system of interaction and structure, ACM Trans. Comput. Log., 8, 1, 1 (2007) · Zbl 1367.03110
[37] Graham-Lengrand, S.; Galmiche, D.; Larchey-Wendling, D., Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture, TABLEAUX 2013, LNCS, 149-156 (2013), Berlin: Springer, Berlin · Zbl 1401.68277
[38] Paulson, Lc, A higher-order implementation of rewriting, Sci. Comput. Program., 3, 2, 119-149 (1983) · Zbl 0551.68076
[39] Meier, A.: Tramp: transformation of machine-found proofs into natural deduction proofs at the assertion level (system description). In: McAllester, D. (ed.) CADE-17, LNCS, vol. 1831, pp. 460-464. Springer, Berlin (2000) · Zbl 0963.68537
[40] De Nivelle, H.; Bradfield, Jc, Extraction of proofs from the clausal normal form transformation, CSL 2002, LNCS, 584-598 (2002), Berlin: Springer, Berlin · Zbl 1020.03009
[41] Mclaughlin, S.; Barrett, C.; Ge, Y., Cooperating theorem provers: a case study combining HOL-light and CVC lite, Electron. Notes Theor. Comput. Sci., 144, 2, 43-51 (2006) · Zbl 1272.68362
[42] Fontaine, P.; Marion, Jy; Merz, S.; Nieto, Lp; Tiu, A.; Hermanns, H.; Palsberg, J., Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants, TACAS 2006, LNCS, 167-181 (2006), Berlin: Springer, Berlin · Zbl 1180.68240
[43] Böhme, S.; Fox, Acj; Sewell, T.; Weber, T.; Jouannaud, J.; Shao, Z., Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL, CPP 2011, LNCS, 183-198 (2011), Berlin: Springer, Berlin · Zbl 1350.68225
[44] Ekici, Burak; Katz, Guy; Keller, Chantal; Mebsout, Alain; Reynolds, Andrew J.; Tinelli, Cesare, Extending SMTCoq, a Certified Checker for SMT (Extended Abstract), Electronic Proceedings in Theoretical Computer Science, 210, 21-29 (2016)
[45] Zimmer, J., Meier, A., Sutcliffe, G., Zhan, Y.: Integrated proof transformation services. In: Benzmüller, C., Windsteiger, W. (eds.) IJCAR WS 7 (2004)
[46] Hetzl, S.; Libal, T.; Riener, M.; Rukhaia, M.; Galmiche, D.; Larchey-Wendling, D., Understanding resolution proofs through Herbrand’s theorem, TABLEAUX 2013, LNCS, 157-171 (2013), Berlin: Springer, Berlin · Zbl 1401.03038
[47] Burel, G.: A shallow embedding of resolution and superposition proofs into the \(\lambda \Pi \)-calculus modulo. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013, EPiC Series in Computing, vol. 14, pp. 43-57. EasyChair (2013)
[48] Miller, D.; Falaschi, M., Proof checking and logic programming, LOPSTR 2015, LNCS, 3-17 (2015), Berlin: Springer, Berlin · Zbl 1362.68055
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.