×

Extensional higher-order paramodulation in Leo-III. (English) Zbl 07432187

Summary: 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.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI arXiv

References:

[1] Abadi, M.; Cardelli, L.; Curien, P.; Lévy, J., Explicit substitutions, J. Funct. Program., 1, 4, 375-416 (1991) · Zbl 0941.68542
[2] Andrews, PB, Resolution in type theory, J. Symb. Log., 36, 3, 414-432 (1971) · Zbl 0231.02038
[3] Andrews, PB, General models and extensionality, J. Symb. Log., 37, 2, 395-397 (1972) · Zbl 0264.02050
[4] Andrews, PB, General models, descriptions, and choice in type theory, J. Symb. Log., 37, 2, 385-394 (1972) · Zbl 0264.02049
[5] Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory. Springer, Applied Logic Series (2002) · Zbl 1002.03002
[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). doi:10.1007/10721959_11 · Zbl 0963.68530
[7] Andrews, PB; Brown, CE, TPS: a hybrid automatic-interactive system for developing proofs, J. Appl. Logic, 4, 4, 367-395 (2006) · Zbl 1107.68091
[8] Andrews, PB; Miller, DA; Cohen, EL; Pfenning, F., Automating higher-order logic, Contemp. Math., 29, 169-192 (1984)
[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). doi: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) · Zbl 0814.68117
[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). doi:10.1007/978-3-030-29436-6_3 · Zbl 07178968
[12] Barcan, RC, A functional calculus of first order based on strict implication, J. Symb. Log., 11, 1, 1-16 (1946) · Zbl 0063.00205
[13] Barendregt, HP; Dekkers, W.; Statman, R., Lambda Calculus with Types. Perspectives in logic (2013), Cambridge: Cambridge University Press, Cambridge
[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). doi: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). doi:10.1007/978-3-030-29436-6_4 · Zbl 1471.03014
[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). doi:10.1007/978-3-319-94205-6_3 · Zbl 06958090
[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). doi:10.1007/3-540-48660-7_39 · Zbl 0937.03013
[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) · Zbl 1252.03025
[20] Benzmüller, C., Cut-elimination for quantified conditional logic, J. Philos. Logic, 46, 3, 333-353 (2017) · Zbl 1417.03282
[21] Benzmüller, C., Universal (meta-)logical reasoning: recent successes, Sci. Comput. Prog., 172, 48-62 (2019)
[22] Benzmüller, C.; Brown, CE; Kohlhase, M., Higher-order semantics and extensionality, J. Symb. Log., 69, 4, 1027-1088 (2004) · Zbl 1071.03024
[23] Benzmüller, C., Brown, C.E., Kohlhase, M.: Cut-simulation and impredicativity. Logical Methods Comput. Sci. 5(1), (2009) · Zbl 1160.03004
[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) · Zbl 1418.03069
[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). doi:10.1007/BFb0054256
[26] Benzmüller, C.; Miller, D.; Siekmann, JH, Automation of higher-order logic, Computational Logic, Handbook of the History of Logic (2014), Amsterdam: Elsevier, Amsterdam · Zbl 1404.03005
[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). doi:10.3233/978-1-61499-098-7-163 · Zbl 1327.68204
[28] Benzmüller, C.; Paulson, LC, Multimodal and intuitionistic logics in simple type theory, Logic J. IGPL, 18, 6, 881-892 (2010) · Zbl 1222.03023
[29] Benzmüller, C.; Paulson, LC, Quantified multimodal logics in simple type theory, Logica Univ., 7, 1, 7-20 (2013) · Zbl 1334.03014
[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). doi:10.1007/978-3-642-45221-5_9 · Zbl 1406.68103
[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). doi:10.1007/978-3-319-42432-3_6 · Zbl 1434.68638
[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). doi:10.29007/grmx
[33] Benzmüller, C.; Sultana, N.; Paulson, LC; Theiss, F., The higher-order prover LEO-II, J. Autom. Reason., 55, 4, 389-404 (2015) · Zbl 1356.68176
[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) · Zbl 1417.03131
[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. (2004), Berlin: Springer, Berlin · Zbl 1069.68095
[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). doi:10.1007/978-3-030-29436-6_5 · Zbl 07178970
[40] Blackburn, P.; van Benthem, JF; Wolter, F., Handbook of modal logic (2006), Amsterdam: Elsevier, Amsterdam · Zbl 1114.03001
[41] Blanchette, JC; Böhme, S.; Paulson, LC, Extending Sledgehammer with SMT solvers, J. Autom. Reason., 51, 1, 109-128 (2013) · Zbl 1314.68272
[42] Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Logical methods in computer science 12(4), (2016). doi:10.2168/LMCS-12(4:13)2016 · Zbl 1445.68327
[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). doi:10.1007/978-3-642-14052-5_11 · Zbl 1291.68326
[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). doi:10.1007/978-3-642-38574-2_29 · Zbl 1381.68260
[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). doi: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). doi:10.1007/978-3-642-31365-3_11 · Zbl 1358.68250
[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). doi:10.1007/978-3-030-29436-6_8 · Zbl 07178973
[49] Bruijn, NGD, 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) · Zbl 0253.68007
[50] Cervesato, I.; Pfenning, F., A linear spine calculus, J. Log. Comput., 13, 5, 639-688 (2003) · Zbl 1041.03007
[51] Church, A., A formulation of the simple theory of types, J. Symb. Log., 5, 2, 56-68 (1940) · JFM 66.1192.06
[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). doi:10.1007/978-3-540-73595-3_18 · Zbl 1213.68568
[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)
[55] Digricoli, VJ; Harrison, MC, Equality-based binary resolution, J. ACM, 33, 2, 253-289 (1986)
[56] Frege, G., Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens (1879), Halle: Verlag von Louis Nebert, Halle
[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). doi: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). doi:10.29007/jsb9 · Zbl 1403.68225
[60] Goldfarb, WD, The undecidability of the second-order unification problem, Theor. Comput. Sci., 13, 2, 225-230 (1981) · Zbl 0457.03006
[61] Gordon, MJ; Melham, TF, Introduction to HOL A Theorem Proving Environment for Higher Order Logic (1993), Cambridge: Cambridge University Press, Cambridge · Zbl 0779.68007
[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). doi:10.1007/978-3-642-03359-9_4 · Zbl 1252.68255
[64] Henkin, L., Completeness in the theory of types, J. Symb. Log., 15, 2, 81-91 (1950) · Zbl 0039.00801
[65] Huet, GP, The undecidability of unification in third order logic, Inf. control, 22, 3, 257-267 (1973) · Zbl 0257.02038
[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). doi:10.1007/10722086_7 · Zbl 0963.68522
[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, AJ; Rocca, SRD; Tiuryn, J.; Urzyczyn, P., Alpha-conversion and typability, Inf. Comput., 150, 1, 1-21 (1999) · Zbl 1004.03005
[69] Kirchner, D.; Benzmüller, C.; Zalta, EN, Computer science and metaphysics: a cross-fertilization, Open Philos., 2, 1, 230-251 (2019)
[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). doi:10.1007/978-3-540-71070-7_24 · Zbl 1165.68462
[71] Leibniz, G.W.: Discourse on metaphysics. In: L.E. Loemker (ed.) Philosophical Papers and Letters, pp. 303-330. Springer Netherlands, Dordrecht (1989). doi: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). doi:10.1007/978-3-319-08587-6_5 · Zbl 1423.68421
[73] Meng, J.; Paulson, LC, Translating higher-order clauses to first-order clauses, J. Autom. Reasoning, 40, 1, 35-60 (2008) · Zbl 1203.68188
[74] Meng, J.; Paulson, LC, Lightweight relevance filtering for machine-generated resolution problems, J. Appl. Logic, 7, 1, 41-57 (2009) · Zbl 1183.68560
[75] Miller, D.A.: Proofs in higher-order logic. Ph.D. thesis, Carnegie-Mellon University (1983)
[76] Miller, DA, A logic programming language with lambda-abstraction, function variables, and simple unification, J. Log. Comput., 1, 4, 497-536 (1991) · Zbl 0738.68016
[77] Muskens, R., Intensional models for the theory of types, J. Symb. Log., 72, 1, 98-118 (2007) · Zbl 1116.03008
[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). doi:10.1007/3-540-55602-8_186 · Zbl 0925.03076
[79] Nipkow, T.; Paulson, LC; Wenzel, M., Isabelle/HOL - A Proof Assistant for Higher-Order Logic (2002), Berlin: Springer, Berlin · Zbl 0994.68131
[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). doi:10.1007/978-3-319-08587-6_20 · Zbl 1423.68423
[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). doi: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). doi:10.1007/978-3-642-31365-3_35 · Zbl 1358.68262
[83] Riazanov, A.; Voronkov, A., The design and implementation of VAMPIRE, AI Commun., 15, 2-3, 91-110 (2002) · Zbl 1021.68082
[84] Robinson, G.; Wos, L., Paramodulation and theorem-proving in first-order theories with equality, Mach. Intell., 4, 135-150 (1969) · Zbl 0219.68047
[85] Schulz, S., E-A Brainiac theorem prover, AI Commun., 15, 3, 111-126 (2002) · Zbl 1020.68084
[86] Siekmann, JH; Benzmüller, C.; Autexier, S., Computer supported mathematics with \(\Omega\) MEGA, J. Appl. Logic, 4, 4, 533-559 (2006) · Zbl 1107.68101
[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). doi:10.1007/978-3-540-71067-7_6 · Zbl 1165.68474
[88] Snyder, W.; Gallier, J., Higher-Order unification revisited: complete sets of transformations, J. Symb. Comput., 8, 101-140 (1989) · Zbl 0682.03034
[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) · Zbl 1402.68013
[90] Steen, A.; Benzmüller, C., Sweet SIXTEEN: automation via embedding into classical higher-order logic, Logic Logical Philos., 25, 4, 535-554 (2016) · Zbl 1373.03030
[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). doi:10.1007/978-3-319-94205-6_8 · Zbl 06958095
[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). doi:10.1007/978-3-319-42432-3_10 · Zbl 1434.68646
[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). doi: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). doi:10.29007/fsv3
[96] Sutcliffe, G., Semantic derivation verification: techniques and implementation, Int. J. Artif. Intell. Tools, 15, 6, 1053-1070 (2006)
[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) · Zbl 1425.68381
[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) · Zbl 1211.68371
[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). doi:10.1007/978-3-642-28717-6_32 · Zbl 1352.68217
[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). doi: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). doi:10.1007/978-3-319-20615-8_22 · Zbl 1417.68196
[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). doi:10.1007/978-3-319-40229-1_25 · 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.