Book Description

Automated deduction is one of the fundamental disciplines in the field of artificial intelligence. The purpose of systems for automated deduction is to find formal proofs for given conjectures by drawing conclusions from formally specified knowledge. Their main strength is that they allow a purely declarative description of knowledge, i.e., procedural information on the drawing of conclusions need not be provided. In combination with the indeterminism in the drawing of possible conclusions, however, the ability to handle declarative specifications introduces the aspect of search into the deduction process. Usually, tremendous search spaces have to be explored in order to find a proof. Successful systems for automated deduction can be built, for example, on the basis of connection tableau calculi. In this thesis, an approach to a more intelligent search in connection tableau calculi is made. The approach is based on the compression of structurally similar formulas given to and derived by connection tableau calculi. Disjunctive constraints over first order terms are used to express the results of the compression. There are two main theoretical results of the thesis. Firstly, it introduces a new class of sound and complete connection tableau calculi, the so-called constrained-connection-tableau calculi, which are compatible with the most important search pruning techniques of conventional connection tableau calculi. Secondly, intelligent algorithms for solving disjunctive constraints over first order terms are developed. As a practical result, the implementation of the approach leads to a powerful system for automated deduction which demonstrates the high potential of the new developments.