Top

Journal of Automated Reasoning

Published in:

27-03-2021

Extensional Higher-Order Paramodulation in Leo-III

Authors: Alexander Steen, Christoph Benzmüller

Published in: Journal of Automated Reasoning | Issue 6/2021

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Leo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The prover may cooperate with multiple external specialist reasoning systems such as first-order provers and SMT solvers. Leo-III is compatible with the TPTP/TSTP framework for input formats, reporting results and proofs, and standardized communication between reasoning systems, enabling, e.g., proof reconstruction from within proof assistants such as Isabelle/HOL. Leo-III supports reasoning in polymorphic first-order and higher-order logic, in many quantified normal modal logics, as well as in different deontic logics. Its development had initiated the ongoing extension of the TPTP infrastructure to reasoning within non-classical logics.

previous article On the Importance of Domain Model Configuration for Automated Planning Engines

next article Automated Reasoning with Restricted Intensional Sets

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Available only for authorised users

Note the different capitalization of Leo-III as opposed to LEO-I and LEO-II. This is motivated by the fact that Leo-III is designed to be a general-purpose system rather than a subcomponent to another system. Hence, the original capitalization derived from the phrase “Logical Engine for Omega” (LEO) is not continued.

See http://tptp.org/TPTP/Proposals/LogicSpecification.html.

See the individual projects related to the Leo prover family at https://github.com/leoprover. Further information is available at http://inf.fu-berlin.de/~lex/leo3.

As a simple counterexample, consider a (strict) term ordering \(\succ \) for HOL terms that satisfies the usual properties from first-order superposition (e.g., the subterm property) and is compatible with \(\beta \)-reduction. For any non-empty signature \(\Sigma \), \(\mathrm {c} \in \Sigma \), the chain \(\mathrm {c} \equiv _\beta (\uplambda X.\, \mathrm {c}) \; \mathrm {c} \succ \mathrm {c}\) can be constructed, implying \(\mathrm {c} \succ \mathrm {c}\) and thus contradicting irreflexivity of \(\succ \). Note that \((\uplambda X.\, \mathrm {c}) \; \mathrm {c} \succ \mathrm {c}\) since the right-hand side is a proper subterm of the left-hand side (assuming an adequately lifted definition of subterm property to HO terms).

The Identity of Indiscernibles (also known as Leibniz’s law) refers to a principle first formulated by Gottfried Leibniz in the context of theoretical philosophy [71]. The principle states that if two objects X and Y coincide on every property P, then they are equal, i.e., \(\forall X_\tau .\,\forall Y_\tau .\,\left( \forall P_{o\tau }. P \; X \Leftrightarrow P \; Y\right) \Rightarrow X = Y\), where “\(=\)” denotes the desired equality predicate. Since this principle can easily be formulated in HOL, it is possible to encode equality in higher-order logic without using the primitive equality predicate. An extensive analysis of the intricate differences between primitive equality and defined notions of equality is presented by Benzmüller et al. [22] to which the authors refer for further details.

In fact, the implementation of Leo-III employs a nameless representation of bound variables such that variable capture is avoided by design, cf. §4.5 for details.

The set \(\mathcal {GB}_{\tau }^{t}\) of approximating/partial bindings parametric to a type \(\tau = {\beta {\alpha ^n\ldots \alpha ^1}}\) (for \(n\ge 0\)) and to a constant t of type \({\beta {\gamma ^m\ldots \gamma ^1}}\) (for \(m\ge 0\)) is defined as follows (for further details see also [88]): Given a “name” k (where a name is either a constant or a variable) of type \({\beta {\gamma ^m\ldots \gamma ^1}}\), the term l having form \(\uplambda {X^1_{\alpha ^{1}}. \ldots \uplambda X^n_{\alpha ^{n}}}. (k\, {{r^1}\ldots {r^m}})\) is a partial binding of type \({\beta {\alpha ^n\ldots \alpha ^1}}\) and head k. Each \({r}^{i \le m}\) has form \(H^i {X^1_{\alpha ^1}\ldots X^n_{\alpha ^n}}\) where \(H^{i\le m}\) are fresh variables typed \(\gamma ^{i\le m}{\alpha ^n\ldots \alpha ^1}\). Projection bindings are partial bindings whose head k is one of \(X^{i\le l}\). Imitation bindings are partial bindings whose head k is identical to the given constant symbol t in the superscript of \(\mathcal {GB}_{\tau }^{t}\). \(\mathcal {GB}_{\tau }^{t}\) is the set of all projection and imitation bindings modulo type \(\tau \) and constant t. In our example derivation we twice use imitation bindings of form \(\uplambda X_\iota . \lnot (H_{o\iota } X_\iota )\) from \(\mathcal {GB}_{o\iota }^{\lnot }\).

