© 2001 by Oxford University Press
SHR Tableaux — A Framework for Automated Model Generation
1 Mathematisches Institut, Universität München, Theresienstr. 39, 80333 München, Germany. E-mail: rudlof{at}rz.mathematik.uni-muenchen.de
Refutation methods share two important points distinguishing them from the literature in the field of automated reasoning: they use the same basic idea — a mixture of hyperresolution and tableaux methods — in order to construct a refutation tree and they are considered rather to be model generators than refutation methods. But, they differ very much in the way they represent structures — and consequently the classes of formulae they can cope with are very different. Semantic Hyperresolution tableaux, introduced and investigated in this work, can be seen as a formal description of the model generation process the above methods have in common. We discuss the properties of this model generation process: we show for example that it is minimally and refutationally complete and that it is computable for each finite set of clauses over a language with equality. Moreover we investigate the set of models that can be computed in finite time. Especially we show, that each finite term model of a finite set of clauses can be computed in finite time.
Keywords: Automated model generation; finite model; hyperresolution; ground term rewriting
Accepted 9 March 1999.