Combined reasoning by automated cooperation

• Published in: Journal of applied logic 2008-09, Vol.6 (3), p.318-342
• Main Authors: Benzmüller, Christoph, Sorge, Volker, Jamnik, Mateja, Kerber, Manfred
• Format: Article
• Language: English
• Subjects: Agent architecture; Automated reasoning; Computer algebra; Higher-order and first-order proving; Model generators; System integration
• ISSN: 1570-8683; 1570-8691
• DOI: 10.1016/j.jal.2007.06.003

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. Of particular interest is the integration of first-order and higher-order techniques. First-order reasoning systems, on the one hand, have reached considerable strength in some niches, but in many areas of mathematics they still cannot reliably solve relatively simple problems, for example, when reasoning about sets, relations, or functions. Higher-order reasoning systems, on the other hand, can solve problems of this kind automatically. But the complexity inherent in their calculi prevents them from solving a whole range of problems. However, while many problems cannot be solved by any one system alone, they can be solved by a combination of these systems. We present a general agent-based methodology for integrating different reasoning systems. It provides a generic integration framework which facilitates the cooperation between diverse reasoners, but can also be refined to enable more efficient, specialist integrations. We empirically evaluate its usefulness, effectiveness and efficiency by case studies involving the integration of first-order and higher-order automated theorem provers, computer algebra systems, and model generators.