On the complexity of existential positive queries

DOI10.1145/2559946MaRDI QIDQ5410336zbMATH OpenOpenAlexWikidataFDO

Authors Hubie Chen

Publication date 16 April 2014

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1206.3902, https://eprints.bbk.ac.uk/id/eprint/21941/1/1206.3902.pdf

zbMATH Keywords

compilationfirst-order logicfixed-parameter tractabilitymodel checking

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We systematically investigate the complexity of model checking the existential positive fragment of first-order logic. In particular, for a set of existential positive sentences, we consider model checking where the sentence is restricted to fall into the set; a natural question is then to classify which sentence sets are tractable and which are intractable. With respect to fixed-parameter tractability, we give a general theorem that reduces this classification question to the corresponding question for primitive positive logic, for a variety of representations of structures. This general theorem allows us to deduce that an existential positive sentence set having bounded arity is fixed-parameter tractable if and only if each sentence is equivalent to one in bounded-variable logic. We then use the lens of classical complexity to study these fixed-parameter tractable sentence sets. We show that such a set can be NP-complete, and consider the length needed by a translation from sentences in such a set to bounded-variable logic; we prove superpolynomial lower bounds on this length using the theory of compilability, obtaining an interesting type of formula size lower bound. Overall, the tools, concepts, and results of this article set the stage for the future consideration of the complexity of model checking on more expressive logics.

Recommendations

• The complexity of equivalence, entailment, and minimization in existential positive logic
• On the complexity of the model checking problem
• First-Order Model Checking Problems Parameterized by the Model

Cites work

• An n! lower bound on formula size
• Conjunctive-query containment and constraint satisfaction
• Constraint satisfaction with succinctly specified relations
• Decomposing quantified conjunctive (or disjunctive) formulas
• Homomorphism preservation theorems
• scientific article; zbMATH DE number 803291 (Why is no real title available?)
• scientific article; zbMATH DE number 839556 (Why is no real title available?)
• On preservation under homomorphisms and unions of conjunctive queries
• Parametrized complexity theory.
• Preprocessing of intractable problems
• Query evaluation via tree-decompositions
• The complexity of homomorphism and constraint satisfaction problems seen from the other side
• The complexity of positive first-order logic without equality
• The core of a graph
• The succinctness of first-order logic on linear orders
• Tractable hypergraph properties for constraint satisfaction and conjunctive queries
• Tractable structures for constraint satisfaction with truth tables
• Tree-width for first order formulae
• Turing machines that take advice
• When is the evaluation of conjunctive queries tractable?

Cited in

(13)

• Expressive power and succinctness of the positive calculus of binary relations
• How many variables are needed to express an existential positive query?
• How many variables are needed to express an existential positive query?
• On the complexity of the model checking problem
• The tractability frontier of graph-like first-order query sets
• The tractability frontier of graph-like first-order query sets
• The complexity of equivalence, entailment, and minimization in existential positive logic
• The parameterized space complexity of model-checking bounded variable first-order logic
• Expressive Power and Succinctness of the Positive Calculus of Relations
• Optimally rewriting formulas and database queries: a confluence of term rewriting, structural decomposition, and complexity
• From quantifier depth to quantifier number: separating structures with k variables
• Optimally rewriting formulas and database queries: a confluence of term rewriting, structural decomposition, and complexity
• Equi-rank homomorphism preservation theorem on finite structures

This page was built for publication: On the complexity of existential positive queries

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5410336)