zbMATH — the first resource for mathematics

The strategy challenge in SMT solving. (English) Zbl 1383.68084
Bonacina, Maria Paola (ed.) et al., Automated reasoning and mathematics. Essays in memory of William W. McCune. Berlin: Springer (ISBN 978-3-642-36674-1/pbk). Lecture Notes in Computer Science 7788. Lecture Notes in Artificial Intelligence, 15-44 (2013).
Summary: High-performance SMT solvers contain many tightly integrated, hand-crafted heuristic combinations of algorithmic proof methods. While these heuristic combinations tend to be highly tuned for known classes of problems, they may easily perform badly on classes of problems not anticipated by solver developers. This issue is becoming increasingly pressing as SMT solvers begin to gain the attention of practitioners in diverse areas of science and engineering. We present a challenge to the SMT community: to develop methods through which users can exert strategic control over core heuristic aspects of SMT solvers. We present evidence that the adaptation of ideas of strategy prevalent both within the Argonne and LCF theorem proving paradigms can go a long way towards realizing this goal.
For the entire collection see [Zbl 1259.68002].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI Link
[1] Dolzmann, T.S.A.: Redlog User Manual - Edition 2.0. MIP-9905 (1999)
[2] Ackermann, W.: Solvable cases of the decision problem. Studies in Logic and the Foundation of Mathematics (1954) · Zbl 0056.24505
[3] Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The Matita Interactive Theorem Prover. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 64–69. Springer, Heidelberg (2011) · Zbl 1341.68179
[4] Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2010), http://www.SMT-LIB.org
[5] Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007) · Zbl 05216239
[6] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004) · Zbl 1069.68095
[7] Bonacina, M.P.: A Taxonomy of Theorem-Proving Strategies. In: Veloso, M.M., Wooldridge, M.J. (eds.) Artificial Intelligence Today. LNCS (LNAI), vol. 1600, pp. 43–84. Springer, Heidelberg (1999) · Zbl 0984.03011
[8] Bonacina, M.P., Hsiang, J.: On the modeling of search in theorem proving–towards a theory of strategy analysis. Inf. Comput. 147(2), 171–208 (1998) · Zbl 0927.68081
[9] Bonacina, M.P., McCune, W.W.: Distributed Theorem Proving by Peers. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 841–845. Springer, Heidelberg (1994)
[10] Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P., Schulz, S., Sebastiani, R.: MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. J. Autom. Reason. 35(1-3), 265–293 (2005) · Zbl 1109.68101
[11] Brown, C.W.: QEPCAD-B: A System for Computing with Semi-algebraic Sets via Cylindrical Algebraic Decomposition. SIGSAM Bull. 38, 23–24 (2004)
[12] Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Santuari, A., Sebastiani, R.: To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in \(\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})\) . In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 557–571. Springer, Heidelberg (2006) · Zbl 1165.68482
[13] Davis, M.: Eliminating the Irrelevant from Mechanical Proofs. In: Proc. Symp. Applied Math., vol. XV, pp. 15–30 (1963) · Zbl 0131.01201
[14] Davis, M.: The early history of automated deduction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 3–15. Elsevier and MIT Press (2001) · Zbl 1011.68511
[15] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5, 394–397 (1962) · Zbl 0217.54002
[16] Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201–215 (1960) · Zbl 0212.34203
[17] de Moura, L., Bjørner, N.: Relevancy propagation. Technical Report MSR-TR-2007-140, Microsoft Research (2007)
[18] de Moura, L., 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) · Zbl 05262379
[19] de Moura, L.M., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)
[20] Dolzmann, A., Seidl, A., Sturm, T.: Efficient Projection Orders for CAD. In: ISSAC 2004: Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation, pp. 111–118. ACM (2004) · Zbl 1134.68575
[21] Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006) · Zbl 05187406
[22] Gilmore, P.C.: A Proof Method for Quantification Theory: its Justification and Realization. IBM J. Res. Dev. 4, 28–35 (1960) · Zbl 0097.00301
[23] Gordon, M.: From LCF to HOL: a short history, pp. 169–185. MIT Press, Cambridge (2000)
[24] Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem-proving environment for higher-order logic. Cambridge University Press (1993) · Zbl 0779.68007
[25] Hickey, J.J.: The MetaPRL Logical Programming Environment. PhD thesis, Cornell University, Ithaca, NY (January 2001)
[26] Jovanović, D., de Moura, L.: Cutting to the Chase Solving Linear Integer Arithmetic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 338–353. Springer, Heidelberg (2011) · Zbl 1314.90054
[27] Kirchner, F., Muñoz, C.: The proof monad. Journal of Logic and Algebraic Programming 79(3-5), 264–277 (2010) · Zbl 1208.68144
[28] Kowalski, R.: Search Strategies for Theorem Proving. Machine Intelligence 5, 181–201 (1969) · Zbl 0218.68018
[29] Lusk, E.L.: Controlling Redundancy in Large Search Spaces: Argonne-Style Theorem Proving Through the Years. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 96–106. Springer, Heidelberg (1992)
[30] Luttik, B., Visser, E.: Specification of rewriting strategies. In: Sellink, M.P.A. (ed.) 2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF 1997), Electronic Workshops in Computing. Springer, Berlin (1997)
[31] McCune, W.: Solution of the Robbins Problem. J. Autom. Reason. 19(3), 263–276 (1997) · Zbl 0883.06011
[32] McCune, W.: Prover9 and Mace4 (2005-2010), http://www.cs.unm.edu/mccune/prover9/
[33] Milner, R.: Logic for computable functions: description of a machine implementation. Technical Report STAN-CS-72-288, Stanford University (1972)
[34] Newell, A., Shaw, J.C., Simon, H.A.: Elements of a Theory of Human Problem Solving. Psychological Review 65, 151–166 (1958)
[35] Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006) · Zbl 1326.68164
[36] Passmore, G.O.: Combined Decision Procedures for Nonlinear Arithmetics, Real and Complex. PhD thesis, University of Edinburgh (2011)
[37] Passmore, G.O., Jackson, P.B.: Combined Decision Techniques for the Existential Theory of the Reals. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) Calculemus/MKM 2009. LNCS (LNAI), vol. 5625, pp. 122–137. Springer, Heidelberg (2009) · Zbl 1247.03018
[38] Passmore, G.O., Jackson, P.B.: Abstract Partial Cylindrical Algebraic Decomposition I: The Lifting Phase. In: Cooper, S.B., Dawar, A., Löwe, B. (eds.) CiE 2012. LNCS, vol. 7318, pp. 560–570. Springer, Heidelberg (2012) · Zbl 1357.68199
[39] Paulson, L.: Logic and Computation: Interactive Proof with Cambdrige LCF, vol. 2. Cambridge University Press (1987) · Zbl 0645.68041
[40] Paulson, L.: Isabelle: The next 700 theorem provers. In: Logic and Computer Science, pp. 361–386. Academic Press (1990)
[41] Plaisted, D.A.: The Search Efficiency of Theorem Proving Strategies. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 57–71. Springer, Heidelberg (1994)
[42] Prawitz, D.: An Improved Proof Procedure. Theoria 26(2), 102–139 (1960) · Zbl 0099.00801
[43] Robinson, A.: Short Lecture. Summer Institute for Symbolic Logic, Cornell University (1957)
[44] Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12, 23–41 (1965) · Zbl 0139.12303
[45] Wang, H.: Toward mechanical mathematics. IBM J. Res. Dev. 4, 2–22 (1960) · Zbl 0097.00404
[46] Weispfenning, V.: Quantifier Elimination for Real Algebra - the Quadratic Case and Beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85–101 (1997) · Zbl 0867.03003
[47] Wos, L., Carson, D., Robinson, G.: The unit preference strategy in theorem proving. In: Proceedings of the Fall Joint Computer Conference, AFIPS 1964, Part I, October 27-29, pp. 615–621. ACM, New York (1964) · Zbl 0135.18306
[48] Wos, L., Robinson, G.A., Carson, D.F.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12, 536–541 (1965) · Zbl 0135.18401
[49] Zankl, H., Middeldorp, A.: Satisfiability of Non-linear (Ir)rational Arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS (LNAI), vol. 6355, pp. 481–500. Springer, Heidelberg (2010) · Zbl 1310.68126
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.