Home  Online Resources  Table of Contents

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: rudlof@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

  Full-Text PDF  (516 KB)

[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2001.