Abstract
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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Chandra, A.K., Merlin, P.M.: Optimal implementation of conjunctive queries in relational data bases. In: Proceddings of STOC 1977, pp. 77–90 (1977)
Chen, H., Dalmau, V.: Decomposing quantified conjunctive (or disjunctive) formulas. In: LICS (2012)
Chen, H., Grohe, M.: Constraint satisfaction with succinctly specified relations. Journal of Computer and System Sciences 76(8), 847–860 (2010)
Chen, H., Madelaine, F., Martin, B.: Quantified constraints and containment problems. In: Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS (2008)
Gottlob, G., Greco, G., Scarcello, F.: The complexity of quantified constraint satisfaction problems under structural restrictions. In: IJCAI 2005 (2005)
Grohe, M.: The complexity of homomorphism and constraint satisfaction problems seen from the other side. Journal of the ACM 54(1) (2007)
Grohe, M., Schwentick, T., Segoufin, L.: When is the evaluation of conjunctive queries tractable? In: STOC 2001 (2001)
Marx, D.: Tractable hypergraph properties for constraint satisfaction and conjunctive queries. In: Proceedings of the 42nd ACM Symposium on Theory of Computing, pp. 735–744 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, H., Marx, D. (2013). Block-Sorted Quantified Conjunctive Queries. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds) Automata, Languages, and Programming. ICALP 2013. Lecture Notes in Computer Science, vol 7966. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39212-2_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-39212-2_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39211-5
Online ISBN: 978-3-642-39212-2
eBook Packages: Computer ScienceComputer Science (R0)