×

A heuristic prover for real inequalities. (English) Zbl 1356.68174

Summary: We describe a general method for verifying inequalities between real-valued expressions, especially the kinds of straightforward inferences that arise in interactive theorem proving. In contrast to approaches that aim to be complete with respect to a particular language or class of formulas, our method establishes claims that require heterogeneous forms of reasoning, relying on a Nelson-Oppen-style architecture in which special-purpose modules collaborate and share information. The framework is thus modular and extensible. A prototype implementation shows that the method works well on a variety of examples, and complements techniques that are used by contemporary interactive provers.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
26D07 Inequalities involving other types of functions
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Akbarpour, B.; Paulson, L.; Autexier, S. (ed.); etal., MetiTarski: an automatic prover for the elementary functions, 217-231 (2008), Berlin · Zbl 1166.68335
[2] Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Trans. Comput. Logic 9(1), 2 (2007) · Zbl 1367.68244 · doi:10.1145/1297658.1297660
[3] Avigad, J., Friedman, H.: Combining decision procedures for the reals. Log. Methods Comput. Sci. 2(4), 4:4, 42 (2006) · Zbl 1127.03006 · doi:10.2168/LMCS-2(4:4)2006
[4] Avigad, J., Hölzl, J., Serafin, L.: A formally verified proof of the Central Limit Theorem. (In preparation) · Zbl 1425.68369
[5] Avigad, J.; Lewis, RY; Roux, C.; Klein, Gerwin (ed.); Gamboa, Ruben (ed.), A heuristic prover for real inequalities, 61-76 (2014), Heidelberg · Zbl 1416.68149
[6] Avis, D.: Living with lrs. In: Akiyama, J., Kano, M., Urabe, M. (eds.) Discrete and Computational Geometry (Tokyo, 1998), pp. 47-56. Springer, Berlin (2000) · Zbl 0971.68613
[7] Barrett, C.; Sebastiani, R.; Seshia, SA; Tinelli, C.; Biere, A. (ed.); etal., Satisability modulo theories, 825-885 (2008), Amsterdam
[8] Basu, S., Pollack, R., Roy, M.: Algorithms in Real Algebraic Geometry. Springer, Berlin (2003) · Zbl 1031.14028 · doi:10.1007/978-3-662-05355-3
[9] Billingsley, P.: Probability and Measure, 3rd edn. Wiley, New York (1995) · Zbl 0822.60002
[10] Blanchette, J., Böhme, S., Paulson, L.: Extending Sledgehammer with SMT solvers. Automated Deduction-CADE-23. Springer, Berlin (2011) · Zbl 1314.68271 · doi:10.1007/978-3-642-22438-6_11
[11] Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, Cambridge (2004) · Zbl 1058.90049 · doi:10.1017/CBO9780511804441
[12] Chaieb, A., Nipkow, T.: Proof synthesis and reflection for linear arithmetic. J. Autom. Reason. 41(1), 33-59 (2008) · Zbl 1171.03006 · doi:10.1007/s10817-008-9101-x
[13] Contejean, E.; Oostrom (ed.), A certified AC matching algorithm, 70-84 (2004), Berlin · Zbl 1187.68524 · doi:10.1007/978-3-540-25979-4_5
[14] de Moura, L., Bjørner, N.: Efficient E-Matching for SMT Solvers. CADE. Springer, Berlin (2007) · Zbl 1213.68578 · doi:10.1007/978-3-540-73595-3_13
[15] de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: TACAS, pp. 337-340. (2008) · Zbl 0452.68013
[16] Dutertre, B.; Moura, L.; Ball, T. (ed.); Jones, R. (ed.), A fast linear-arithmetic solver for DPLL(T), 81-94 (2006), Berlin
[17] Fukuda, K., Prodon, A.: Double Description Method Revisited. Combinatorics and Computer Science. Springer, Berlin (1996) · doi:10.1007/3-540-61576-8_77
[18] Garling, D.J.H.: Inequalities: A Journey into Linear Analysis. Cambridge University Press, Cambridge (2007) · Zbl 1135.26014 · doi:10.1017/CBO9780511755217
[19] Gao, S., Avigad, J., Clarke, E.M.: Delta-complete decision procedures for satisfiability over the reals. In: Gramlich, B. et al. (eds.) IJCAR, pp. 286-300. Springer, Heidelberg (2012) · Zbl 1358.03028
[20] Hardy, G .H., Littlewood, J .E., Pólya, G.: Inequalities. Cambridge University Press, Cambridge (1988). (Reprint of the 1952 edition) · Zbl 0634.26008
[21] Harrison, J.; Srivas, M. (ed.); Camilleri, A. (ed.), HOL light: a tutorial introduction, 265-269 (1996), Berlin
[22] Harrison, J.; Schneider, K. (ed.); Brandt, J. (ed.), Verifying nonlinear real formulas via sums of squares, 102-118 (2007), Berlin · Zbl 1144.68357
[23] Hunt, W. A.; Krug, R. B.; Moore, J.; Geist, D. (ed.); Tronci, E. (ed.), Linear and nonlinear arithmetic in ACL2, 319-333 (2003), Berlin · Zbl 1179.68136 · doi:10.1007/978-3-540-39724-3_29
[24] Jones, C.N., Kerrigan, E.C., Maciejowski, J.M.: Equality set projection: a new algorithm for the projection of polytopes in halfspace representation. Technical report, Department of Engineering, University of Cambridge (2004)
[25] Kaufmann, M., Manolios, P., Strother Moore, J.: Computer-Aided Reasoning: An Approach. Kluwer, Berlin (2000)
[26] Lewis, R.Y.: Polya: a heuristic procedure for reasoning with real inequalities. M.S. Thesis, Department of Philosophy, Carnegie Mellon University (2014)
[27] McLaughlin, S.; Harrison, J.; Nieuwenhuis, R. (ed.), A proof producing decision procedure for real arithmetic, 295-314 (2005), Berlin · Zbl 1135.03329 · doi:10.1007/11532231_22
[28] Meng, J., Paulson, L.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log. 7(1), 41-57 (2009) · Zbl 1183.68560 · doi:10.1016/j.jal.2007.07.004
[29] Moore, R., Kearfott, R., Cloud, M.: Introduction to Interval Analysis. Society for Industrial and Applied Mathematics (SIAM), Philadelphia (2009) · Zbl 1168.65002 · doi:10.1137/1.9780898717716
[30] Moses, J.: Algebraic simplification: a guide for the perplexed. Commun. ACM 14, 527-537 (1971) · Zbl 0222.68017 · doi:10.1145/362637.362648
[31] Moskal, M., Łopusański, J., Kiniry, J.: E-matching for fun and profit. In: Proceedings of the 5th International Workshop on SMT (2008) · Zbl 1277.68142
[32] Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1, 245-257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079
[33] Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL. A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002) · Zbl 0994.68131
[34] Platzer, A.; KeYmaera, JQuesel; Armando (ed.); Baumgartner (ed.); Dowek (ed.), A Hybrid theorem prover for hybrid systems, 171-178 (2008), Heidelberg · Zbl 1165.68469
[35] Platzer, A.; Quesel, J.; Rummer, P.; Schmidt (ed.), Real world verification, 485-501 (2009), Heidelberg · Zbl 1250.68197
[36] Polya, G.: How to Solve It. Princeton University Press, Princeton, NJ (1945) · Zbl 0061.00616
[37] Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G. et al. (ed.). ESCoR: Empirically Successful Computerized Reasoning 2006. CEUR Workshop Proceedings, pp. 18-33 (2006)
[38] Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. Commun. ACM 8, 4-13 (1992)
[39] Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986) · Zbl 0665.90063
[40] Ziegler, G.: Lectures on Polytopes. Springer, Berlin (1995) · Zbl 0823.52002 · doi:10.1007/978-1-4613-8431-1
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.