ATP systems are used in a wide variety of domains: A mathematician might use the axioms of group theory to prove the conjecture that groups of order two are commutative; a management consultant might formulate axioms that describe how organizations grow and interact and, from these axioms, prove that organizational death rates decrease with age; or a frustrated teenager might formulate the jumbled faces of a Rubik's cube as a conjecture and prove, from axioms that describe legal changes to the cube's configuration, that the cube can be rearranged to the solution state. All these tasks can be performed by an ATP system, given an appropriate formulation of the problem as axioms, hypotheses, and a conjecture. Most commonly, ATP systems are embedded as components of larger, more complex software systems, and in this context, the ATP systems are required to autonomously solve subproblems that are generated by the overall system. To build a useful ATP system, several issues have to ...

INTRODUCTION The evidence is already in favour of the computer becoming an aid to research in branches of mathematics which do not involve numerical computation. Programs have now been constructed for performing certain symbolic operations in mathematics, for example algebraic simplification of equations and indefinite integration, and for solving some of the problems (which are certainly not in the class of numerical calculations) now occurring in theoretical physics and other areas. One may reasonably expect that sooner or later programs of this type will be incorporated in a'questionanswering' package. As the construction of multi-programming systems progresses, and'on-line' use of the computer is accepted as normal, it will become more and more practicable for the mathematician to rely on the computer for answers to routine non-numerical questions. It is, therefore, of interest from a practical as well as a theoretical point of view to ask if this development can be taken a stage further by mechanising the processes of mathematical proof. In this way the computer could be used as a tool for establishing true mathematical statements or checking proofs for correctness. The problem is essentially to produce practicable programs for proving theorems which will answer some reasonably complicated questions before overstepping the bounds of available time and memory space. This is potentially one of the most rewarding areas of computer applications, but as many people already know, it is also one of the most frustrating.

We give some lectures on the work on formal logic of Jacques Herbrand, and sketch his life and his influence on automated theorem proving. The intended audience ranges from students interested in logic over historians to logicians. Besides the well-known correction of Herbrand's False Lemma by Goedel and Dreben, we also present the hardly known unpublished correction of Heijenoort and its consequences on Herbrand's Modus Ponens Elimination. Besides Herbrand's Fundamental Theorem and its relation to the Loewenheim-Skolem-Theorem, we carefully investigate Herbrand's notion of intuitionism in connection with his notion of falsehood in an infinite domain. We sketch Herbrand's two proofs of the consistency of arithmetic and his notion of a recursive function, and last but not least, present the correct original text of his unification algorithm with a new translation.

Revising knowledge bases (KBs) in description logics (DLs) in a syntax-independent manner is an important, nontrivial problem for the ontology management and DL communities. Several attempts have been made to adapt classical model-based belief revision and update techniques to DLs, but they are restricted in several ways. In particular, they do not provide operators or algorithms for general DL KB revision. The key difficulty is that, unlike propositional logic, a DL KB may have infinitely many models with complex (and possibly infinite) structures, making it difficult to define and compute revisions in terms of models. In this paper, we study general KBs in a specific DL in the DL-Lite family. We introduce the concept of features for such KBs, develop an alternative semantic characterization of KBs using features (instead of models), define two specific revision operators for KBs, and present the first algorithm for computing best approximations for syntax-independent revisions of KBs.

This paper introduces a new methodology of revising general KBs in DL-Lite. Two specific revision operators are defined, their properties are investigated and algorithms for computing revisions are developed.

Thus, the reader is able to experiment is a logical consequence of a set of aspects of the deduction steps as both a user and a developer statements (the axioms and hypotheses).