NDLI: On the complexity of existential positive queries

Please wait, while we are loading the content...

ACM Transactions on Computational Logic (TOCL) : Volume 17

ACM Transactions on Computational Logic (TOCL) : Volume 16

ACM Transactions on Computational Logic (TOCL) : Volume 15

Issue 4, August 2014

Issue 3, July 2014

Issue 2, April 2014

Issue 1, February 2014

A PSPACE-complete first-order fragment of computability logic

Improved witnessing and local improvement principles for second-order bounded arithmetic

Algebra-coalgebra duality in brzozowski's minimization algorithm

Non-finite axiomatizability of dynamic topological logic

Quantifier-free interpolation in combinations of equality interpolating theories

Degree lower bounds of tower-type for approximating formulas with parity quantifiers

Using tableau to decide description logics with full role negation and identity

Extending two-variable logic on data trees with order on data values and its automata

On the complexity of existential positive queries

A resolution calculus for the branching-time temporal logic CTL

ACM Transactions on Computational Logic (TOCL) : Volume 14

ACM Transactions on Computational Logic (TOCL) : Volume 13

ACM Transactions on Computational Logic (TOCL) : Volume 12

ACM Transactions on Computational Logic (TOCL) : Volume 11

ACM Transactions on Computational Logic (TOCL) : Volume 10

ACM Transactions on Computational Logic (TOCL) : Volume 9

ACM Transactions on Computational Logic (TOCL) : Volume 8

ACM Transactions on Computational Logic (TOCL) : Volume 7

ACM Transactions on Computational Logic (TOCL) : Volume 6

ACM Transactions on Computational Logic (TOCL) : Volume 5

ACM Transactions on Computational Logic (TOCL) : Volume 4

ACM Transactions on Computational Logic (TOCL) : Volume 3

ACM Transactions on Computational Logic (TOCL) : Volume 2

ACM Transactions on Computational Logic (TOCL) : Volume 1

On the complexity of existential positive queries

Content Provider	ACM Digital Library
Author	Chen, Hubie
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.
Starting Page	1
Ending Page	20
Page Count	20
File Format	PDF
ISSN	15293785
e-ISSN	1557945X
DOI	10.1145/2559946
Volume Number	15
Issue Number	1
Journal	ACM Transactions on Computational Logic (TOCL)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-03-06
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Compilation First-order logic Fixed-parameter tractability Model checking
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Logic Computational Mathematics Computer Science

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Model Checking Existential Logic on Partially Ordered Sets

On first-order topological queries

The tractability of model checking for LTL: The good, the bad, and the ugly fragments

First-order queries on structures of bounded degree are computable with constant delay

Fixed-parameter tractability, definability, and model checking (2001)

Complexity of Existential Positive First-Order Logic

Monadic datalog over finite structures of bounded treewidth

FO model checking on geometric graphs

Fixed-parameter complexity of semantics for logic programs

On the complexity of existential positive queries

Similar Documents

Model Checking Existential Logic on Partially Ordered Sets

On first-order topological queries

The tractability of model checking for LTL: The good, the bad, and the ugly fragments

First-order queries on structures of bounded degree are computable with constant delay

Fixed-parameter tractability, definability, and model checking (2001)

Complexity of Existential Positive First-Order Logic

Monadic datalog over finite structures of bounded treewidth

FO model checking on geometric graphs

Fixed-parameter complexity of semantics for logic programs

On the complexity of existential positive queries