Extending Sledgehammer with SMT Solvers

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)

Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Applied Logic, vol. 27. Springer (2002)

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)

Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard—Version 2.0. In: Gupta, A., Kroening, D. (eds.) Satisfiability Modulo Theories (SMT) (2010)

Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification (CAV 2007), LNCS, vol. 4590, pp. 298–302. Springer (2007)

Barsotti, D., Nieto, L.P., Tiu, A.: Verification of clock synchronization algorithms: experiments on a combination of deductive tools. Form. Asp. Comput. 19(3), 321–341 (2007)

Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13(2), 261–293 (2003)

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)

Bezem, M., Hendriks, D., de Nivelle, H.: Automatic proof construction in type using resolution. J. Autom. Reasoning 29(3–4), 253–275 (2002)

Blanchette, J.C.: Automatic Proofs and Refutations for Higher-Order Logic. Ph.D. thesis, Dept. of Informatics, T.U. München (2012)

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)

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)

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)

Böhme, S.: Proving Theorems of Higher-Order Logic with SMT Solvers. Ph.D. thesis, Dept. of Informatics, T.U. München (2012)

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)

Böhme, S., Moskal, M., Schulte, W., Wolff, B.: HOL-Boogie—an interactive prover-backend for the verifying C compiler. J. Autom. Reasoning 44(1–2), 111–144 (2010)

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)

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)

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)

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)

Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Form. Asp. Comput. 20, 379–405 (2008)

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)

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)

Dutertre, B., de Moura, L.: The Yices SMT solver. Available http://yices.csl.sri.com/tool-paper.pdf (2006). Accessed 21 Feb 2013

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)

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)

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)

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

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)

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)

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)

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)

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)

Klein, G., Nipkow, T., Paulson, L. (eds.): The Archive of Formal Proofs. http://afp.sf.net/ . Accessed 21 Feb 2013

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)

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)

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)

Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning 40(1), 35–60 (2008)

Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic 7(1), 41–57 (2009)

Moskal, M.: Programming with triggers. In: Dutertre, B., Strichman, O. (eds.) Satisfiability Modulo Theories (SMT 2009) (2009)

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)

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

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

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

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)

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)

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

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)

Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Commun. 15(2–3), 91–110 (2002)

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)

Rudnicki, P., Urban, J.: Escape to ATP for Mizar. In: Fontaine, P., Stump, A. (eds.) Proof Exchange for Theorem Proving (PxTP-2011) (2011)

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)

Schropp, A.: Instantiating Deeply Embedded Many-sorted Theories into HOL Types in Isabelle. M.Sc. thesis, Dept. of Informatics, T.U. München (2012)

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)

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)

Sutcliffe, G.: System description: SystemOnTPTP. In: McAllester, D. (ed.) Conference on Automated Deduction (CADE-17), LNAI, vol. 1831, pp. 406–410. Springer (2000)

Sutcliffe, G.: The TPTP problem library and associated infrastructure—the FOF and CNF parts, v3.5.0. J. Autom. Reasoning 43(4), 337–362 (2009)

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

Weber, T.: SMT solvers: new oracles for the HOL theorem prover. J. Softw. Tools Technol. Transfer 13(5), 419–429 (2011)

Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1965–2013. Elsevier (2001)

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)

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)