Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Extensional Higher-Order Paramodulation in Leo-III

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. 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.

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

  3. 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.

  4. 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).

  5. 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.

  6. 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.

  7. 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 }\).

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

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

  10. 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.

  11. 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.

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

References

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

  6. 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

  7. 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.002

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  9. 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.217

    Article  MathSciNet  MATH  Google Scholar 

  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/2269159

    Article  MathSciNet  MATH  Google Scholar 

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

    Book  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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-0

    Article  MathSciNet  MATH  Google Scholar 

  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.008

    Article  Google Scholar 

  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/1102022211

    Article  MathSciNet  MATH  Google Scholar 

  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  Google Scholar 

  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/jzp080

    Article  MathSciNet  MATH  Google Scholar 

  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-y

    Article  MathSciNet  MATH  Google Scholar 

  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-y

    Article  MathSciNet  MATH  Google Scholar 

  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-9

    Article  MATH  Google Scholar 

  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)

    Google Scholar 

  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  Google Scholar 

  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  Google Scholar 

  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-5

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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.639

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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:1005879229581

    Article  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

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

    MATH  Google Scholar 

  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/2266967

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  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.2756

    Article  MathSciNet  MATH  Google Scholar 

  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-0015

    Article  Google Scholar 

  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-y

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  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.497

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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  Google Scholar 

  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  Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

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

    MATH  Google Scholar 

  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.008

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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)

    MathSciNet  MATH  Google Scholar 

  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/S0218213006003119

    Article  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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/1710

    Article  MathSciNet  MATH  Google Scholar 

  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

Download references

Author information

Authors and Affiliations

  1. University of Luxembourg, FSTM, Esch-sur-Alzette, Luxembourg

    Alexander Steen & Christoph Benzmüller

  2. Department of Mathematics and Computer Science, Freie Universität Berlin, Berlin, Germany

    Christoph Benzmüller

Authors
  1. Alexander Steen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christoph Benzmüller
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexander Steen.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This work has been supported by the DFG under Grant BE 2501/11-1 (Leo-III) and by the Volkswagenstiftung (“Consistent Rational Argumentation in Politics”).

Leo-III Proof of Fig. 7

Leo-III Proof of Fig. 7

figure e

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Steen, A., Benzmüller, C. Extensional Higher-Order Paramodulation in Leo-III. J Autom Reasoning 65, 775–807 (2021). https://doi.org/10.1007/s10817-021-09588-x

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-021-09588-x

Keywords

Search

Navigation