Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
430008 | Journal of Computer and System Sciences | 2015 | 15 Pages |
The existential positive fragment of first-order logic is the set of formulas built from conjunction, disjunction, and existential quantification. On sentences from this fragment, we study three fundamental computational problems: logical equivalence, entailment, and the problem of deciding, given a sentence and a positive integer k, whether or not the sentence is logically equivalent to a k -variable sentence. We study the complexity of these three problems, and give a description thereof with respect to all relational signatures. In particular, we establish for the first time that, over a signature containing a relation symbol of binary (or higher) arity, all three of these problems are complete for the complexity class Π2p of the polynomial hierarchy.