Working with ARMs: Complexity results on atomic representations of Herbrand models

An atomic representation of a Herbrand model (ARM) is a finite set of (not necessarily ground) atoms over a given Herbrand universe. Each ARM represen ts a possibly infinite Herbrand interpretation. This concept has emerged in dependently in different branches of computer science as a natural and usef ul generalization of the concept of finite Herbrand interpretation. It was shown that several recursively decidable problems on finite Herbrand models (or interpretations) remain decidable on ARMs. The following problems are essential when working with ARMs: Deciding the e quivalence of two ARMs, deciding subsumption between ARMs, and evaluating c lauses over ARMs. These problems were shown to be decidable, but their comp utational complexity has remained obscure so far. The previously published decision algorithms require exponential space. In this paper, we prove that all mentioned problems are coNP-complete. (C) 2001 Academic Press.