We study the complexity of model checking in quantified conjunctive logic, that is, the fragment of first-order logic where both quantifiers may be used, but conjunction is the only permitted connective. In particular, we study block-sorted queries, which we define to be prenex sentences in multi-sorted relational first-order logic where two variables having the same sort must appear in the same quantifier block. We establish a complexity classification theorem that describes precisely the sets of block-sorted queries of bounded arity on which model checking is fixed-parameter tractable. This theorem strictly generalizes, for the first time, the corresponding classification for existential conjunctive logic (which is known and due to Grohe) to a logic in which both quantifiers are present. © 2013 Springer-Verlag.
CITATION STYLE
Chen, H., & Marx, D. (2013). Block-sorted quantified conjunctive queries. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7966 LNCS, pp. 125–136). https://doi.org/10.1007/978-3-642-39212-2_14
Mendeley helps you to discover research relevant for your work.