Abstract
LEO-II is a standalone, resolution-based higher-order theorem prover designed for effective cooperation with specialist provers for natural fragments of higher-order logic. At present LEO-II can cooperate with the first-order automated theorem provers E, SPASS, and Vampire. The improved performance of LEO-II, especially in comparison to its predecessor LEO, is due to several novel features including the exploitation of term sharing and term indexing techniques, support for primitive equality reasoning, and improved heuristics at the calculus level. LEO-II is implemented in Objective Caml and its problem representation language is the new TPTP THF language.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Andrews, P.B., Brown, C.E.: TPS: A hybrid automatic-interactive system for developing proofs. J. Applied Logic 4(4), 367–395 (2006)
Beeson, M.: Mathematical induction in Otter-Lambda. J. Autom. Reasoning 36(4), 311–344 (2006)
Benzmüller, C.: Equality and Extensionality in Automated Higher-Order Theorem Proving. PhD thesis, Saarlandes University (1999)
Benzmüller, C., Kohlhase, M.: LEO – a higher-order theorem prover. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 139–143. Springer, Heidelberg (1998)
Benzmüller, C., Paulson, L.: Festschrift in Honour of Peter B. Andrews on his 70th Birthday. In: Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. IFCoLog (to appear, 2007)
Benzmüller, C., Paulson, L., Theiss, F., Fietzke, A.: Progress report on LEO-II – an automatic theorem prover for higher-order logic. In: TPHOLs 2007 Emerging Trends Proc., Internal Report 364/07, Department of Computer Science, University Kaiserslautern, Germany, pp. 33–48 (2007)
Benzmüller, C., Rabe, F., Sutcliffe, G.: THF0 — the core TPTP language for classical higher-order logic. In: Proc (IJCAR 2008). LNCS, vol. 5195. Springer, Heidelberg (2008)
Benzmüller, C., Sorge, V., Jamnik, M., Kerber, M.: Experiments with an Agent-Oriented Reasoning System. In: Baader, F., Brewka, G., Eiter, T. (eds.) KI 2001. LNCS (LNAI), vol. 2174, pp. 409–424. Springer, Heidelberg (2001)
Benzmüller, C., Sorge, V., Jamnik, M., Kerber, M.: Combined reasoning by automated cooperation. J. Applied Logic (in print) (2008)
Bishop, M., Andrews, P.B.: Selectively instantiating definitions. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 365–380. Springer, Heidelberg (1998)
Brown, C.E.: Solving for Set Variables in Higher-Order Theorem Proving. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 408–422. Springer, Heidelberg (2002)
de Bruijn, N.G.: Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math. 34(5), 381–392 (1972)
Gordon, M.J., Melham, T.F.: Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)
Kerber, M.: On the Representation of Mathematical Concepts and their Translation into First-Order Logic. PhD thesis, Univ. Kaiserslautern, Germany (1992)
Klein, L.: Indexing für Terme höherer Stufe. Master’s thesis, Saarland Univ. (1997)
McCune, W.: Experiments with discrimination-tree indexing and path indexing for term retrieval. J. Automated Reasoning 9(2), 147–167 (1992)
Nieuwenhuis, R., Hillenbrand, T., Riazanov, A., Voronkov, A.: On the evaluation of indexing techniques for theorem proving. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 257–271. Springer, Heidelberg (2001)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Pientka, B.: Higher-order substitution tree indexing. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol. 2916, pp. 377–391. Springer, Heidelberg (2003)
Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AICOM 15(2-3), 91–110 (2002)
Schulz, S.: E – A Brainiac Theorem Prover. J. AI Communications 15(2/3), 111–126 (2002)
Siekmann, J., Benzmüller, C., Autexier, S.: Computer supported mathematics with OMEGA. J. Applied Logic 4(4), 533–559 (2006)
Stickel, M.: The path-indexing method for indexing terms. Technical Report 473, Artificial Intelligence Center, SRI International, USA (1989)
Theiss, F., Benzmüller, C.: Term indexing for the LEO-II prover. In: Proc. of the 6th International Workshop on the Implementation of Logics. CEUR Workshop Proc., vol. 212 (2006)
Weidenbach, C., et al.: Spass version 2.0. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 275–279. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benzmüller, C., Paulson, L.C., Theiss, F., Fietzke, A. (2008). LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds) Automated Reasoning. IJCAR 2008. Lecture Notes in Computer Science(), vol 5195. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71070-7_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-71070-7_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71069-1
Online ISBN: 978-3-540-71070-7
eBook Packages: Computer ScienceComputer Science (R0)