Model Representation over Finite and Infinite Signatures

摘要

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.