×

zbMATH — the first resource for mathematics

Extending Sledgehammer with SMT solvers. (English) Zbl 1314.68272
Summary: Sledgehammer is a component of Isabelle/HOL that employs resolution-based first-order automatic theorem provers (ATPs) to discharge goals arising in interactive proofs. It heuristically selects relevant facts and, if an ATP is successful, produces a snippet that replays the proof in Isabelle. We extended Sledgehammer to invoke satisfiability modulo theories (SMT) solvers as well, exploiting its relevance filter and parallel architecture. The ATPs and SMT solvers nicely complement each other, and Isabelle users are now pleasantly surprised by SMT proofs for problems beyond the ATPs’ reach.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI Link
References:
[1] Ahrendt, W., Beckert, B., Hähnle, R., Menzel, W., Reif, W., Schellhorn, G., Schmitt, P.H.: Integrating automated and interactive theorem proving. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction—A Basis for Applications, Systems and Implementation Techniques, vol. II, pp. 97-116. Kluwer (1998) · Zbl 0970.68151
[2] Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Applied Logic, vol. 27. Springer (2002) · Zbl 1002.03002
[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.) Certified Programs and Proofs (CPP 2011), LNCS, vol. 7086, pp. 135-150. Springer (2011) · Zbl 1350.68223
[4] Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard—Version 2.0. In: Gupta, A., Kroening, D. (eds.) Satisfiability Modulo Theories (SMT) (2010)
[5] Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification (CAV 2007), LNCS, vol. 4590, pp. 298-302. Springer (2007) · Zbl 1185.68211
[6] Barsotti, D; Nieto, LP; Tiu, A, Verification of clock synchronization algorithms: experiments on a combination of deductive tools, Form. Asp. Comput., 19, 321-341, (2007) · Zbl 1125.68107
[7] Barthe, G; Capretta, V; Pons, O, Setoids in type theory, J. Funct. Program., 13, 261-293, (2003) · Zbl 1060.03030
[8] Besson, F., Fontaine, P., Théry, L.: A flexible proof format for SMT: a proposal. In: Fontaine, P., Stump, A. (eds.) Proof Exchange for Theorem Proving (PxTP-2011), pp. 15-26 (2011) · Zbl 1272.68362
[9] Bezem, M; Hendriks, D; Nivelle, H, Automatic proof construction in type using resolution, J. Autom. Reasoning, 29, 253-275, (2002) · Zbl 1015.03018
[10] Blanchette, J.C.: Automatic Proofs and Refutations for Higher-Order Logic. Ph.D. thesis, Dept. of Informatics, T.U. München (2012)
[11] Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) Conference on Automated Deduction (CADE-23), LNAI, vol. 6803, pp. 207-221. Springer (2011) · Zbl 1314.68271
[12] Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), LNCS, vol. 7795. Springer (2013) · Zbl 1381.68259
[13] Blanchette, J.C., Popescu, A., Wand, D., Weidenbach, C.: More SPASS with Isabelle—Superposition with hard sorts and configurable simplification. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving (ITP 2012), no. 7406 in LNCS, pp. 345-360. Springer (2012) · Zbl 1360.68742
[14] Böhme, S.: Proving Theorems of Higher-Order Logic with SMT Solvers. Ph.D. thesis, Dept. of Informatics, T.U. München (2012) · Zbl 1246.83140
[15] 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.P., Shao, Z. (eds.) Certified Programs and Proofs (CPP 2011), LNCS, vol. 7086, pp. 183-198. Springer (2011) · Zbl 1350.68225
[16] Böhme, S; Moskal, M; Schulte, W; Wolff, B, HOL-boogie—an interactive prover-backend for the verifying C compiler, J. Autom. Reasoning, 44, 111-144, (2010) · Zbl 1185.68211
[17] Böhme, S., Nipkow, T.: Sledgehammer: judgement day. In: Giesl, J., Hähnle, R. (eds.) International Joint Conference on Automated Reasoning (IJCAR 2010), LNAI, vol. 6173, pp. 107-121. Springer (2010) · Zbl 1291.68327
[18] Böhme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L. (eds.) Interactive Theorem Proving (ITP 2010), LNCS, vol. 6172, pp. 179-194. Springer (2010) · Zbl 1291.68328
[19] Böhme, S., Weber, T.: Designing proof formats: a user’s perspective. In: Fontaine, P., Stump, A. (eds.) Proof Exchange for Theorem Proving (PxTP-2011), pp. 27-32 (2011) · Zbl 1060.03030
[20] Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.C.: Using first-order theorem provers in the Jahob data structure verification system. In: Cook, B., Podelski, A. (eds.) Verification, Model Checking, and Abstract Interpretation (VMCAI 2007), LNCS, vol. 4349, pp. 74-88. Springer (2007) · Zbl 1132.68348
[21] Bradley, AR; Manna, Z, Property-directed incremental invariant generation, Form. Asp. Comput., 20, 379-405, (2008) · Zbl 1149.68402
[22] Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2009), LNCS, vol. 5674, pp. 23-42. Springer (2009)
[23] Dahn, B., Gehne, J., Honigmann, T., Wolf, A.: Integration of automated and interactive theorem proving in ILF. In: McCune, W. (ed.) Conference on Automated Deduction (CADE-14), LNCS, vol. 1249, pp. 57-60. Springer (1997) · Zbl 1125.68107
[24] Dutertre, B., de Moura, L.: The Yices SMT solver. Available http://yices.csl.sri.com/tool-paper.pdf (2006). Accessed 21 Feb 2013
[25] Erkök, L., Matthews, J.: Using Yices as an automated solver in Isabelle/HOL. In: Rushby, J., Shankar, N. (eds.) Automated Formal Methods (AFM08), pp. 3-13 (2008)
[26] 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.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2006), LNCS, vol. 3920, pp. 167-181. Springer (2006) · Zbl 1180.68240
[27] Foster, S., Struth, G.: Integrating an automated theorem prover into Agda. In: Bobaru, M.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods (NFM 2011), LNCS, vol. 6617, pp. 116-130 (2011)
[28] Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation, LNCS, vol. 78. Springer (1979) · Zbl 0421.68039
[29] Guttmann, W., Struth, G., Weber, T.: Automating algebraic methods in Isabelle. In: Qin, S., Qiu, Z. (eds.) International Conference on Formal Engineering Methods (ICFEM 2011), LNCS, vol. 6991, pp. 617-632. Springer (2011)
[30] Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) Conference on Automated Deduction (CADE-23), LNAI, vol. 6803, pp. 299-314. Springer (2011) · Zbl 1341.68189
[31] Hughes, R.J.M.: Super-combinators: A new implementation method for applicative languages. In: LISP and Functional Programming (LFP 1982), pp. 1-10. ACM Press (1982)
[32] Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) Theorem Proving in Higher Order Logics (TPHOLs ’99), LNCS, vol. 1690, pp. 311-321 (1999)
[33] Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: Archer, M., Di Vito, B., Muñoz, C. (eds.) Design and Application of Strategies/Tactics in Higher Order Logics, no. CP-2003-212448 in NASA Technical Reports, pp. 56-68 (2003)
[34] Klein, G., Nipkow, T., Paulson, L. (eds.): The Archive of Formal Proofs. http://afp.sf.net/. Accessed 21 Feb 2013
[35] McCune, W., Shumsky, O.: System description: IVY. In: McAllester, D. (ed.) Conference on Automated Deduction (CADE-17), LNAI, vol. 1831, pp. 401-405. Springer (2000) · Zbl 0963.68527
[36] McLaughlin, S; Barrett, C; Ge, Y, Cooperating theorem provers: a case study combining HOL-light and CVC lite, Electr. Notes Theor. Comput. Sci., 144, 43-51, (2006) · Zbl 1272.68362
[37] Meier, A.: Tramp: Transformation of machine-found proofs into natural deduction proofs at the assertion level (system description). In: McAllester, D. (ed.) Conference on Automated Deduction (CADE-17), LNAI, vol. 1831, pp. 460-464. Springer (2000) · Zbl 0963.68537
[38] Meng, J; Paulson, LC, Translating higher-order clauses to first-order clauses, J. Autom. Reasoning, 40, 35-60, (2008) · Zbl 1203.68188
[39] Meng, J; Paulson, LC, Lightweight relevance filtering for machine-generated resolution problems, Journal of Applied Logic, 7, 41-57, (2009) · Zbl 1183.68560
[40] Moskal, M.: Programming with triggers. In: Dutertre, B., Strichman, O. (eds.) Satisfiability Modulo Theories (SMT 2009) (2009)
[41] de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), LNCS, vol. 4963, pp. 337-340. Springer (2008)
[42] Nipkow, T.: Re: [isabelle] A beginner’s questionu [sic]. Archived https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-November/msg00097.html (2010). Accessed 21 Feb 2013
[43] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002) · Zbl 0994.68131
[44] Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 335-367. Elsevier (2001) · Zbl 0992.03018
[45] Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S., (eds.) International Workshop on the Implementation of Logics (IWIL-2010) (2010)
[46] Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2007), LNCS, vol. 4732, pp. 232-245 (2007) · Zbl 1144.68364
[47] Ranise, S., Tinelli, C.: The SMT-LIB standard: Version 1.2. http://smtlib.cs.uiowa.edu/papers/format-v1.2-r06.08.30.pdf (2006). Accessed 21 Feb 2013
[48] Reif, W., Schellhorn, G.: Theorem proving in large theories. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction—A Basis for Applications, vol. III: Applications, pp. 225-241. Kluwer (1998) · Zbl 0972.68520
[49] Riazanov, A; Voronkov, A, The design and implementation of vampire, AI Commun., 15, 91-110, (2002) · Zbl 1021.68082
[50] Rinard, M.C.: Integrated reasoning and proof choice point selection in the Jahob system—mechanisms for program survival. In: Schmidt, R.A. (ed.) Conference on Automated Deduction (CADE-22), LNCS, vol. 5663, pp. 1-16. Springer (2009)
[51] Rudnicki, P., Urban, J.: Escape to ATP for Mizar. In: Fontaine, P., Stump, A. (eds.) Proof Exchange for Theorem Proving (PxTP-2011) (2011)
[52] Rushby, J.M.: Tutorial: automated formal methods with PVS, SAL, and Yices. In: Hung, D.V., Pandya, P. (eds.) Software Engineering and Formal Methods (SEFM 2006), p. 262. IEEE (2006)
[53] Schropp, A.: Instantiating Deeply Embedded Many-sorted Theories into HOL Types in Isabelle. M.Sc. thesis, Dept. of Informatics, T.U. München (2012)
[54] Schulz, S.: System description: E 0.81. In: Basin, D., Rusinowitch, M. (eds.) International Joint Conference on Automated Reasoning (IJCAR 2004), LNAI, vol. 3097, pp. 223-228. Springer (2004) · Zbl 1126.68578
[55] Siekmann, J., Benzmüller, C., Fiedler, A., Meier, A., Normann, I., Pollet, M.: Proof development with \(Ω\)mega: the irrationality of \(\sqrt2\). In: Kamareddine, F. (ed.) Thirty Five Years of Automating Mathematics, Applied Logic, vol. 28, pp. 271-314. Springer (2003) · Zbl 1063.68093
[56] Sutcliffe, G.: System description: SystemOnTPTP. In: McAllester, D. (ed.) Conference on Automated Deduction (CADE-17), LNAI, vol. 1831, pp. 406-410. Springer (2000) · Zbl 0963.68529
[57] Sutcliffe, G, The TPTP problem library and associated infrastructure—the FOF and CNF parts, v3.5.0, J. Autom. Reasoning, 43, 337-362, (2009) · Zbl 1185.68636
[58] Wampler-Doty, M.: A complete proof of the Robbins conjecture. In: G. Klein, T. Nipkow, L. Paulson (eds.) The Archive of Formal Proofs. Available http://afp.sf.net/entries/Robbins-Conjecture.shtml (2010). Accessed 21 Feb 2013
[59] Weber, T, SMT solvers: new oracles for the HOL theorem prover, J. Softw. Tools Technol. Transfer, 13, 419-429, (2011)
[60] Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1965-2013. Elsevier (2001) · Zbl 1011.68129
[61] Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A. (eds.) Theorem Proving in Higher Order Logics (TPHOLs ’97), LNCS, vol. 1275, pp. 307-322 (1997) · Zbl 1060.03030
[62] Wenzel, M.: Parallel proof checking in Isabelle/Isar. In: Dos Reis, G., Théry, L. (eds.) Programming Languages for Mechanized Mathematics Systems (PLMMS 2009). ACM Digital Library (2009) · Zbl 1125.68107
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.