# A. Leitsch:

Automated Model Building,

or How to Improve Logical Information in Theorem Proving

### Abstract

Frequently automated theorem provers are just considered as (more or
less clever) implementations of logic calculi. Most effort is spent on
pruning the search space and on optimization of basic rules like
unification and resolution. Although these efforts are necessary and
useful, we believe that more emphasis should be laid on the "intelligence"
of the programs and on the quality of *logical information*.

The main
purpose of this talk is to explain and (to some extent)
define this point of view. First of all we show how the termination
behavior of traditional theorem provers can be improved by simple analysis
of the syntax of input problems (prover generators instead of rigid
refinements). Clearly if (e.g.) a resolution theorem
prover terminates without producing a contradiction we know that the
set of clauses is satisfiable (or the original untransformed theorem is
not provable). We show that hyperresolution and ordered resolution are
specifically suited for decision procedures. Sometimes these deductive
decision procedures (hyperresolution or positive resolution + ordered
paramodulation) can (almost directly) be used as procedures extracting
models (i.e. representations of models) from satisfiable sets of clauses.
Thus, in many cases, traditional and efficient methods commonly used in
ATP can be applied to extract more information out of the problems than
just provability.

Unfortunately these methods have only a quite limited
potential to express and to construct rather complicated models. To this
aim stronger methods (based on equational constraints) have been invented
and analyzed. To some extent, there is a trade-off between semantic
information and efficiency, but sometimes it makes sense to buy more
information at the cost of speed. Still the currently existing extensions
of clausal calculi are too weak to handle specific (very simple) cases
of (Herbrand-) model construction. Finally we present some open problems
concerning symbolic model building and model representation and
potentially powerful tools (like meta-terms and order constraints).