Using Grammars for Computational Representations of Herbrand Models

. Finding computationally valuable representations of models of predicate logic formulas is an important task in many fields related to automated theorem proving, e.g. automated model building or semantic resolution. For representing a single (Herbrand) model we need a mechanism to describe all true ground atoms in the model, i.e. to characterize potentially infinite sets of terms. In this article we investigate the use of context-free languages for this purpose. We focus on expressive power (which we find out to be exactly the finite models) and on algorithmic issues like clause evaluation, equivalence test (which we solve by methods of automated theorem proving), etc., proving our approach to be an interesting base for investigating connections between term schematizations, formal language theory and automated model building. 1 Introduction Representing single models of predicate logic formulas plays an important role in various subfields of automated theorem proving. We just mentio..