Journal of Logic and Computation, Volume 11, Issue 1, pp. 107-155: Abstract.
SHR Tableaux - A Framework for Automated Model Generation
Thomas M. Rudlof
Mathematisches Institut, Universität München, Theresienstr. 39, 80333 München, Germany. E-mail: email@example.com
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