Operators on lattices of ω-Herbrand interpretations

Abstract

Interpretations defined by J. Herbrand in early 1930's have found new applications when logic programming emerged in 1970's. Now they are being used as a major technical tool in the theory underlying construction of languages such as Prolog.

In an Herbrand interpretation of a first-order language L elements of the universe are precisely the closed terms of L. In our research we consider the following generalization: by an ω-Herbrand interpretation for L we understand an Herbrand interpretation for the language resulting from L by adjoining ω new individual constants.

We have shown that the theory of equality determined by such interpretations is decidable. In this paper we consider operators corresponding to formulas A ← B where B is a positive formula with general quantifiers. We prove that such operators on the lattice of ω-Herbrand models reach their least fixed points in ω steps. (This shows a great conceptual difference between conventional Herbrand models and ω-Herbrand models.)

We see the following applications of these results: The decidability algorithm can be used as a computing mechanism in an implementation of a fully declarative programming language that overcomes several deficiencies of Prolog; The result on least fixed points provides a basis for the proof of declarative correctness and completeness of that language.