Abstract
State-of-the-art first-order automated theorem proving systems have reached considerable strength over recent years. However, in many areas of mathematics they are still a long way from reliably proving theorems that would be considered relatively simple by humans. For example, when reasoning about sets, relations, or functions, first-order systems still exhibit serious weaknesses. While it has been shown in the past that higher-order reasoning systems can solve problems of this kind automatically, the complexity inherent in their calculi and their inefficiency in dealing with large numbers of clauses prevent these systems from solving a whole range of problems.
We present a solution to this challenge by combining a higher-order and a first-order automated theorem prover, both based on the resolution principle, in a flexible and distributed environment. By this we can exploit concise problem formulations without forgoing efficient reasoning on first-order subproblems. We demonstrate the effectiveness of our approach on a set of problems still considered non-trivial for many first-order theorem provers.
This work was supported by EPSRC grant GR/M22031 and DFG-SFB 378 (first author), EU Marie-Curie-Fellowship HPMF-CT-2002-01701 (second author), and EPSRC Advanced Research Fellowship GR/R76783 (third author).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Andrews, P.: An Introduction to mathematical logic and Type Theory: To Truth through Proof. Applied Logic Series, vol. 27. Kluwer, Dordrecht (2002)
Benzmüller, C.: Equality and Extensionality in Higher-Order Theorem Proving. PhD thesis, Universität des Saarlandes, Germany (1999)
Benzmüller, C.: Extensional higher-order paramodulation and RUE-resolution. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 399–413. Springer, Heidelberg (1999)
Benzmüller, C.: Comparing approaches to resolution based higher-order theorem proving. Synthese 133(1-2), 203–235 (2002)
Benzmüller, C., Jamnik, M., Kerber, M., Sorge, V.: 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., Kohlhase, M.: LEO – a higher-order theorem prover. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, p. 139. Springer, Heidelberg (1998)
Benzmüller, C., Sorge, V.: A Blackboard Architecture for Guiding Interactive Proofs. In: Giunchiglia, F. (ed.) AIMSA 1998. LNCS (LNAI), vol. 1480, pp. 102–114. Springer, Heidelberg (1998)
Benzmüller, C., Sorge, V.: Oants – An open approach at combining Interactive and Automated Theorem Proving. In: Proc. of Calculemus-2000, AK Peters (2001)
Bishop, M., Andrews, P.: Selectively instantiating definitions. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, p. 365. Springer, Heidelberg (1998)
Brown, C.E.: Set Comprehension in Church’s Type Theory. PhD thesis, Dept. of Mathematical Sciences, Carnegie Mellon University, USA (2004)
de Nivelle, H.: The Bliksem Theorem Prover, Version 1.12. Max-Planck-Institut, Saarbrücken, Germany (1999), http://www.mpi-sb.mpg.de/bliksem/manual.ps
Denzinger, J., Fuchs, D.: Cooperation of Heterogeneous Provers. In: Proc. IJCAI-16, pp. 10–15. Morgan Kaufmann, San Francisco (1999)
Fisher, M., Ireland, A.: Multi-agent proof-planning. In: CADE-15 Workshop “Using AI methods in Deduction” (1998)
Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 335–349. Springer, Heidelberg (2003)
Hurd, J.: An LCF-style interface between HOL and first-order logic. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 134–138. Springer, Heidelberg (2002)
Kerber, M.: On the Representation of Mathematical Concepts and their Translation into First Order Logic. PhD thesis, Universität Kaiserslautern, Germany (1992)
Meier, A.: TRAMP: Transformation ofMachine-Found Proofs into Natural Deduction Proofs at the Assertion Level. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, Springer, Heidelberg (2000)
Meng, J., Paulson, L.C.: Experiments on supporting interactive proof using resolution. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 372–384. Springer, Heidelberg (2004)
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)
Pastre, D.: Muscadet2.3: A knowledge-based theorem prover based on natural deduction. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 685–689. Springer, Heidelberg (2001)
Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 376–380. Springer, Heidelberg (2001)
Sorge, V.: OANTS: A Blackboard Architecture for the Integration of Reasoning Techniques into Proof Planning. PhD thesis, Universität des Saarlandes, Germany (2001)
Stenz, G., Wolf, A.: E-SETHEO: An Automated3 Theorem Prover – System Abstract. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol. 1847, pp. 436–440. Springer, Heidelberg (2000)
Sutcliffe, G., Suttner, C.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning 21(2), 177–203 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benzmüller, C., Sorge, V., Jamnik, M., Kerber, M. (2005). Can a Higher-Order and a First-Order Theorem Prover Cooperate?. In: Baader, F., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2005. Lecture Notes in Computer Science(), vol 3452. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32275-7_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-32275-7_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25236-8
Online ISBN: 978-3-540-32275-7
eBook Packages: Computer ScienceComputer Science (R0)