Journal of Logic and Computation Advance Access originally published online on March 21, 2007
Journal of Logic and Computation 2007 17(3):453-477; doi:10.1093/logcom/exm008
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||
Original Articles |
Model Representation over Finite and Infinite Signatures*
Technische Universität Wien, A-1040 Vienna, Austria.
E-mail: chrisf{at}logic.at; reini{at}logic.at
Received 12 October 2006.
 |
Abstract |
|---|
The computationally adequate representation of term models for sets of clauses is a topic that is relevant to many areas of Computer Science. Two fundamental decision problems arise: (1) to check whether a given clause is true in a represented model and (2) to decide whether two representations of the same type represent the same model. Atomic representations of a term model (ARMs), contexts and disjunctions of implicit generalizations (DIGs) are three important examples of model representation formalisms. The complexity of the mentioned decision problems has been studied so far only for ARMs over finite signatures. We settle the remaining cases, i.e. ARMs over any infinite signature, and DIGs and contexts over both finite and infinite signatures. Moreover we show that contexts and DIGs have the same expressive power, i.e. they allow one to represent exactly the same class of models. However DIGs may be exponentially more succinct than all equivalent contexts.
*Preliminary versions of the results presented here appeared in [20] and [21].