Omega-ants: A blackboard architecture for the integration of reasoning techniques into proof planning

Abstract

Many automated reasoning systems and techniques have been developed for theo- rem proving for specific mathematical domains. Automated theorem provers and interactive systems for various calculi as well as proof planners have all had some success in limited areas. However, in many challenging interesting domains there is no single system available that has achieved a degree of reliability such that one can be certain this system can solve all problems for such a domain. Therefore, there have been many attempts at combining systems and reasoning techniques over the last decade. In particular, there have been attempts at integrating homogeneous and heterogeneous theorem provers,incorporating decision procedures and symbolic computation, and parallelization of theorem proving. This thesis presents both novel way of combining reasoning techniques and also the application of these combined techniques to proof planning for group theory and finite algebra. In particular, we combine interactive and automated reasoning, proof planning and symbolic computation. Our means to achieve this combination is a hierarchical blackboard architecture called Omega-Ants. This architecture was orig- inally developed to support the user in interactive theorem proving by searching for possible next proof steps in-between user interactions. It consists of two layers of blackboards with individual concurrent knowledge sources. The lower layer searches for instantiations of inference rule parameters within the actual proof state; the upper layer exploits this information to assemble a set of applicable inference rules and presents them to the user. The architecture also has mechanisms to adapt its behavior with respect to the current proof context and the availability of system resources. It furthermore allows for the integration of various automated components such as automated theorem provers, model generators or computer algebra systems. Moreover, the inference rule application can be automated itself, converting Omega-Ants into an automatic resource-adaptive reasoning system. We also describe the integration of the Omega-Ants mechanism into the multi- strategy proof planner MULTI to support traditional proof planning. In particular, we present how Omega-Ants can be employed to support interactive proof planning and to allow a search for applicable theorems from a mathematical knowledge base in parallel to the automatic proof planning process. Additionally, we present a means for soundly integrating certain symbolic computations into proof planning. The Omega-Ants architecture as well as all discussed combinations of reasoning techniques are implemented in the mega theorem proving environment and for each combination we have carried out extensive case studies in group theory and finite algebra.

Die vorliegende Arbeit präsentiert einen neuen Ansatz zur Kombination verschiedener Beweistechniken, insbesondere von interaktiven und automatischen Theorembeweisen, sowie Beweisplanung und Computeralgebra, und deren Anwendung zur Beweisplanung in endlicher Algebra und Gruppentheorie. Die zentrale Struktur, mit deren Hilfe die Kombination durchgeführt wird, ist die hierarchische Blackboardarchitektur Omega-Ants. Die Architektur verfügt über Mechanismen, sich sowohl bezüglich dem aktuellen Beweiskontext als auch der Ressourcenlage im System anzupassen. Darüberhinaus ermöglicht es eine Integration verschiedener automatischer Komponenten wie zum Beispiel automatischer Beweiser, Modellgenerierern oder Computeralgebrasystemen. Außerdem kann Omega-Ants selbst als automatisches, ressourcenadaptives Beweissystem eingesetzt werden. Weiterhin beschreibt die Arbeit die Integration des Omega-Ants Mechanismus in den Multistrategiebeweisplaner Multi zur Unterstützung von traditionellem Beweisplanen. Insbesondere kann Omega-Ants zur interaktiven Beweisplanung benutzt werden und auch als Mechanismus, um während des automatischen Beweisplanens möglicherweise anwendbare mathematische Sätze in einer Wissensbasis zu suchen. Zusätzlich wird eine Methodik beschrieben, mit deren Hilfe symbolisches Rechnen auf korrekte, wenn auch eingeschränkte Weise in die Beweisplanung integriert werden kann. Sowohl die Omega-Ants Architektur als auch die weiteren diskutierten Kombinationen von Beweistechniken wurden in der Beweisentwicklungsumgebung Omega implementiert und für jede der vorgestellten Kombinationen wurde eine ausführliche Fallstudie in der Gruppentheorie und endlichen Algebra durchgeführt.