Paper: Working with Arms: Complexity Results on Atomic Representations of Herbrand Models (at LICS 1999)

Authors: Georg Gottlob Reinhard Pichler

Abstract

An Atomic Representation of a Herbrand Model (ARM) is a finite set of (not necessarily ground) atoms over a given Herbrand universe. Each ARM reprents a possibly infinite Herbrand interpretation. This concept has emerged independently in different branches of Computer Science as a natural and useful 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 equivalence of two ARMs, deciding subsumption between ARMS, and evaluating clauses over ARMS. These problems were shown to be decidable, but their computational complexity has remained obscure so far. The previously published decision algorithms require exponential space. In spite of this, by developing new decision procedures, we are able to prove that all mentioned problems are coNP-complete.

BibTeX

  @InProceedings{GottlobPichler-WorkingwithArmsComp,
    author = 	 {Georg Gottlob and Reinhard Pichler},
    title = 	 {Working with Arms: Complexity Results on Atomic Representations of Herbrand Models},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999)},
    year =	 {1999},
    month =	 {July}, 
    pages =      {306--315},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }