Reference : Annotation theories over finite graphs
Scientific journals : Article
Engineering, computing & technology : Computer science
Annotation theories over finite graphs
Gabbay, Dov M. [King’s College London, Department of Computer Science, London, UK; Bar-Ilan University, Ramat-Gan, Israel]
Szalas, A. [> >]
Studia Logica
[en] argumentation theory ; labeled graphs ; semantics of logic programs
[en] 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
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].
To appear

File(s) associated to this reference

Fulltext file(s):

Open access
art%3A10.1007%2Fs11225-009-9220-3.pdfPublisher postprint374.11 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.