Top

Journal of Automated Reasoning

Published in:

04-01-2019

Scalable Fine-Grained Proofs for Formula Processing

Authors: Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine

Published in: Journal of Automated Reasoning | Issue 3/2020

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

previous article A Resolution-Based Theorem Prover for : Architecture, Refinements, Strategies and Experiments

next article Preface: Selected Extended Papers of CADE 2017

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

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

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

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

http://isabelle.in.tum.de/repos/isabelle/file/8050734eee3e/src/HOL/Tools/SMT/.

http://isabelle.in.tum.de/repos/isabelle/file/44e1c9f93755/src/HOL/SMT_Examples/SMT_Examples.thy.

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)CrossRef

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)

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)

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)MathSciNetCrossRef

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)CrossRef

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)

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)

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

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)CrossRef

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)MATH

11.

de Nivelle, H.: Translation of resolution proofs into short first-order proofs without choice axioms. Inf. Comput. 199(1–2), 24–54 (2005)MathSciNetCrossRef

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)

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)CrossRef

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)

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)

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)

17.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-order Logic, LNCS, vol. 2283. Springer, Berlin (2002)CrossRef

18.

Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation, LNCS, vol. 78. Springer, Berlin (1979)CrossRef

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.: Normal form transformations. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, pp. 273–333. Elsevier, Amsterdam (2001)CrossRef

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)

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.

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)CrossRef

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)

29.

Stump, A.: Proof checking technology for satisfiability modulo theories. Electron. Notes Theor. Comput. Sci. 228, 121–133 (2009)CrossRef

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)

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)

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)

33.

Barendregt, H., Wiedijk, F.: The challenge of computer mathematics. Philos. Trans. R. Soc. Lond. Ser. A 363(1835), 2351–2375 (2005)MathSciNetCrossRef

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)

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)

36.

Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Log. 8(1), 1 (2007)MathSciNetCrossRef

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)

38.

Paulson, L.C.: A higher-order implementation of rewriting. Sci. Comput. Program. 3(2), 119–149 (1983)MathSciNetCrossRef

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)

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)

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)CrossRef

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)

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)

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)MathSciNetCrossRef

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.: 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)

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.: Proof checking and logic programming. In: Falaschi, M. (ed.) LOPSTR 2015, LNCS, vol. 9527, pp. 3–17. Springer, Berlin (2015)

Title: Scalable Fine-Grained Proofs for Formula Processing
Authors: Haniel Barbosa
Jasmin Christian Blanchette
Mathias Fleury
Pascal Fontaine
Publication date: 04-01-2019
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 3/2020
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-018-09502-y

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 3/2020

Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof

A Verified Implementation of Algebraic Numbers in Isabelle/HOL

Strong Extension-Free Proof Systems

A Resolution-Based Theorem Prover for : Architecture, Refinements, Strategies and Experiments

Efficient Verified (UN)SAT Certificate Checking

Preface: Selected Extended Papers of CADE 2017

Premium Partner