| 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):
| ||||||||||||||
All documents in ORBilu are protected by a user license.
