Combined Reasoning by Automated Cooperation

Different reasoning systems have different strengths and weaknesses, and often it is useful to combine these systems to gain as much as possible from their strengths and retain as little as possible from their weaknesses. Important examples of this include the relationship between first-order and higher-order automated theorem provers, between automated theorem provers and computer algebra systems, and between theorem provers and model generators. We present a general agent-based methodology for integrating such different reasoning systems, and empirically evaluate its usefulness, effectiveness and efficiency by case studies. Of particular interest is the integration of higher-order and first-order automated theorem provers. Namely, first-order automated theorem proving systems have reached considerable strength, but 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. While our framework is general enough to facilitate cooperation of first-order and higher-order automated theorem provers, we also present a refinement of the general approach that enables a more efficient integration