Leo’s Parallel Architecture and Datastructures (LeoPARD) can be found at https://github.com/leoprover/LeoPARD.

See http://tptp.org/TPTP/Proposals/LogicSpecification.html.

Remark on CAX: In this special case of THM (theorem), the given axioms are inconsistent so that anything follows, including the given conjecture. Hence, it is counted against solved problems.

This information is extracted from the TPTP problem rating information that is attached to each problem. The unsolved problems are NLP004⌃7, SET013⌃7, SEU558⌃1, SEU683⌃1, SEV143⌃5, SYO037⌃1, SYO062⌃4.004, SYO065⌃4.001, SYO066⌃4.004, MSC007⌃1.003.004, SEU938⌃5 and SEV106⌃5.

HOLyHammer (HOL ATP) and Zipperposition (first-order ATP) are the only other systems supporting polymorphism.

Abadi, M., Cardelli, L., Curien, P., Lévy, J.: Explicit substitutions. J. Funct. Program. 1(4), 375–416 (1991). https://doi.org/10.1017/S0956796800000186MathSciNetCrossRefMATH

Andrews, P.B.: Resolution in type theory. J. Symb. Log. 36(3), 414–432 (1971)MathSciNetCrossRef

Andrews, P.B.: General models and extensionality. J. Symb. Log. 37(2), 395–397 (1972). https://doi.org/10.2307/2272982MathSciNetCrossRefMATH

Andrews, P.B.: General models, descriptions, and choice in type theory. J. Symb. Log. 37(2), 385–394 (1972). https://doi.org/10.2307/2272981MathSciNetCrossRefMATH

Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory. Springer, Applied Logic Series (2002)

Andrews, P.B., Bishop, M., Brown, C.E.: System description: TPS: A theorem proving system for type theory. In: D.A. McAllester (ed.) Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, Lecture Notes in Computer Science, vol. 1831, pp. 164–169. Springer (2000). https://doi.org/10.1007/10721959_11

Andrews, P.B., Brown, C.E.: TPS: a hybrid automatic-interactive system for developing proofs. J. Appl. Logic 4(4), 367–395 (2006). https://doi.org/10.1016/j.jal.2005.10.002MathSciNetCrossRefMATH

Andrews, P.B., Miller, D.A., Cohen, E.L., Pfenning, F.: Automating higher-order logic. Contemp. Math. 29, 169–192 (1984)MathSciNetCrossRef

Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: M.E. Stickel (ed.) 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, Lecture Notes in Computer Science, vol. 449, pp. 427–441. Springer (1990). https://doi.org/10.1007/3-540-52885-7_105

10.

Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994). https://doi.org/10.1093/logcom/4.3.217MathSciNetCrossRefMATH

11.

Barbosa, H., Reynolds, A., Ouraoui, D.E., Tinelli, C., Barrett, C.W.: Extending SMT solvers to higher-order logic. In: P. Fontaine (ed.) Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11716, pp. 35–54. Springer (2019). https://doi.org/10.1007/978-3-030-29436-6_3

12.

Barcan, R.C.: A functional calculus of first order based on strict implication. J. Symb. Log. 11(1), 1–16 (1946). https://doi.org/10.2307/2269159MathSciNetCrossRefMATH

13.

Barendregt, H.P., Dekkers, W., Statman, R.: Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, Cambridge (2013)CrossRef

14.

