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.

This book constitutes the refereed proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2000, held in St Andrews, Scotland, UK, in July 2000.The 23 revised full papers and 2 system descriptions presented were carefully reviewed and selected from 42 submissions. Also included are 3 invited lectures and 6 nonclassical system comparisons. All current issues surrounding the mechanization of reasoning with tableaux and similar methods are addressed - ranging from theoretical foundations to implementation, systems development, and applications, as well as covering a broad variety of logical calculi.

Automated deduction is a fundamental research area in the field of artificial intelligence. The aim of an automated deduction system is to find a formal proof for a given goal based on given axioms. Essentially automated deduction can be viewed as a search problem which spans huge search spaces. One main thrust of research in automated deduction is the development of techniques for achieving a reduction of the search space. A particularly promising approach for search space reduction relies on the integration of top-down and bottom-up reasoning. A possible approach employs bottom-up generated lemmas in top-down systems. Lemma use offers the possibility to shorten proofs and to overcome weaknesses of top-down systems like poor redundancy control. In spite of the possible advantages of lemma use, however, naive approaches for lemma integration even tend to slow down top-down systems. The main problem is the increased indeterminism in the search process. In this thesis important contributions for a successful application of lemmas in top-down deduction systems based on connection tableau calculi are made. New methods for lemma generation and for the estimation of the relevancy of lemmas are developed. As a practical contribution, the implementation of the new techniques leads to a powerful system for automated deduction which demonstrates the high potential of the new techniques.

This book constitutes the refereed proceedings of the 5th International Conference on Principles and Practice of Constraint Programmingm CP'99, held in Alexandria, Virginia, USA in October 1999. The 30 revised full papers presented together with three invited papers and eight posters were carefully reviewed and selected for inclusion in the book from a total of 97 papers submitted. All current aspects of constraint programming and applications in various areas are addressed.

Shared-workspace systems with structured graphical representations allow for the free user interaction and the joint construction of problem solutions for potentially open-ended tasks. However, group modelling in shared workspaces has to take on a process-orientated perspective due to the reduced system control in shared workspaces. This text is defined as the monitoring of user actions and the abstraction and interpretation of the raw data in the context of the group interaction and the problem representation. Formally based on plan recognition and the situation calculus, an approach has been developed that incorporates an operational hierarchy for generally modelling activities. The system performs an automatic inline analysis of group interactions and the results are visualized in different forms to give feedback and stimulating self-reflection.

Handbook of Automated Reasoning.

This thesis presents an approach to learning good search guiding heuristics for the supposition-based theorom prover E in equational deductions. Search decisions from successful proof searches are represented as sets annotated clause patterns. Term Space Mapping, an alternative learning method for recursive structures is used to learn heuristic evaluation functions for the evaluation of potential new consequences. Experimental results with extended system E/TSM show the success of the approach. Additional contributions of the thesis are an extended superposition calculus and a description of both the proof procedure and the implementation of a state-of-the-art equational theorem prover.