Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
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 ...