Superposition for lambda-free higher-order logic. (English) Zbl 1535.03060
Summary: We introduce refutationally complete superposition calculi for intentional and extensional clausal \(\lambda \)-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the \(\lambda \)-free higher-order lexicographic path and Knuth-Bendix orders. We implemented the calculi in the Zipperposition prover and evaluated them on Isabelle/HOL and TPTP benchmarks. They appear promising as a stepping stone towards complete, highly efficient automatic theorem provers for full higher-order logic.
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 03B16 | Higher-order logic |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
Keywords:
superposition calculus; Boolean-free lambda-free higher-order logic; refutational completenessSoftware:
Coq; Sledgehammer; Metis_; Zipperposition; VAMPIRE; Isabelle/HOL; StarExec; DISCOUNT; Satallax; Lambda Free RPOs; E Theorem ProverReferences:
| [1] | Jürgen Avenhaus, Jörg Denzinger, and Matthias Fuchs. DISCOUNT: A system for distributed equational deduction. In Jieh Hsiang, editor,RTA-95, volume 914 ofLNCS, pages 397-402. Springer, 1995. |
| [2] | Peter B. Andrews. Resolution in type theory.J. Symb. Log., 36(3):414-432, 1971. · Zbl 0231.02038 |
| [3] | Peter B. Andrews. Classical type theory. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume II, pages 965-1007. Elsevier and MIT Press, 2001. · Zbl 0992.03011 |
| [4] | Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, and Uwe Waldmann. Superposition for lambda-free higher-order logic. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors,IJCAR 2018, volume 10900 ofLNCS, pages 28-46. Springer, 2018. · Zbl 1511.68302 |
| [5] | Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone. Encoding monomorphic and polymorphic types.Log. Meth. Comput. Sci., 12(4:13):1-52, 2016. · Zbl 1445.68327 |
| [6] | Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. A transfinite Knuth-Bendix order for lambda-free higher-order terms. In Leonardo de Moura, editor,CADE-26, · Zbl 1496.03037 |
| [7] | Yves Bertot and Pierre Castéran.Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. · Zbl 1069.68095 |
| [8] | Michael Beeson. Lambda logic. In David A. Basin and Michaël Rusinowitch, editors,IJCAR 2004, volume 3097 ofLNCS, pages 460-474. Springer, 2004. · Zbl 1127.03009 |
| [9] | Alexander Bentkamp. Formalization of the embedding path order for lambda-free higher-order terms.Archive of Formal Proofs, 2018.http://isa-afp.org/entries/Lambda_Free_EPO.html. |
| [10] | Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification.J. Log. Comput., 4(3):217-247, 1994. · Zbl 0814.68117 |
| [11] | Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In John Alan Robinson and Andrei Voronkov, editors,Handbook of Automated Reasoning, volume I, pages 19-99. Elsevier · Zbl 0993.03008 |
| [12] | Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED.J. Formaliz. Reas., 9(1):101-148, 2016. · Zbl 1451.68318 |
| [13] | Christoph Benzmüller and Dale Miller. Automation of higher-order logic. In Jörg H. Siekmann, editor,Computational Logic, volume 9 ofHandbook of the History of Logic, pages 215-254. Elsevier, 2014. · Zbl 1404.03005 |
| [14] | Sascha Böhme and Tobias Nipkow. Sledgehammer: Judgement Day. In Jürgen Giesl and Reiner Hähnle, editors,IJCAR 2010, volume 6173 ofLNCS, pages 107-121. Springer, 2010. · Zbl 1291.68327 |
| [15] | François Bobot and Andrei Paskevich. Expressing polymorphic types in a many-sorted language. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors,FroCoS 2011, volume 6989 ofLNCS, pages 87-102. Springer, 2011. · Zbl 1348.68215 |
| [16] | Jasmin Christian Blanchette and Andrei Paskevich. TFF1: The TPTP typed first-order form with rank-1 polymorphism. In Maria Paola Bonacina, editor,CADE-24, volume 7898 ofLNCS, · Zbl 1381.68260 |
| [17] | Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, and Arnaud Fietzke. LEO-II—A cooperative automatic theorem prover for higher-order logic. In Alessandro Armando, Peter · Zbl 1165.68446 |
| [18] | Miquel Bofill and Albert Rubio. Paramodulation with non-monotonic orderings and simplification. J. Autom. Reason., 50(1):51-98, 2013. · Zbl 1315.03017 |
| [19] | Ahmed Bhayat and Giles Reger. Restricted combinatory unification. In Pascal Fontaine, editor, CADE-27, volume 11716 ofLNCS, pages 74-93. Springer, 2019. · Zbl 1535.68445 |
| [20] | Ahmed Bhayat and Giles Reger. A combinator-based superposition calculus for higher-order logic. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors,IJCAR 2020, Part I, volume · Zbl 07614518 |
| [21] | D. Brand. Proving theorems with the modification method.SIAM J. Comput., 4:412-430, 1975. [BREO+19] Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, and Clark Barrett. Extending SMT solvers to higher-order logic. In Pascal Fontaine, editor,CADE-27, volume · Zbl 0333.68059 |
| [22] | Chad E. Brown. Satallax: An automatic higher-order prover. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors,IJCAR 2012, volume 7364 ofLNCS, pages 111-117. Springer, 2012. · Zbl 1358.68250 |
| [23] | Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. A lambda-free higher-order recursive path order. In Javier Esparza and Andrzej S. Murawski, editors,FoSSaCS 2017, volume · Zbl 1486.68085 |
| [24] | Alonzo Church. A formulation of the simple theory of types.J. Symb. Log., 5(2):56-68, 1940. · Zbl 0023.28901 |
| [25] | Iliano Cervesato and Frank Pfenning. A linear spine calculus.J. Log. Comput., 13(5):639-688, 2003. · Zbl 1041.03007 |
| [26] | Simon Cruanes.Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond. Ph.D. thesis, École polytechnique, 2015. · Zbl 1496.68365 |
| [27] | Simon Cruanes. Superposition with structural induction. In Clare Dixon and Marcelo Finger, editors,FroCoS 2017, volume 10483 ofLNCS, pages 172-188. Springer, 2017. · Zbl 1496.68365 |
| [28] | Łukasz Czajka. Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions. In Jeremy Avigad and Adam Chlipala, editors,CPP 2016, pages 49-57. |
| [29] | Vincent J. Digricoli and Malcolm C. Harrison. Equality-based binary resolution.J. ACM, 33(2):253-289, 1986. |
| [30] | Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Higher-order unification via explicit substitutions (extended abstract). InLICS ’95, pages 366-374. IEEE Computer Society, 1995. · Zbl 1005.03016 |
| [31] | Daniel J. Dougherty. Higher-order unification via combinators.Theor. Comput. Sci., 114(2):273- 298, 1993. · Zbl 0772.68061 |
| [32] | Melvin Fitting.First-Order Logic and Automated Theorem Proving. Springer-Verlag, 2nd edition, 1996. · Zbl 0848.68101 |
| [33] | Melvin Fitting.Types, Tableaus, and Gödel’s God. Kluwer, 2002. · Zbl 1038.03001 |
| [34] | Ashutosh Gupta, Laura Kovács, Bernhard Kragl, and Andrei Voronkov. Extensional crisis and proving identity. In Franck Cassez and Jean-François Raskin, editors,ATVA 2014, volume 8837 ofLNCS, pages 185-200. Springer, 2014. · Zbl 1448.68459 |
| [35] | M. J. C. Gordon and T. F. Melham, editors.Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993. · Zbl 0779.68007 |
| [36] | Leon Henkin. Completeness in the theory of types.J. Symb. Log., 15(2):81-91, 1950. · Zbl 0039.00801 |
| [37] | Nao Hirokawa, Aart Middeldorp, and Harald Zankl. Uncurrying for termination and complexity. J. Autom. Reasoning, 50(3):279-315, 2013. · Zbl 1286.68262 |
| [38] | Gérard P. Huet. A mechanization of type theory. In Nils J. Nilsson, editor,IJCAI-73, pages 139-146. William Kaufmann, 1973. |
| [39] | Joe Hurd. First-order proof tactics in higher-order logic theorem provers. In Myla Archer, Ben Di Vito, and César Muñoz, editors,Design and Application of Strategies/Tactics in Higher · Zbl 1072.68578 |
| [40] | Manfred Kerber. How to prove higher order theorems in first order logic. In John Mylopoulos and Raymond Reiter, editors,IJCAI-91, pages 137-142. Morgan Kaufmann, 1991. · Zbl 0746.68081 |
| [41] | Cynthia Kop.Higher Order Termination: Automatable Techniques for Proving Termination of Higher-Order Term Rewriting Systems. Ph.D. thesis, Vrije Universiteit Amsterdam, 2012. · Zbl 1437.68080 |
| [42] | Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Sharygina and Helmut Veith, editors,CAV 2013, volume 8044 ofLNCS, pages 1-35. Springer, |
| [43] | Daniel Leivant. Higher order logic. In Dov M. Gabbay, Christopher J. Hogger, J. A. Robinson, and Jörg H. Siekmann, editors,Handbook of Logic in Artificial Intelligence and Logic Programming, · Zbl 0467.03015 |
| [44] | Fredrik Lindblad. A focused sequent calculus for higher-order logic. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors,IJCAR 2014, volume 8562 ofLNCS, pages 61-75. Springer, 2014. · Zbl 1423.68421 |
| [45] | Dale A. Miller. A compact representation of proofs.Studia Logica, 46(4):347-370, 1987. · Zbl 0644.03033 |
| [46] | Jia Meng and Lawrence C. Paulson. Translating higher-order clauses to first-order clauses.J. Autom. Reason., 40(1):35-60, 2008. · Zbl 1203.68188 |
| [47] | Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel.Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 ofLNCS. Springer, 2002. · Zbl 0994.68131 |
| [48] | Fritz H. Obermeyer.Automated Equational Reasoning in Nondeterministicλ-Calculi Modulo TheoriesH∗. Ph.D. thesis, Carnegie Mellon University, 2009. |
| [49] | Nicolas Peltier. A variant of the superposition calculus.Archive of Formal Proofs, 2016. |
| [50] | J.A. Robinson. Mechanizing higher order logic. In B. Meltzer and D. Michie, editors,Machine Intelligence, volume 4, pages 151-170. Edinburgh University Press, 1969. · Zbl 0228.68025 |
| [51] | J.A. Robinson. A note on mechanizing higher order logic. In B. Meltzer and D. Michie, editors, Machine Intelligence, volume 5, pages 121-135. Edinburgh University Press, 1970. |
| [52] | Alexander Steen and Christoph Benzmüller. The higher-order prover Leo-III. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors,IJCAR 2018, volume 10900 ofLNCS, pages · Zbl 1511.68332 |
| [53] | Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, and Frank Theiss. Progress in the development of automated theorem proving for higher-order logic. In Renate A. Schmidt, editor, · Zbl 1250.68236 |
| [54] | Nik Sultana, Jasmin Christian Blanchette, and Lawrence C. Paulson. LEO-II and Satallax on the Sledgehammer test bench.J. Applied Logic, 11(1):91-102, 2013. · Zbl 1262.68161 |
| [55] | Stephan Schulz. E - a brainiac theorem prover.AI Commun., 15(2-3):111-126, 2002. · Zbl 1020.68084 |
| [56] | Stephan Schulz. Fingerprint indexing for paramodulation and rewriting. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors,IJCAR 2012, volume 7364 ofLNCS, pages 477-483. Springer, · Zbl 1358.68263 |
| [57] | Stephan Schulz. System description: E 1.8. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov, editors,LPAR-19, volume 8312 ofLNCS, pages 735-743. Springer, 2013. · Zbl 1407.68442 |
| [58] | Wayne Snyder and Christopher Lynch. Goal directed strategies for paramodulation. In Ronald V. Book, editor,RTA-91, volume 488 ofLNCS, pages 150-161. Springer, 1991. · Zbl 1503.68295 |
| [59] | Manfred Schmidt-Schauß. Unification in a combination of arbitrary disjoint equational theories. J. Symb. Comput., 8:51-99, 1989. · Zbl 0691.03003 |
| [60] | Geoff Sutcliffe, Stephan Schulz, Koen Claessen, and Peter Baumgartner. The TPTP typed first-order form with arithmetic. In Nikolaj Bjørner and Andrei Voronkov, editors,LPAR-18, · Zbl 1352.68217 |
| [61] | Aaron Stump, Geoff Sutcliffe, and Cesare Tinelli. StarExec: A cross-community infrastructure for logic solving. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors,IJCAR |
| [62] | Stephan Schulz, Geoff Sutcliffe, Josef Urban, and Adam Pease. Detecting inconsistencies in large first-order knowledge bases. In Leonardo de Moura, editor,CADE-26, volume 10395 ofLNCS, pages 310-325. Springer, 2017. · Zbl 1494.68262 |
| [63] | Jouko Väänänen. Second-order and higher-order logic. In Edward N. Zalta, editor,The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, fall 2019 edition, 2019. · Zbl 1002.03013 |
| [64] | Petar Vukmirović, Jasmin Christian Blanchette, Simon Cruanes, and Stephan Schulz. Extending a brainiac prover to lambda-free higher-order logic. In Tomas Vojnar and Lijun Zhang, editors, · Zbl 1535.68460 |
| [65] | Daniel Wand.Superposition: Types and Polymorphism. Ph.D. thesis, Universität des Saarlandes, 2017. |
| [66] | Uwe Waldmann, Sophie Tourret, Simon Robillard, and Jasmin Blanchette. A comprehensive framework for saturation theorem proving. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors,IJCAR 2020, Part I, volume 12166 ofLNCS, pages 316-334. Springer, 2020. · Zbl 1512.68433 |
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.
