Annotation theories over finite graphs

In the current paper we consider theories with vocabulary containing a num-
ber of binary and unary relation symbols. Binary relation symbols represent labeled edges
of a graph and unary relations represent unique annotations of the graph’s nodes. Such
theories, which we call
annotation theories
, can be used in many applications, including
the formalization of argumentation, approxim
ate reasoning, semantics of logic programs,
graph coloring, etc. We address a number of problems related to annotation theories over
finite models, including satisfiability, querying problem, specification of preferred models
and model checking problem.
We show that most of considered problems are
NPTime
-or
co-NPTime
-complete.
In order to reduce the complexity for particular theories, we use second-order quantifier
elimination. To our best knowledge none of existing methods works in the case of anno-
tation theories. We then provide a new second-order quantifier elimination method for
stratified theories, which is successful in the considered cases. The new result subsumes
many other results, including those of [2, 28, 21].