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).