Advertisement

Scalable Fine-Grained Proofs for Formula Processing

  • Haniel Barbosa
  • Jasmin Christian Blanchette
  • Mathias Fleury
  • Pascal Fontaine
Article
  • 23 Downloads

Abstract

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.

Keywords

SMT Formula processing Rewriting Proof production Proof reconstruction Proof checking 

Notes

Acknowledgements

We thank Simon Cruanes for discussing many aspects of the framework with us as it was emerging. We also thank Robert Lewis, Stephan Merz, Lawrence Paulson, Anders Schlichtkrull, Hans-Jörg Schurr, Mark Summerfield, Sophie Tourret, and the anonymous reviewers for suggesting many improvements. The work has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (Grant Agreement No. 713999, Matryoshka). Experiments presented in this article were carried out using the Grid’5000 testbed (https://www.grid5000.fr/), supported by a scientific interest group hosted by Inria and including CNRS, RENATER, and several universities as well as other organizations. A mirror of all the software and evaluation data described in this article is hosted by Zenodo (https://doi.org/10.5281/zenodo.582482).

References

  1. 1.
    Barbosa, H., Fontaine, P., Reynolds, A.: Congruence closure with free variables. In: Legay, A., Margaria, T. (eds.) TACAS 2017, LNCS, vol. 10206, pp. 214–230 (2017)Google Scholar
  2. 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)Google Scholar
  3. 3.
    Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of SAT/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.P., Shao, Z. (eds.) CPP 2011, LNCS, vol. 7086, pp. 135–150. Springer, Berlin (2011)Google Scholar
  4. 4.
    Blanchette, J.C., Böhme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. J. Autom. Reason. 56(2), 155–200 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S., Zivota, S.: System description: GAPT 2.0. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706, pp. 293–301. Springer, Berlin (2016)Google Scholar
  6. 6.
    Böhme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L. (eds.) ITP 2010, LNCS, vol. 6172, pp. 179–194. Springer, Berlin (2010)Google Scholar
  7. 7.
    Barbosa, H., Blanchette, J.C., Fontaine, P.: Scalable fine-grained proofs for formula processing. In: de Moura, L. (ed.) CADE-26, LNCS. Springer, Berlin (2017)Google Scholar
  8. 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. 9.
    Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18, LNCS, vol. 7180, pp. 406–419. Springer, Berlin (2012)Google Scholar
  10. 10.
    Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)zbMATHGoogle Scholar
  11. 11.
    de Nivelle, H.: Translation of resolution proofs into short first-order proofs without choice axioms. Inf. Comput. 199(1–2), 24–54 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007, LNCS, vol. 4732, pp. 232–245. Springer, Berlin (2007)Google Scholar
  13. 13.
    Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 335–367. Elsevier, Amsterdam (2001)CrossRefGoogle Scholar
  14. 14.
    Barrett, C., de Moura, L., Fontaine, P.: Proofs in satisfiability modulo theories. In: Woltzenlogel Paleo, B., Delahaye, D. (eds.) All About Proofs, Proofs for All, Mathematical Logic and Foundations, vol. 55, pp. 23–44. College Publications, New York (2015)Google Scholar
  15. 15.
    Déharbe, D., Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Exploiting symmetry in SMT problems. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE-23, LNCS, vol. 6803, pp. 222–236. Springer, Berlin (2011)Google Scholar
  16. 16.
    Bouton, T., de Oliveira, D.C.B., Déharbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE-22, LNCS, vol. 5663, pp. 151–156. Springer, Berlin (2009)Google Scholar
  17. 17.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-order Logic, LNCS, vol. 2283. Springer, Berlin (2002)zbMATHGoogle Scholar
  18. 18.
    Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation, LNCS, vol. 78. Springer, Berlin (1979)zbMATHGoogle Scholar
  19. 19.
    Böhme, S.: Proving theorems of higher-order logic with SMT solvers. Ph.D. Thesis, Technische Universität München (2012)Google Scholar
  20. 20.
    Baaz, M., Egly, U., Leitsch, A.: Normal form transformations. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 273–333. Elsevier, Amsterdam (2001)CrossRefGoogle Scholar
  21. 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)Google Scholar
  22. 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)Google Scholar
  23. 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)Google Scholar
  24. 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)Google Scholar
  25. 25.
    Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013, LNCS, vol. 8044, pp. 1–35. Springer, Berlin (2013).  https://doi.org/10.1007/978-3-642-39799-8_1
  26. 26.
    Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22, LNCS, vol. 5663, pp. 140–145. Springer, Berlin (2009)Google Scholar
  27. 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)Google Scholar
  28. 28.
    Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. In: LICS’87, pp. 194–204. IEEE Computer Society (1987)Google Scholar
  29. 29.
    Stump, A.: Proof checking technology for satisfiability modulo theories. Electron. Notes Theor. Comput. Sci. 228, 121–133 (2009)CrossRefGoogle Scholar
  30. 30.
    Katz, G., Barrett, C.W., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy proofs for DPLL(T)-based SMT solvers. In: Piskac, R., Talupur, M. (eds.) FMCAD 2016, pp. 93–100. IEEE Computer Society, New York (2016)Google Scholar
  31. 31.
    Hadarean, L., Barrett, C.W., Reynolds, A., Tinelli, C., Deters, M.: Fine grained SMT proofs for the theory of fixed-width bit-vectors. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20, LNCS, vol. 9450, pp. 340–355. Springer, Berlin (2015)Google Scholar
  32. 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)Google Scholar
  33. 33.
    Barendregt, H., Wiedijk, F.: The challenge of computer mathematics. Philos. Trans. R. Soc. Lond. Ser. A 363(1835), 2351–2375 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  34. 34.
    Berghofer, S., Nipkow, T.: Proof terms for simply typed higher order logic. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000, LNCS, vol. 1869, pp. 38–52. Springer, Berlin (2000)Google Scholar
  35. 35.
    Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-Pi-calculus modulo. In: Rocca, S.R.D. (ed.) TLCA 2007, LNCS, vol. 4583, pp. 102–117. Springer, Berlin (2007)Google Scholar
  36. 36.
    Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Log. 8(1), 1 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  37. 37.
    Graham-Lengrand, S.: Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013, LNCS, vol. 8123, pp. 149–156. Springer, Berlin (2013)Google Scholar
  38. 38.
    Paulson, L.C.: A higher-order implementation of rewriting. Sci. Comput. Program. 3(2), 119–149 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  39. 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)Google Scholar
  40. 40.
    de Nivelle, H.: Extraction of proofs from the clausal normal form transformation. In: Bradfield, J.C. (ed.) CSL 2002, LNCS, vol. 2471, pp. 584–598. Springer, Berlin (2002)Google Scholar
  41. 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)CrossRefzbMATHGoogle Scholar
  42. 42.
    Fontaine, P., Marion, J.Y., Merz, S., Nieto, L.P., Tiu, A.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006, LNCS, vol. 3920, pp. 167–181. Springer, Berlin (2006)Google Scholar
  43. 43.
    Böhme, S., Fox, A.C.J., Sewell, T., Weber, T.: Reconstruction of Z3’s bit-vector proofs in HOL4 and Isabelle/HOL. In: Jouannaud, J., Shao, Z. (eds.) CPP 2011, LNCS, vol. 7086, pp. 183–198. Springer, Berlin (2011)Google Scholar
  44. 44.
    Ekici, B., Katz, G., Keller, C., Mebsout, A., Reynolds, A.J., Tinelli, C.: Extending SMTCoq, a certified checker for SMT (extended abstract). In: Blanchette, J.C., Kaliszyk, C. (eds.) HaTT 2016, EPTCS, vol. 210, pp. 21–29 (2016)Google Scholar
  45. 45.
    Zimmer, J., Meier, A., Sutcliffe, G., Zhan, Y.: Integrated proof transformation services. In: Benzmüller, C., Windsteiger, W. (eds.) IJCAR WS 7 (2004)Google Scholar
  46. 46.
    Hetzl, S., Libal, T., Riener, M., Rukhaia, M.: Understanding resolution proofs through Herbrand’s theorem. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013, LNCS, vol. 8123, pp. 157–171. Springer, Berlin (2013)Google Scholar
  47. 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)Google Scholar
  48. 48.
    Miller, D.: Proof checking and logic programming. In: Falaschi, M. (ed.) LOPSTR 2015, LNCS, vol. 9527, pp. 3–17. Springer, Berlin (2015)Google Scholar

Copyright information

© Springer Nature B.V. 2019

Authors and Affiliations

  1. 1.University of IowaIowa CityUSA
  2. 2.CNRS, Inria, LORIAUniversité de LorraineNancyFrance
  3. 3.Vrije Universiteit AmsterdamAmsterdamThe Netherlands
  4. 4.Max-Planck-Institute für InformatikSaarbrückenGermany
  5. 5.Saarbrücken Graduate School of Computer ScienceUniversität des SaarlandesSaarbrückenGermany

Personalised recommendations