Barrett, C., et al.: CVC4. In: G. Gopalakrishnan, S. Qadeer (eds.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, LNCS, vol. 6806, pp. 171–177. Springer (2011). https://doi.org/10.1007/978-3-642-22110-1_14

15.

Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovic, P., Waldmann, U.: Superposition with lambdas. In: P. Fontaine (ed.) Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11716, pp. 55–73. Springer (2019). https://doi.org/10.1007/978-3-030-29436-6_4

16.

Bentkamp, A., Blanchette, J.C., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. In: D. Galmiche, S. Schulz, R. Sebastiani (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Lecture Notes in Computer Science, vol. 10900, pp. 28–46. Springer (2018). https://doi.org/10.1007/978-3-319-94205-6_3

17.

Benzmüller, C.: Equality and extensionality in automated higher order theorem proving. Ph.D. thesis, Saarland University, Saarbrücken, Germany (1999)

18.

Benzmüller, C.: Extensional higher-order paramodulation and RUE-resolution. In: H. Ganzinger (ed.) Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, Lecture Notes in Computer Science, vol. 1632, pp. 399–413. Springer (1999). https://doi.org/10.1007/3-540-48660-7_39

19.

Benzmüller, C.: Combining and automating classical and non-classical logics in classical higher-order logics. Ann. Math. Artif. Intell. 62(1–2), 103–128 (2011). https://doi.org/10.1007/s10472-011-9249-7MathSciNetCrossRefMATH

20.

Benzmüller, C.: Cut-elimination for quantified conditional logic. J. Philos. Logic 46(3), 333–353 (2017). https://doi.org/10.1007/s10992-016-9403-0MathSciNetCrossRefMATH

21.

Benzmüller, C.: Universal (meta-)logical reasoning: recent successes. Sci. Comput. Prog. 172, 48–62 (2019). https://doi.org/10.1016/j.scico.2018.10.008CrossRef

22.

Benzmüller, C., Brown, C.E., Kohlhase, M.: Higher-order semantics and extensionality. J. Symb. Log. 69(4), 1027–1088 (2004). https://doi.org/10.2178/jsl/1102022211MathSciNetCrossRefMATH

23.

Benzmüller, C., Brown, C.E., Kohlhase, M.: Cut-simulation and impredicativity. Logical Methods Comput. Sci. 5(1), (2009)

24.

Benzmüller, C., Farjami, A., Parent, X.: A dyadic deontic logic in HOL. In: J.M. Broersen, C. Condoravdi, N. Shyam, G. Pigozzi (eds.) Deontic Logic and Normative Systems - 14th International Conference, DEON 2018, Utrecht, The Netherlands, July 3-6, 2018., pp. 33–49. College Publications (2018)

25.

Benzmüller, C., Kohlhase, M.: System description: LEO - A higher-order theorem prover. In: C. Kirchner, H. Kirchner (eds.) Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings, Lecture Notes in Computer Science, vol. 1421, pp. 139–144. Springer (1998). https://doi.org/10.1007/BFb0054256

26.

Benzmüller, C., Miller, D.: Automation of higher-order logic. In: Siekmann, J.H. (ed.) Computational Logic, Handbook of the History of Logic. Elsevier, Amsterdam (2014)MATH

27.

Benzmüller, C., Otten, J., Raths, T.: Implementing and evaluating provers for first-order modal logics. In: L.D. Raedt, et al. (eds.) ECAI 2012 - 20th European Conference on Artificial Intelligence. Including prestigious applications of artificial intelligence (PAIS-2012) system demonstrations track, montpellier, France, August 27-31 , 2012, Frontiers in Artificial Intelligence and applications, vol. 242, pp. 163–168. IOS Press (2012). https://doi.org/10.3233/978-1-61499-098-7-163

28.

Benzmüller, C., Paulson, L.C.: Multimodal and intuitionistic logics in simple type theory. Logic J. IGPL 18(6), 881–892 (2010). https://doi.org/10.1093/jigpal/jzp080MathSciNetCrossRefMATH

29.

Benzmüller, C., Paulson, L.C.: Quantified multimodal logics in simple type theory. Logica Univ. 7(1), 7–20 (2013). https://doi.org/10.1007/s11787-012-0052-yMathSciNetCrossRefMATH

30.

Benzmüller, C., Raths, T.: HOL based first-order modal logic provers. In: K.L. McMillan, A. Middeldorp, A. Voronkov (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8312, pp. 127–136. Springer (2013). https://doi.org/10.1007/978-3-642-45221-5_9

31.

Benzmüller, C., Scott, D.S.: Automating free logic in Isabelle/HOL. In: G. Greuel, T. Koch, P. Paule, A.J. Sommese (eds.) Mathematical software - ICMS 2016 - 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, Lecture Notes in Computer Science, vol. 9725, pp. 43–50. Springer (2016). https://doi.org/10.1007/978-3-319-42432-3_6

32.

Benzmüller, C., Steen, A., Wisniewski, M.: Leo-III Version 1.1 (System description). In: T. Eiter, D. Sands, G. Sutcliffe, A. Voronkov (eds.) IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana, May 7-12, 2017, Kalpa publications in computing, vol. 1. EasyChair (2017). https://doi.org/10.29007/grmx

33.

Benzmüller, C., Sultana, N., Paulson, L.C., Theiss, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389–404 (2015). https://doi.org/10.1007/s10817-015-9348-yMathSciNetCrossRefMATH

34.

Benzmüller, C., Weber, L., Woltzenlogel Paleo, B.: Computer-assisted analysis of the Anderson-Hájek ontological controversy. Logica Univ. 11(1), 139–151 (2017). https://doi.org/10.1007/s11787-017-0160-9CrossRefMATH

35.

Benzmüller, C., Woltzenlogel Paleo, B.: The inconsistency in Gödel’s ontological argument: A success story for AI in metaphysics. In: S. Kambhampati (ed.) Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pp. 936–942. IJCAI/AAAI Press (2016)

36.

Benzmüller, C., Woltzenlogel Paleo, B.: Experiments in computational metaphysics: Gödel’s proof of God’s existence Savijnanam scientific exploration for a spiritual paradigm. J. Bhaktivedanta Inst. 9, 43–57 (2017)

37.

Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin (2004)MATH

38.

Bhayat, A., Reger, G.: Set of support for higher-order reasoning. In: B. Konev, J. Urban, P. Rümmer (eds.) Proceedings of the 6th Workshop on practical aspects of automated reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, July 19th, 2018., CEUR Workshop Proceedings, vol. 2162, pp. 2–16. CEUR-WS.org (2018)

39.

Bhayat, A., Reger, G.: Restricted combinatory unification. In: P. Fontaine (ed.) Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11716, pp. 74–93. Springer (2019). https://doi.org/10.1007/978-3-030-29436-6_5

40.

Blackburn, P., van Benthem, J.F., Wolter, F.: Handbook of modal logic, vol. 3. Elsevier, Amsterdam (2006)MATH

41.

Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013). https://doi.org/10.1007/s10817-013-9278-5MathSciNetCrossRefMATH

42.

Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Logical methods in computer science 12(4), (2016). https://doi.org/10.2168/LMCS-12(4:13)2016

43.

Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: M. Kaufmann, L.C. Paulson (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6172, pp. 131–146. Springer (2010). https://doi.org/10.1007/978-3-642-14052-5_11

44.

Blanchette, J.C., Paskevich, A.: TFF1: the TPTP typed first-order form with rank-1 polymorphism. In: M.P. Bonacina (ed.) Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, LNCS, vol. 7898, pp. 414–420. Springer (2013). https://doi.org/10.1007/978-3-642-38574-2_29

45.

Blanchette, J.C., Weber, T., Batty, M., Owens, S., Sarkar, S.: Nitpicking C++ concurrency. In: P. Schneider-Kamp, M. Hanus (eds.) Proceedings of the 13th International ACM SIGPLAN Conference on principles and practice of declarative programming, July 20-22, 2011, Odense, Denmark, pp. 113–124. ACM (2011). https://doi.org/10.1145/2003476.2003493

46.

Böhme, S.: Proving theorems of higher-order logic with SMT solvers. Ph.D. thesis, Technische Universität München (2012)

47.

Brown, C.E.: Satallax: An automatic higher-order prover. In: B. Gramlich, D. Miller, U. Sattler (eds.) Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7364, pp. 111–117. Springer (2012). https://doi.org/10.1007/978-3-642-31365-3_11

48.

Brown, C.E., Gauthier, T., Kaliszyk, C., Sutcliffe, G., Urban, J.: GRUNGE: A grand unified ATP challenge. In: P. Fontaine (ed.) Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11716, pp. 123–141. Springer (2019). https://doi.org/10.1007/978-3-030-29436-6_8

49.

Bruijn, N.G.D.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. INDAG. Math 34, 381–392 (1972)MathSciNetCrossRef

50.

Cervesato, I., Pfenning, F.: A linear spine calculus. J. Log. Comput. 13(5), 639–688 (2003). https://doi.org/10.1093/logcom/13.5.639MathSciNetCrossRefMATH

51.

Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56–68 (1940). https://doi.org/10.2307/2266170MathSciNetCrossRefMATH

52.

Couchot, J., Lescuyer, S.: Handling polymorphism in automated deduction. In: F. Pfenning (ed.) Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4603, pp. 263–278. Springer (2007). https://doi.org/10.1007/978-3-540-73595-3_18

53.

Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. (extensions de la superposition pour l’arithmétique linéaire entière, l’induction structurelle, et bien plus encore). Ph.D. thesis, École Polytechnique, Palaiseau, France (2015)

54.

Denzinger, J., Kronenburg, M., Schulz, S.: Discount-a distributed and learning equational prover. J. Autom. Reason. 18(2), 189–198 (1997). https://doi.org/10.1023/A:1005879229581CrossRef

55.

Digricoli, V.J., Harrison, M.C.: Equality-based binary resolution. J. ACM 33(2), 253–289 (1986). https://doi.org/10.1145/5383.5389MathSciNetCrossRef

56.

Frege, G.: Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Verlag von Louis Nebert, Halle (1879)

57.

Fuenmayor, D., Benzmüller, C.: Types, tableaus and Gödel’s God in Isabelle/HOL. Arch. Formal Proofs (2017)

58.

Gleißner, T., Steen, A.: The MET: The art of flexible reasoning with modalities. In: C. Benzmüller, F. Ricca, X. Parent, D. Roman (eds.) Rules and Reasoning - Second International Joint Conference, RuleML+RR 2018, Luxembourg, September 18-21, 2018, Proceedings, LNCS, vol. 11092, pp. 274–284. Springer (2018). https://doi.org/10.1007/978-3-319-99906-7_19

59.

Gleißner, T., Steen, A., Benzmüller, C.: Theorem provers for every normal modal logic. In: T. Eiter, D. Sands (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, EPiC Series in Computing, vol. 46, pp. 14–30. EasyChair (2017). https://doi.org/10.29007/jsb9

60.

Goldfarb, W.D.: The undecidability of the second-order unification problem. Theor. Comput. Sci. 13(2), 225–230 (1981)MathSciNetCrossRef

61.

Gordon, M.J., Melham, T.F.: Introduction to HOL A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)MATH

62.

Hales, T.C., et al.: A formal proof of the kepler conjecture. CoRR abs/1501.02155 (2015)

63.

Harrison, J.: HOL Light: An overview. In: S. Berghofer, T. Nipkow, C. Urban, M. Wenzel (eds.) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5674, pp. 60–66. Springer (2009). https://doi.org/10.1007/978-3-642-03359-9_4

64.

Henkin, L.: Completeness in the theory of types. J. Symb. Log. 15(2), 81–91 (1950). https://doi.org/10.2307/2266967MathSciNetCrossRefMATH

65.

Huet, G.P.: The undecidability of unification in third order logic. Inf. control 22(3), 257–267 (1973)MathSciNetCrossRef

66.

Hustadt, U., Schmidt, R.A.: MSPASS: modal reasoning by translation and first-order resolution. In: R. Dyckhoff (ed.) Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings, Lecture Notes in Computer Science, vol. 1847, pp. 67–71. Springer (2000). https://doi.org/10.1007/10722086_7

67.

Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: the TPTP typed higher-order form with rank-1 polymorphism. In: P. Fontaine, S. Schulz, J. Urban (eds.) Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning, CEUR Workshop Proceedings, vol. 1635, pp. 41–55. CEUR-WS.org (2016)

68.

Kfoury, A.J., Rocca, S.R.D., Tiuryn, J., Urzyczyn, P.: Alpha-conversion and typability. Inf. Comput. 150(1), 1–21 (1999). https://doi.org/10.1006/inco.1998.2756MathSciNetCrossRefMATH

69.

Kirchner, D., Benzmüller, C., Zalta, E.N.: Computer science and metaphysics: a cross-fertilization. Open Philos. 2(1), 230–251 (2019). https://doi.org/10.1515/opphil-2019-0015CrossRef

70.

Korovin, K.: iProver - an instantiation-based theorem prover for first-order logic (system description). In: A. Armando, P. Baumgartner, G. Dowek (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, LNCS, vol. 5195, pp. 292–298. Springer (2008). https://doi.org/10.1007/978-3-540-71070-7_24

71.

Leibniz, G.W.: Discourse on metaphysics. In: L.E. Loemker (ed.) Philosophical Papers and Letters, pp. 303–330. Springer Netherlands, Dordrecht (1989). https://doi.org/10.1007/978-94-010-1426-7_36

72.

Lindblad, F.: A focused sequent calculus for higher-order logic. In: S. Demri, D. Kapur, C. Weidenbach (eds.) Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8562, pp. 61–75. Springer (2014). https://doi.org/10.1007/978-3-319-08587-6_5

73.

Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning 40(1), 35–60 (2008). https://doi.org/10.1007/s10817-007-9085-yMathSciNetCrossRefMATH

74.

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

75.

Miller, D.A.: Proofs in higher-order logic. Ph.D. thesis, Carnegie-Mellon University (1983)

76.

Miller, D.A.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput. 1(4), 497–536 (1991). https://doi.org/10.1093/logcom/1.4.497MathSciNetCrossRefMATH

77.

Muskens, R.: Intensional models for the theory of types. J. Symb. Log. 72(1), 98–118 (2007). https://doi.org/10.2178/jsl/1174668386MathSciNetCrossRefMATH

78.

Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering constrained clauses. In: D. Kapur (ed.) Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, Lecture Notes in Computer Science, vol. 607, pp. 477–491. Springer (1992). https://doi.org/10.1007/3-540-55602-8_186

79.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science. Springer, Berlin (2002)MATH

80.

Otten, J.: MleanCoP: A connection prover for first-order modal logic. In: S. Demri, D. Kapur, C. Weidenbach (eds.) Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8562, pp. 269–276. Springer (2014). https://doi.org/10.1007/978-3-319-08587-6_20

81.

Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: D. Kapur (ed.) Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, Lecture Notes in Computer Science, vol. 607, pp. 748–752. Springer (1992). https://doi.org/10.1007/3-540-55602-8_217

82.

Raths, T., Otten, J.: The QMLTP problem library for first-order modal logics. In: B. Gramlich, D. Miller, U. Sattler (eds.) Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, LNCS, vol. 7364, pp. 454–461. Springer (2012). https://doi.org/10.1007/978-3-642-31365-3_35

83.

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

84.

Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. Mach. Intell. 4, 135–150 (1969)MathSciNetMATH

85.

Schulz, S.: E-A Brainiac theorem prover. AI Commun. 15(3), 111–126 (2002)MATH

86.

Siekmann, J.H., Benzmüller, C., Autexier, S.: Computer supported mathematics with \(\Omega \)MEGA. J. Appl. Logic 4(4), 533–559 (2006). https://doi.org/10.1016/j.jal.2005.10.008MathSciNetCrossRefMATH

87.

Slind, K., Norrish, M.: A brief overview of HOL4. In: O.A. Mohamed, C.A. Muñoz, S. Tahar (eds.) Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, Lecture Notes in Computer Science, vol. 5170, pp. 28–32. Springer (2008). https://doi.org/10.1007/978-3-540-71067-7_6

88.

Snyder, W., Gallier, J.: Higher-Order unification revisited: complete sets of transformations. J. Symb. Comput. 8, 101–140 (1989)MathSciNetCrossRef

89.

Steen, A.: Extensional paramodulation for Higher-Order logic and its effective implementation Leo-III, DISKI, vol. 345. Akademische Verlagsgesellschaft AKA GmbH, Berlin, : Dissertation. Freie Universität Berlin, Germany (2018)

90.

Steen, A., Benzmüller, C.: Sweet SIXTEEN: automation via embedding into classical higher-order logic. Logic Logical Philos. 25(4), 535–554 (2016)MathSciNetMATH

91.

Steen, A., Benzmüller, C.: The higher-order prover Leo-III. In: D. Galmiche, S. Schulz, R. Sebastiani (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as part of the federated logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, LNCS, vol. 10900, pp. 108–116. Springer (2018). https://doi.org/10.1007/978-3-319-94205-6_8

92.

Steen, A., Benzmüller, C.: On reductions of Hintikka sets for higher-Order logic. arXiv:2004.07506 (2020). arxiv.org/abs/2004.07506

93.

Steen, A., Wisniewski, M., Benzmüller, C.: Agent-based HOL reasoning. In: G. Greuel, T. Koch, P. Paule, A.J. Sommese (eds.) Mathematical Software - ICMS 2016 - 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, LNCS, vol. 9725, pp. 75–81. Springer (2016). https://doi.org/10.1007/978-3-319-42432-3_10

94.

Steen, A., Wisniewski, M., Benzmüller, C.: Going polymorphic - TH1 reasoning for Leo-III. In: T. Eiter, D. Sands, G. Sutcliffe, A. Voronkov (eds.) IWIL@LPAR 2017 Workshop and LPAR-21 short presentations, Maun, Botswana, May 7-12, 2017, Kalpa Publications in Computing, vol. 1. EasyChair (2017). https://doi.org/10.29007/jgkw

95.

Steen, A., Wisniewski, M., Schurr, H., Benzmüller, C.: Capability discovery for automated reasoning systems. In: T. Eiter, D. Sands, G. Sutcliffe, A. Voronkov (eds.) IWIL@LPAR 2017 Workshop and LPAR-21 Short presentations, Maun, Botswana, May 7-12, 2017, Kalpa Publications in Computing, vol. 1. EasyChair (2017). https://doi.org/10.29007/fsv3

96.

Sutcliffe, G.: Semantic derivation verification: techniques and implementation. Int. J. Artif. Intell. Tools 15(6), 1053–1070 (2006). https://doi.org/10.1142/S0218213006003119CrossRef

97.

Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: V. Diekert, M. Volkov, A. Voronkov (eds.) Proceedings of the 2nd International computer science Symposium in Russia, no. 4649 in lecture notes in computer science, pp. 7–23. Springer (2007)

98.

Sutcliffe, G.: The SZS Ontologies for automated reasoning software. In: LPAR Workshops: knowledge exchange: automated provers and proof assistants, and The 7th International Workshop on the Implementation of Logics (Doha, Qatar), vol. 418, pp. 38–49. CEUR Workshop Proceedings (2008)

99.

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)MathSciNetCrossRef

100.

Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1–27 (2010). https://doi.org/10.6092/issn.1972-5787/1710MathSciNetCrossRefMATH

101.

Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: N. Bjørner, A. Voronkov (eds.) Logic for programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7180, pp. 406–419. Springer (2012). https://doi.org/10.1007/978-3-642-28717-6_32

102.

Vukmirovic, P., Blanchette, J.C., Cruanes, S., Schulz, S.: Extending a brainiac prover to lambda-free higher-order logic. In: T. Vojnar, L. Zhang (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, Lecture Notes in Computer Science, vol. 11427, pp. 192–210. Springer (2019). https://doi.org/10.1007/978-3-030-17462-0_11

103.

Wand, D.: Superposition: Types and induction. (superposition: types et induction). Ph.D. thesis, Saarland University, Saarbrücken, Germany (2017)

104.

Wisniewski, M., Steen, A., Benzmüller, C.: LeoPARD - A generic platform for the implementation of higher-order reasoners. In: M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, V. Sorge (eds.) Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings, LNCS, vol. 9150, pp. 325–330. Springer (2015). https://doi.org/10.1007/978-3-319-20615-8_22

105.

Wisniewski, M., Steen, A., Benzmüller, C.: TPTP and beyond: Representation of quantified non-classical logics. In: C. Benzmüller, J. Otten (eds.) Proceedings of the 2nd International Workshop Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016)., Coimbra, Portugal, July 1, 2016., CEUR Workshop Proceedings, vol. 1770, pp. 51–65. CEUR-WS.org (2016)

106.

Wisniewski, M., Steen, A., Kern, K., Benzmüller, C.: Effective normalization techniques for HOL. In: N. Olivetti, A. Tiwari (eds.) Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, LNCS, vol. 9706, pp. 362–370. Springer (2016). https://doi.org/10.1007/978-3-319-40229-1_25

Title: Extensional Higher-Order Paramodulation in Leo-III
Authors: Alexander Steen
Christoph Benzmüller
Publication date: 27-03-2021
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 6/2021
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-021-09588-x

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner