Reference : Annotation theories over finite graphs
Scientific journals : Article
Engineering, computing & technology : Computer science
http://hdl.handle.net/10993/15878
Annotation theories over finite graphs
English
Gabbay, Dov M. [King’s College London, Department of Computer Science, London, UK; Bar-Ilan University, Ramat-Gan, Israel]
Szalas, A. [> >]
2009
Studia Logica
Springer
Yes
0039-3215
1572-8730
Berlin
Germany
[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
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].
http://hdl.handle.net/10993/15878
To appear

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
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.