×

zbMATH — the first resource for mathematics

The higher-order prover Leo-II. (English) Zbl 1356.68176
Summary: Leo-II is an automated theorem prover for classical higher-order logic. The prover has pioneered cooperative higher-order-first-order proof automation, it has influenced the development of the TPTP THF infrastructure for higher-order logic, and it has been applied in a wide array of problems. Leo-II may also be called in proof assistants as an external aid tool to save user effort. For this it is crucial that Leo-II returns proof information in a standardised syntax, so that these proofs can eventually be transformed and verified within proof assistants. Recent progress in this direction is reported for the Isabelle/HOL system.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Álvez, J; Lucio, P; Rigau, G, Adimen-SUMO: reengineering an ontology for first-order reasoning, Int. J. Semantic Web Inf. Syst., 8, 80-116, (2012)
[2] Andrews, PB, On connections and higher order logic, J. Autom. Reason., 5, 257-291, (1989) · Zbl 0694.03011
[3] Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Applied Logic Series, vol. 27. Springer, Berlin (2002) · Zbl 1002.03002
[4] Andrews, PB; Bishop, M; Issar, S; Nesmith, D; Pfenning, F; Xi, H, TPS: a theorem-proving system for classical type theory, J. Autom. Reason., 16, 321-353, (1996) · Zbl 0858.03017
[5] Backes, J; Brown, CE, Analytic tableaux for higher-order logic with choice, J. Autom. Reason., 47, 451-479, (2011) · Zbl 1258.03019
[6] Benzmüller, C.: A calculus and a system architecture for extensional higher-order resolution. Research Report 97-198, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, USA (1997)
[7] Benzmüller, C.: Extensional higher-order paramodulation and RUE-resolution. In: Ganzinger, H. (ed.) Automated Deduction—CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, no. 1632 in LNCS, pp. 399-413. Springer (1999). doi:10.1007/3-540-48660-7_39 · Zbl 0781.68101
[8] Benzmüller, C, Comparing approaches to resolution based higher-order theorem proving, Synthese, 133, 203-235, (2002) · Zbl 1020.03011
[9] Benzmüller, C.: Automating access control logic in simple type theory with LEO-II. In: Gritzalis, D., López, J. (eds.) Emerging Challenges for Security, Privacy and Trust, 24th IFIP TC 11 International Information Security Conference, SEC 2009, Pafos, Cyprus, May 18-20, 2009. Proceedings, IFIP, vol. 297, pp. 387-398. Springer (2009). doi:10.1007/978-3-642-01244-0_34 · Zbl 1020.68084
[10] Benzmüller, C, Combining and automating classical and non-classical logics in classical higher-order logic, Ann. Math. Artif. Intell. (CLIMA XI), 62, 103-128, (2011) · Zbl 1252.03025
[11] Benzmüller, C.: Automating quantified conditional logics in HOL. In: Rossi, F. (ed.) 23rd International Joint Conference on Artificial Intelligence (IJCAI-13), pp. 746-753. Beijing, China (2013a)
[12] Benzmüller, C.: A top-down approach to combining logics. In: Proceedings of the 5th International Conference on Agents and Artificial Intelligence (ICAART), pp. 346-351. SciTePress Digital Library, Barcelona (2013b). doi:10.5220/0004324803460351 · Zbl 0332.02035
[13] Benzmüller, C; Delahaye, D (ed.); Woltzenlogel Paleo, B (ed.), Higher-order automated theorem provers, 171-214, (2015), London
[14] Benzmüller, C., Brown, C.: A structured set of higher-order problems. In: Hurd, J., Melham, T.F. (eds.) Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, Springer, no. 3603 in LNCS, pp. 66-81 (2005). doi:10.1007/11541868_5
[15] Benzmüller, C., Brown, C.: The curious inference of Boolos in MIZAR and OMEGA. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof - Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric, vol. 10(23), pp. 299-388. The University of Bialystok, Polen (2007)
[16] Benzmüller, C., Kohlhase, M.: LEO—a higher-order theorem prover. In: Kirchner, C., Kirchner, H. (eds), Automated Deduction—CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings, Springer, no. 1421 in LNCS, pp. 139-143 (1998). doi:10.1007/BFb0054256 · Zbl 0253.68007
[17] Benzmüller, C; Paulson, L, Multimodal and intuitionistic logics in simple type theory, Logic J. IGPL, 18, 881-892, (2010) · Zbl 1222.03023
[18] Benzmüller, C; Paulson, L, Quantified multimodal logics in simple type theory, Logica Universalis, 7, 7-20, (2013) · Zbl 1334.03014
[19] Benzmüller, C., Sultana, N.: LEO-II version 1.5. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013, EasyChair, EPiC Series, vol. 14, pp. 2-10 (2013)
[20] Benzmüller, C., Sultana, N.: Update report: LEO-II version 1.5. CoRR abs/1303.3761 (2013)
[21] Benzmüller, C., Woltzenlogel Paleo, B.: Formalization, mechanization and automation of Gödel’s proof of God’s existence (2013). arXiv:1308.4526 · Zbl 1071.03024
[22] Benzmüller, C., Woltzenlogel Paleo, B.: Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers. In: Schaub, T., Friedrich, G., O’Sullivan, B. (eds.) ECAI 2014, IOS Press, Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 93-98 (2014). doi:10.3233/978-1-61499-419-0-93 · Zbl 1366.03169
[23] Benzmüller, C., Woltzenlogel Paleo, B.: Higher-order modal logics: Automation and applications. In: Paschke, A., Faber, W. (eds.) Reasoning Web 2015, no. 9203 in LNCS, pp. 1-43. Springer, Berlin (2015). doi:10.1007/978-3-319-21768-0_2 · Zbl 1162.68646
[24] Benzmüller, C., Ziener, M.: Automated consistency checking of expressive ontologies—beware of the wrong interpretation of success!. In: Fink, M., Homola, M., Mileo, A., Varzinczak, I.J. (eds.) The 5th International Workshop on Acquisition, Representation and Reasoning with Contextualized Knowledge (ARCOE-LogIC 2013). Corunna, Spain (2013)
[25] Benzmüller, C; Brown, C; Kohlhase, M, Higher-order semantics and extensionality, J. Symb. Log., 69, 1027-1088, (2004) · Zbl 1071.03024
[26] Benzmüller, C; Sorge, V; Jamnik, M; Kerber, M, Combined reasoning by automated cooperation, J. Appl. Log., 6, 318-342, (2008) · Zbl 1162.68646
[27] Benzmüller, C; Brown, C; Kohlhase, M, Cut-simulation and impredicativity, Log. Methods Comput. Sci., 5, 1-21, (2009) · Zbl 1160.03004
[28] Benzmüller, C; Weber, L; Woltzenlogel Paleo, B; Silvestre, RS (ed.); Béziau, JY (ed.), Computer-assisted analysis of the Anderson-Hájek ontological controversy, 53-54, (2015), Brasil
[29] Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S.A. (eds.) Proceedings of TACAS 2013, LNCS, vol. 7795, pp. 493-507. Springer (2013). doi:10.1007/978-3-642-36742-7_34 · Zbl 1381.68259
[30] Brown, C.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning (IJCAR 2012), LNCS, vol. 7364, pp. 111-117. Springer, Berlin (2012). doi:10.1007/978-3-642-31365-3_11 · Zbl 1358.68250
[31] Bruijn, N, 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
[32] Claessen, K., Lillieström, A., Smallbone, N.: Sort it out with monotonicity. In: Proceedings of CADE-23, LNAI, vol. 6803, pp. 207-221. Springer (2011) · Zbl 1341.03017
[33] Digricoli, VJ; Harrison, MC, Equality-based binary resolution, J ACM, 33, 253-289, (1986)
[34] Gordon, M., Melham, T.: Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993) · Zbl 0779.68007
[35] Hales, T: Mathematics in the Age of the Turing Machine. ArXiv e-prints arXiv:1302.2898 (2013) · Zbl 1252.03025
[36] Harrison, J.: HOL Light: An overview. In: Proceedings of TPHOLs 2009, LNCS, vol. 5674, pp. 60-66. Springer (2009) · Zbl 1252.68255
[37] Huet, G.: A complete mechanization of type theory. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence , pp. 139-146 (1973a)
[38] Huet, G, A unification algorithm for typed lambda-calculus, Theor. Comput. Sci., 1, 27-57, (1975) · Zbl 0332.02035
[39] Huet, G.P.: Constrained resolution: a complete method for higher order logic. Ph.D. thesis, Case Western Reserve University (1972)
[40] Huet, G.P.: A mechanization of type theory. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence, pp. 139-146 (1973b) · Zbl 0858.03017
[41] Kaliszyk, C; Urban, J, Learning-assisted automated reasoning with flyspeck, J. Autom. Reason., 53, 173-213, (2014) · Zbl 1314.68283
[42] McCune, W, Experiments with discrimination-tree indexing and path indexing for term retrieval, J. Autom. Reason., 9, 147-167, (1992) · Zbl 0781.68101
[43] Miller, D.: Proofs in higher-order logic. Ph.D. thesis, Carnegie Mellon University (1983)
[44] Mints, G, Cut-elimination for simple type theory with an axiom of choice, J. Symb. Log., 64, 479-485, (1999) · Zbl 0930.03080
[45] Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, Hets. In: Proceedings of TACAS 2007, LNCS, vol. 4424, pp. 519-522. Springer (2007) · Zbl 1258.03019
[46] Nieuwenhuis, R., Hillenbrand, T., Riazanov, A., Voronkov, A.: On the evaluation of indexing techniques for theorem proving. In: Proceedings of IJCAR-01, LNAI, vol. 2083, pp. 257-271. Springer (2001) · Zbl 0988.68595
[47] Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. No. 2283 in LNCS. Springer (2002) · Zbl 0994.68131
[48] Pease, A; Benzmüller, C, Sigma: an integrated development environment for formal ontology, AI Commun., 26, 79-97, (2013)
[49] Pease, A., Sutcliffe, G.: First order reasoning on a large ontology. In: Urban, J., Sutcliffe, G., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, no. 257 in CEUR Workshop Proceedings, pp. 59-69 (2007)
[50] Pientka, B.: Higher-order substitution tree indexing. In: Palamidessi, C. (ed.) Proceedings of ICLP 2003, LNCS, vol. 2916, pp. 377-391. Springer (2003) · Zbl 1204.68060
[51] Riazanov, A; Voronkov, A, The design and implementation of VAMPIRE, AI Commun., 15, 91-110, (2002) · Zbl 1021.68082
[52] Schulz, S, E - A brainiac theorem prover, AI Commun., 15, 111-126, (2002) · Zbl 1020.68084
[53] Siekmann, J; Benzmüller, C; Autexier, S, Computer supported mathematics with OMEGA, J. Appl. Log., 4, 533-559, (2006) · Zbl 1107.68101
[54] Sobel, J.: Logic and Theism: Arguments for and Against Beliefs in God, Cambridge U. Press, chap Appendix B. Notes in Dana Scott’s Hand, pp. 145-146 (2004a)
[55] Sobel, J.: Logic and Theism: Arguments for and Against Beliefs in God, Cambridge U. Press, chap Appendix A. Notes in Kurt Gödel’s Hand, pp. 144-145 (2004b)
[56] Stalnaker, R.: A theory of conditionals. In: Studies in Logical Theory, Oxford, pp. 98-112 (1968)
[57] Stickel, M.: The path-indexing method for indexing terms. Tech. Rep. 473, Artificial Intelligence Center, SRI International, 333 Ravenswood Ave., Menlo Park, CA 94025 (1989) · Zbl 1107.68101
[58] Sultana, N.: Higher-order proof translation. Ph.D. thesis, Computer Laboratory, University of Cambridge, Available as Tech Report UCAM-CL-TR-867 (2015) · Zbl 1372.65041
[59] Sultana, N., Benzmüller, C.: Understanding LEO-II’s proofs. In: Korovin, K., Schulz, S., Ternovska, E. (eds.) IWIL 2012, EasyChair, Merida, Venezuela, EPiC Series, vol. 22, pp. 33-52 (2013) · Zbl 1160.03004
[60] Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M., Voronkov, A. (eds.) Proceedings of the 2nd International Computer Science Symposium in Russia, pp. 7-23. Springer, LNCS (2007)
[61] Sutcliffe, G.: The SZS ontologies for automated reasoning software. In: LPAR Workshops, CEUR Workshop Proceedings (http://ceur-ws.org/), vol. 418 (2008)
[62] Sutcliffe, G, The TPTP problem library and associated infrastructure, J. Autom. Reason., 43, 337-362, (2009) · Zbl 1185.68636
[63] Sutcliffe, G.: The TPTP World—Infrastructure for Automated Reasoning. In: Proceedings of LPAR-16, no. 6355 in LNAI, pp. 1-12. Springer (2010) · Zbl 1253.68292
[64] Sutcliffe, G; Benzmüller, C, Automated reasoning in higher-order logic using the TPTP THF infrastructure, J. Formaliz. Reason., 3, 1-27, (2010) · Zbl 1211.68371
[65] Theiß, F., Benzmüller, C.: Term indexing for the LEO-II prover. In: IWIL-6 workshop at LPAR, : The 6th International Workshop on the Implementation of Logics. Pnom Penh, Cambodia (2006) · Zbl 1185.68636
[66] Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D.: Spass version 2.0. In: Voronkov, A. (ed) Proceedings of CADE 2002, LNCS, vol. 2392, pp. 275-279. Springer (2002) · Zbl 1072.68596
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.