Can a higher-order and a first-order theorem prover cooperate?

C Benzmuller, Volker Sorge, Mateja Jamnik, Manfred Kerber

Research output: Contribution to journalArticlepeer-review

5 Citations (Scopus)


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.
Original languageEnglish
Pages (from-to)415-431
Number of pages17
JournalLecture Notes in Computer Science
Publication statusPublished - 1 Jan 2005
Event11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR) -
Duration: 1 Jan 2005 → …


Dive into the research topics of 'Can a higher-order and a first-order theorem prover cooperate?'. Together they form a unique fingerprint.

Cite this