Skip to main content
SpringerLink
Log in

Scalable Fine-Grained Proofs for Formula Processing

  • Conference paper
  • First Online:
Book cover Automated Deduction – CADE 26 (CADE 2017)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10395))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    http://isabelle.in.tum.de/repos/isabelle/file/00731700e54f/src/HOL/ex/veriT_Preprocessing.thy.

  2. 2.

    http://matryoshka.gforge.inria.fr/pubs/processing/veriT.tar.gz.

  3. 3.

    http://matryoshka.gforge.inria.fr/pubs/processing/.

References

  1. 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, Heidelberg (2011). doi:10.1007/978-3-642-25379-9_12

    Chapter  Google Scholar 

  2. Barbosa, H., Blanchette, J.C., Fontaine, P.: Technical report associated with this paper (2017). https://hal.inria.fr/hal-01526841

  3. 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. Springer, Heidelberg (2017). doi:10.1007/978-3-662-54580-5_13

    Chapter  Google Scholar 

  4. Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: Version 2.5. Technical report, University of Iowa (2015). http://smt-lib.org/

  5. 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 

  6. Blanchette, J.C., Böhme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. J. Autom. Reasoning 56(2), 155–200 (2016). doi:10.1007/s10817-015-9335-3

    Article  MathSciNet  MATH  Google Scholar 

  7. Böhme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179–194. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14052-5_14

    Chapter  Google Scholar 

  8. 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, Heidelberg (2009). doi:10.1007/978-3-642-02959-2_12

    Google Scholar 

  9. Déharbe, D., Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Exploiting symmetry in SMT problems. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 222–236. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22438-6_18

    Google Scholar 

  10. 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, Cham (2016). doi:10.1007/978-3-319-40229-1_20

    Google Scholar 

  11. Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979). doi:10.1007/3-540-09724-4

    MATH  Google Scholar 

  12. Hadarean, L., Barrett, C., 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 2015. LNCS, vol. 9450, pp. 340–355. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48899-7_24

    Chapter  Google Scholar 

  13. Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. In: LICS 1987, pp. 194–204. IEEE Computer Society (1987)

    Google Scholar 

  14. 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 (2016). doi:10.1109/FMCAD.2016.7886666

  15. 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, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_1

    Chapter  Google Scholar 

  16. 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, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_38

    Chapter  Google Scholar 

  17. 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 (2008). CEUR-WS.org

  18. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). doi:10.1007/3-540-45949-9

    MATH  Google Scholar 

  19. de Nivelle, H.: Translation of resolution proofs into short first-order proofs without choice axioms. Inf. Comput. 199(1–2), 24–54 (2005). doi:10.1016/j.ic.2004.10.011

    Article  MathSciNet  MATH  Google Scholar 

  20. Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 335–367. Elsevier and MIT Press (2001)

    Google Scholar 

  21. Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactivetheorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 232–245. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74591-4_18

    Google Scholar 

  22. Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013). doi:10.1007/978-3-642-45221-5_49

    Chapter  Google Scholar 

  23. Stump, A.: Proof checking technology for satisfiability modulo theories. Electr. Notes Theor. Comput. Sci. 228, 121–133 (2009). doi:10.1016/j.entcs.2008.12.121

    Article  Google Scholar 

  24. 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 (2004)

    Google Scholar 

  25. 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, Heidelberg (2009). doi:10.1007/978-3-642-02959-2_10

    Google Scholar 

Download references

Acknowledgment

We thank Simon Cruanes for discussing many aspects of the framework with us as it was emerging, and we thank Robert Lewis, Stephan Merz, Lawrence Paulson, Anders Schlichtkrull, Mark Summerfield, Sophie Tourret, and the anonymous reviewers for suggesting many textual improvements. This research has been partially supported by the Agence nationale de la recherche/Deutsche Forschungsgemeinschaft project SMArT (ANR-13-IS02-0001, STU 483/2-1) and by the European Union project SC\(^\mathsf {2}\) (grant agreement No. 712689). The work has also received funding from the European Research Council under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Experiments presented in this paper 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 paper is hosted by Zenodo (https://doi.org/10.5281/zenodo.582482).

Author information

Authors and Affiliations

  1. Université de Lorraine, CNRS, Inria, LORIA, Nancy, France

    Haniel Barbosa, Jasmin Christian Blanchette & Pascal Fontaine

  2. Universidade Federal do Rio Grande do Norte, Natal, Brazil

    Haniel Barbosa

  3. Vrije Universiteit Amsterdam, Amsterdam, The Netherlands

    Jasmin Christian Blanchette

  4. Max-Planck-Institut für Informatik, Saarbrücken, Germany

    Jasmin Christian Blanchette

Authors
  1. Haniel Barbosa
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jasmin Christian Blanchette
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Pascal Fontaine
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Haniel Barbosa .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Leonardo de Moura

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Barbosa, H., Blanchette, J.C., Fontaine, P. (2017). Scalable Fine-Grained Proofs for Formula Processing. In: de Moura, L. (eds) Automated Deduction – CADE 26. CADE 2017. Lecture Notes in Computer Science(), vol 10395. Springer, Cham. https://doi.org/10.1007/978-3-319-63046-5_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63046-5_25

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63045-8

  • Online ISBN: 978-3-319-63046-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation