Making higher-order superposition work. (English) Zbl 1512.68432
Summary: Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about Booleans, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 03B16 | Higher-order logic |
Software:
CVC4; Why3; OTTER; DISCOUNT; AVATAR; CoqHammer; TPTP; VAMPIRE; StarExec; HOLyHammer; Sledgehammer; E Theorem Prover; Coq; Satallax; WhyML; HOL; ZipperpositionReferences:
| [1] | Bachmair, L., Ganzinger, H.: Non-clausal resolution and superposition with selection and redundancy criteria. In: Voronkov, A. (ed.) LPAR ’92, LNCS, vol. 624, pp. 273-284. Springer (1992) · Zbl 0925.03063 |
| [2] | Backes, J.; Brown, CE, Analytic tableaux for higher-order logic with choice, J. Autom. Reason., 47, 4, 451-479 (2011) · Zbl 1258.03019 · doi:10.1007/s10817-011-9233-2 |
| [3] | Barbosa, H., Reynolds, A., El Ouraoui, D., Tinelli, C., Barrett, C.W.: Extending SMT solvers to higher-order logic. In: Fontaine, P. (ed.) CADE-27, LNCS, vol. 11716, pp. 35-54. Springer (2019) · Zbl 1535.68443 |
| [4] | Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011, LNCS, vol. 6806, pp. 171-177. Springer (2011) |
| [5] | Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P.: Superposition for full higher-order logic. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28, LNCS, vol. 12699, pp. 396-412. Springer (2021) · Zbl 1497.03030 |
| [6] | Bentkamp, A.; Blanchette, J.; Tourret, S.; Vukmirović, P.; Waldmann, U., Superposition with lambdas, J. Autom. Reason., 65, 7, 893-940 (2021) · Zbl 07433023 · doi:10.1007/s10817-021-09595-y |
| [7] | Bentkamp, A., Blanchette, J.C., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018, LNCS, vol. 10900, pp. 28-46. Springer (2018) · Zbl 1511.68302 |
| [8] | Benzmüller, C., Sorge, V., Jamnik, M., Kerber, M.: Can a higher-order and a first-order theorem prover cooperate? In: Baader, F., Voronkov, A. (eds.) LPAR 2004, LNCS, vol. 3452, pp. 415-431. Springer (2004) · Zbl 1108.68570 |
| [9] | Bhayat, A., Reger, G.: Restricted combinatory unification. In: Fontaine, P. (ed.) CADE-27, LNCS, vol. 11716, pp. 74-93. Springer (2019) · Zbl 1535.68445 |
| [10] | Bhayat, A., Reger, G.: A combinator-based superposition calculus for higher-order logic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020, Part I, LNCS, vol. 12166, pp. 278-296. Springer (2020) · Zbl 07614518 |
| [11] | Brown, CE, Reducing higher-order theorem proving to a sequence of SAT problems, J. Autom. Reason., 51, 1, 57-77 (2013) · Zbl 1314.68276 · doi:10.1007/s10817-013-9283-8 |
| [12] | Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. Ph.D. thesis, École polytechnique (2015) |
| [13] | Czajka, L.; Kaliszyk, C., Hammer for Coq: automation for dependent type theory, J. Autom. Reason., 61, 1-4, 423-453 (2018) · Zbl 1448.68458 · doi:10.1007/s10817-018-9458-4 |
| [14] | Denzinger, J.; Kronenburg, M.; Schulz, S., DISCOUNT—a distributed and learning equational prover, J. Autom. Reason., 18, 2, 189-198 (1997) · doi:10.1023/A:1005879229581 |
| [15] | Ebner, G., Blanchette, J., Tourret, S.: Unifying splitting. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28, LNCS, vol. 12699, pp. 344-360. Springer (2021) · Zbl 1540.68265 |
| [16] | Färber, M., Brown, C.E.: Internal guidance for Satallax. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706, pp. 349-361. Springer (2016) · Zbl 1475.68435 |
| [17] | Filliâtre, J., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013, LNCS, vol. 7792, pp. 125-128. Springer (2013) · Zbl 1435.68366 |
| [18] | Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. In: Baader, F. (ed.) CADE-19, LNCS, vol. 2741, pp. 335-349. Springer (2003) · Zbl 1278.68261 |
| [19] | Gleiss, B., Suda, M.: Layered clause selection for theory reasoning (short paper). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020, Part I, LNCS, vol. 12166, pp. 402-409. Springer (2020) · Zbl 07614525 |
| [20] | Henkin, L., Completeness in the theory of types, J. Symb. Log., 15, 2, 81-91 (1950) · Zbl 0039.00801 · doi:10.2307/2266967 |
| [21] | Hoder, K., Reger, G., Suda, M., Voronkov, A.: Selecting the selection. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706, pp. 313-329. Springer (2016) · Zbl 1475.68436 |
| [22] | Hoder, K., Voronkov, A.: Comparing unification algorithms in first-order theorem proving. In: Mertsching, B., Hund, M., Aziz, M.Z. (eds.) KI 2009, LNCS, vol. 5803, pp. 435-443. Springer (2009) |
| [23] | Huet, GP, A unification algorithm for typed lambda-calculus, Theor. Comput. Sci., 1, 1, 27-57 (1975) · Zbl 0332.02035 · doi:10.1016/0304-3975(75)90011-0 |
| [24] | Jensen, DC; Pietrzykowski, T., Mechanizing omega-order type theory through unification, Theor. Comput. Sci., 3, 2, 123-171 (1976) · Zbl 0361.02020 · doi:10.1016/0304-3975(76)90021-9 |
| [25] | Johnsson, T.: Lambda lifting: transforming programs to recursive equations. In: Jouannaud, J. (ed.) FPCA 1985, LNCS, vol. 201, pp. 190-203. Springer (1985) · Zbl 0568.68013 |
| [26] | Kaliszyk, C.; Urban, J., HOL(y)Hammer: online ATP service for HOL light, Math. Comput. Sci., 9, 1, 5-22 (2015) · Zbl 1322.68177 · doi:10.1007/s11786-014-0182-0 |
| [27] | Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263-297. Pergamon (1970) · Zbl 0188.04902 |
| [28] | Kohlhase, M.: A mechanization of sorted higher-order logic based on the resolution principle. Ph.D. thesis, Universität des Saarlandes, Saarbrücken, Germany (1994) |
| [29] | Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013, LNCS, vol. 8044, pp. 1-35. Springer (2013) |
| [30] | Manna, Z., Waldinger, R.: A deductive approach to program synthesis. In: Buchanan, B.G. (ed.) IJCAI-79, pp. 542-551. William Kaufmann (1979) · Zbl 0427.68023 |
| [31] | McCune, W.; Wos, L., Otter—the CADE-13 competition incarnations, J. Autom. Reason., 18, 2, 211-220 (1997) · doi:10.1023/A:1005843632307 |
| [32] | Murray, NV, Completely non-clausal theorem proving, Artif. Intell., 18, 1, 67-85 (1982) · Zbl 0472.68053 · doi:10.1016/0004-3702(82)90011-X |
| [33] | Nipkow, T.: Functional unification of higher-order patterns. In: Best, E. (ed.) LICS 1993, pp. 64-74. IEEE Computer Society (1993) |
| [34] | Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 335-367. Elsevier and MIT Press (2001) · Zbl 0992.03018 |
| [35] | Nummelin, V., Bentkamp, A., Tourret, S., Vukmirović, P.: Superposition with first-class Booleans and inprocessing clausification. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28, LNCS. Springer (2021) · Zbl 1540.03025 |
| [36] | Okasaki, C.: Purely Functional Data Structures. Cambridge University Press (1999) · Zbl 0941.68032 |
| [37] | Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL-2010, EPiC Series in Computing, vol. 2, pp. 1-11. EasyChair (2010) |
| [38] | Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25, LNCS, vol. 9195, pp. 399-415. Springer (2015) · Zbl 1465.68295 |
| [39] | Schulz, S., E—a brainiac theorem prover, AI Commun., 15, 2-3, 111-126 (2002) · Zbl 1020.68084 |
| [40] | Schulz, S., Cruanes, S., Vukmirović, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE-27, LNCS, vol. 11716, pp. 495-507. Springer (2019) · Zbl 1535.68460 |
| [41] | Schulz, S., Möhrmann, M.: Performance of clause selection heuristics for saturation-based theorem proving. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706, pp. 330-345. Springer (2016) · Zbl 1475.68450 |
| [42] | Steen, A.: Extensional paramodulation for higher-order logic and its effective implementation Leo-III. Ph.D. thesis, Free University of Berlin, Dahlem, Germany (2018) · Zbl 1402.68013 |
| [43] | Steen, A., Benzmüller, C.: There is no best \(\beta \)-normalization strategy for higher-order reasoners. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20, LNCS, vol. 9450, pp. 329-339. Springer (2015) · Zbl 1471.68318 |
| [44] | Steen, A.; Benzmüller, C., Extensional higher-order paramodulation in Leo-III, J. Autom. Reason., 65, 6, 775-807 (2021) · Zbl 1509.68321 · doi:10.1007/s10817-021-09588-x |
| [45] | Stump, A., Sutcliffe, G., Tinelli, C.: Starexec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014, LNCS, vol. 8562, pp. 367-373. Springer (2014) |
| [46] | Sultana, N.; Blanchette, JC; Paulson, LC, LEO-II and Satallax on the Sledgehammer test bench, J. Appl. Log., 11, 1, 91-102 (2013) · Zbl 1262.68161 · doi:10.1016/j.jal.2012.12.002 |
| [47] | Sutcliffe, G., The CADE ATP system competition-CASC, AI Mag., 37, 2, 99-101 (2016) · Zbl 0916.68141 |
| [48] | Sutcliffe, G., The TPTP problem library and associated infrastructure—from CNF to TH0. TPTP v6.4.0, J. Autom. Reason., 59, 4, 483-502 (2017) · Zbl 1425.68381 · doi:10.1007/s10817-017-9407-7 |
| [49] | Sutcliffe, G., The CADE-27 automated theorem proving system competition—CASC-27, AI Commun., 32, 5-6, 373-389 (2019) · Zbl 1464.68433 |
| [50] | Sutcliffe, G.: The 10th IJCAR automated theorem proving system competition—CASC-J10. AI Commun. (2021) · Zbl 1485.68287 |
| [51] | Turner, DA, Another algorithm for bracket abstraction, J. Symb. Log., 44, 2, 267-270 (1979) · Zbl 0408.03013 · doi:10.2307/2273733 |
| [52] | Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014, LNCS, vol. 8559, pp. 696-710. Springer (2014) · Zbl 1495.68240 |
| [53] | Vukmirović, P., Bentkamp, A., Nummelin, V.: Efficient full higher-order unification. In: Ariola, Z.M. (ed.) FSCD, LIPIcs, vol. 167, p. 5:1-5:17. Schloss Dagstuhl—Leibniz-Zentrum für Informatik (2020) · Zbl 1542.68214 |
| [54] | Vukmirović, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28, LNCS, vol. 12699, pp. 415-432. Springer (2021) · Zbl 1512.68431 |
| [55] | Vukmirović, P., Blanchette, J.C., Cruanes, S., Schulz, S.: Extending a brainiac prover to lambda-free higher-order logic. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019, Part I, LNCS, vol. 11427, pp. 192-210. Springer (2019) |
| [56] | Vukmirović, P., Nummelin, V.: Boolean reasoning in a higher-order superposition prover. In: Fontaine, P., Korovin, K., Kotsireas, I. S., Rümmer, P., Tourret, S. (eds.) PAAR-2020, CEUR Workshop Proceedings, vol. 2752, pp. 148-166. CEUR-WS.org (2020) |
| [57] | Waldmann, U., Tourret, S., Robillard, S., Blanchette, J.: A comprehensive framework for saturation theorem proving. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020, Part I, LNCS, vol. 12166, pp. 316-334. Springer (2020) · Zbl 1512.68433 |
| [58] | Wisniewski, M., Steen, A., Kern, K., Benzmüller, C.: Effective normalization techniques for HOL. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016, LNCS, vol. 9706, pp. 362-370. Springer (2016) · Zbl 1475.68453 |
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.
