Comparing Computational Representations of Herbrand Models

. Finding computationally valuable representations of models of predicate logic formulas is an important issue in the field of automated theorem proving, e.g. for automated model building or semantic resolution. In this article we treat the problem of representing single models independently of building them and discuss the power of different mechanisms for this purpose. We start with investigating context-free languages for representing single Herbrand models. We show their computational feasibility and prove their expressive power to be exactly the finite models. We show an equivalence with "ground atoms and ground equations" concluding equal expressive power. Finally we indicate how various other well known techniques could be used for representing essentially infinite models (i.e. models of not finitely controllable formulas), thus motivating our interest in relating model properties with syntactical properties of corresponding Herbrand models and in investigating connections betwe..