Constructing Bachmair-Ganzinger models

Abstract

We give some algorithms for constructing models from sets of clauses saturated by Ordered Resolution (with Selection rules). In the ground case, we give an efficient algorithm for constructing a minimal model. Then we generalize minimal models to preferred models, which may be useful for verification. For the ground case, we also show how to construct all models for a set of clauses saturated by Ordered Resolution, in time polynomial in the number of models. We also generalize our results to nonground models, where we add a restricted splitting rule to our inference rules, and show that for any set of clauses saturated by Ordered Resolution (with Selection), a query about the truth of a particular atom in the model can be decided. © Springer-Verlag Berlin Heidelberg 2013.