Document Zbl 1314.68271

Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.

Extending Sledgehammer with SMT solvers. (English) Zbl 1314.68271

Bjørner, Nikolaj (ed.) et al., Automated deduction – CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 – August 5, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22437-9/pbk; 978-3-642-22438-6/ebook). Lecture Notes in Computer Science 6803. Lecture Notes in Artificial Intelligence, 116-130 (2011).

Summary: Sledgehammer is a component of Isabelle/HOL that employs 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. Isabelle users are now pleasantly surprised by SMT proofs for problems beyond the ATPs’ reach. Remarkably, the best SMT solver performs better than the best ATP on most of our benchmarks.
For the entire collection see [Zbl 1218.68006].

Cited in 28 Documents

MSC:

68T15

Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Robbins Conjecture; CVC Lite; Sledgehammer; SystemOnTPTP; VCC; Gandalf; HOL Light; Satallax; HOL-Boogie; z3; Coq; Isabelle/HOL; SMT-LIB; VAMPIRE; LEO-II; Yices; ETPS; MPTP 0.2; Metis_; cvc3; Archive Formal Proofs

Cite Review PDF

Full Text: DOI

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, Dordrecht (1998) · Zbl 0970.68151 · doi:10.1007/978-94-017-0435-9_4
[2]	Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Applied Logic, vol. 27. Springer, Heidelberg (2002) · Zbl 1002.03002 · doi:10.1007/978-94-015-9934-4
[3]	Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 76–90. Springer, Heidelberg (2010) · Zbl 1291.03015 · doi:10.1007/978-3-642-14203-1_7
[4]	Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007) · doi:10.1007/978-3-540-73368-3_34
[5]	Barsotti, D., Nieto, L.P., Tiu, A.: Verification of clock synchronization algorithms: Experiments on a combination of deductive tools. Formal Asp. Comput. 19(3), 321–341 (2007) · Zbl 1125.68107 · doi:10.1007/s00165-007-0027-6
[6]	Benzmüller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II–a cooperative automatic theorem prover for higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162–170. Springer, Heidelberg (2008) · Zbl 1165.68446 · doi:10.1007/978-3-540-71070-7_14
[7]	Bezem, M., Hendriks, D., de Nivelle, H.: Automatic proof construction in type theory using resolution. J. Auto. Reas. 29(3-4), 253–275 (2002) · Zbl 1015.03018 · doi:10.1023/A:1021939521172
[8]	Böhme, S., Moskal, M., Schulte, W., Wolff, B.: HOL-Boogie–an interactive prover-backend for the Verifying C Compiler. J. Auto. Reas. 44(1-2), 111–144 (2010) · Zbl 1185.68211 · doi:10.1007/s10817-009-9142-9
[9]	Böhme, S., Nipkow, T.: Sledgehammer: Judgement Day. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 107–121. Springer, Heidelberg (2010) · Zbl 1291.68327 · doi:10.1007/978-3-642-14203-1_9
[10]	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) · Zbl 1291.68328 · doi:10.1007/978-3-642-14052-5_14
[11]	Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Asp. Comput. 20, 379–405 (2008) · Zbl 1149.68402 · doi:10.1007/s00165-008-0080-9
[12]	Claessen, K.: Equinox, a new theorem prover for full first-order logic with equality. Presentation at Dagstuhl Seminar on Deduction and Applications (2005)
[13]	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.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009) · doi:10.1007/978-3-642-03359-9_2
[14]	Couchot, J.-F., Lescuyer, S.: Handling polymorphism in automated deduction. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 263–278. Springer, Heidelberg (2007) · Zbl 1213.68568 · doi:10.1007/978-3-540-73595-3_18
[15]	de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008) · doi:10.1007/978-3-540-78800-3_24
[16]	Dutertre, B., de Moura, L.: The Yices SMT solver (2006), http://yices.csl.sri.com/tool-paper.pdf
[17]	Erkök, L., Matthews, J.: Using Yices as an automated solver in Isabelle/HOL. In: Rushby, J., Shankar, N. (eds.) Automated Formal Methods, pp. 3–13 (2008)
[18]	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. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 167–181. Springer, Heidelberg (2006) · Zbl 1180.68240 · doi:10.1007/11691372_11
[19]	Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: These proceedings (2011) · Zbl 1341.68189 · doi:10.1007/978-3-642-22438-6_23
[20]	Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 311–321. Springer, Heidelberg (1999) · doi:10.1007/3-540-48256-3_21
[21]	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, number CP-2003-212448 in NASA Technical Reports, pp. 56–68 (2003)
[22]	Keller, C.: Cooperation between SAT, SMT provers and Coq. Presentation at the Synthesis. Verification and Analysis of Rich Models workshop (2011)
[23]	Klein, G., Nipkow, T., Paulson, L. (eds.): The Archive of Formal Proofs, http://afp.sf.net/
[24]	Korovin, K.: Instantiation-based automated reasoning: From theory to practice. In: Schmidt, R.A. (ed.) CADE-22. LNCS (LNAI), vol. 5663, pp. 163–166. Springer, Heidelberg (2009) · doi:10.1007/978-3-642-02959-2_14
[25]	Leino, K.R.M., Rümmer, P.: A polymorphic intermediate verification language: Design and logical encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 312–327. Springer, Heidelberg (2010) · Zbl 1284.68409 · doi:10.1007/978-3-642-12002-2_26
[26]	McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-Light and CVC Lite. Electr. Notes Theor. Comput. Sci. 144(2), 43–51 (2006) · Zbl 1272.68362 · doi:10.1016/j.entcs.2005.12.005
[27]	Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Auto. Reas. 40(1), 35–60 (2008) · Zbl 1203.68188 · doi:10.1007/s10817-007-9085-y
[28]	Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Applied Logic 7(1), 41–57 (2009) · Zbl 1183.68560 · doi:10.1016/j.jal.2007.07.004
[29]	Moskal, M.: Programming with triggers. In: Dutertre, B., Strichman, O. (eds.) Satisfiability Modulo Theories (2009) · doi:10.1145/1670412.1670416
[30]	Nipkow, T.: Re: [isabelle] A beginner’s questionu [sic], (November 26, 2010), https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-November/msg00097.html
[31]	Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131
[32]	Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 335–367. Elsevier, Amsterdam (2001) · Zbl 0992.03018 · doi:10.1016/B978-044450813-3/50008-4
[33]	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 (2010)
[34]	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, Heidelberg (2007) · Zbl 1144.68364 · doi:10.1007/978-3-540-74591-4_18
[35]	Ranise, S., Tinelli, C.: The SMT-LIB standard: Version 1.2 (2006), http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30.pdf
[36]	Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Comm. 15(2-3), 91–110 (2002) · Zbl 1021.68082
[37]	Rushby, J.M.: Tutorial: Automated formal methods with PVS, SAL, and Yices. In: Hung, D.V., Pandya, P. (eds.) Software Engineering and Formal Methods, p. 262. IEEE, New York (2006)
[38]	Schulz, S.: System description: E 0.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 223–228. Springer, Heidelberg (2004) · Zbl 1126.68578 · doi:10.1007/978-3-540-25984-8_15
[39]	Siekmann, J., Benzmüller, C., Fiedler, A., Meier, A., Normann, I., Pollet, M.: Proof development with {\(\Omega\)}mega: The irrationality of \(\sqrt2\) . In: Kamareddine, F. (ed.) Thirty Five Years of Automating Mathematics. Applied Logic, vol. 28, pp. 271–314. Springer, Heidelberg (2003) · Zbl 1063.68093 · doi:10.1007/978-94-017-0253-9_11
[40]	Sutcliffe, G.: System description: SystemOnTPTP. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 406–410. Springer, Heidelberg (2000) · Zbl 0963.68529 · doi:10.1007/10721959_31
[41]	Sutcliffe, G., Chang, C., Ding, L., McGuinness, D., da Silva, P.P.: Different proofs are good proofs. In: McGuinness, D., Stump, A., Sutcliffe, G., Tinelli, C. (eds.) Workshop on Evaluation Methods for Solvers, and Quality Metrics for Solutions, pp. 1–10 (2010)
[42]	Urban, J.: MPTP 0.2: Design, implementation, and initial experiments. J. Auto. Reas. 37(1-2), 21–43 (2006) · Zbl 1113.68095 · doi:10.1007/s10817-006-9032-3
[43]	Wampler-Doty, M.: A complete proof of the Robbins conjecture. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs (2010), http://afp.sf.net/entries/Robbins-Conjecture.shtml
[44]	Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1965–2013. Elsevier, Amsterdam (2001) · Zbl 1011.68129 · doi:10.1016/B978-044450813-3/50029-1
[45]	Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 307–322. Springer, Heidelberg (1997) · doi:10.1007/BFb0028402
[46]	Wenzel, M.: Parallel proof checking in Isabelle/Isar. In: Dos Reis, G., Théry, L. (eds.) Programming Languages for Mechanized Mathematics Systems, ACM Digital Library (2009)

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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.