The complexity of equivalence, entailment, and minimization in existential positive logic

摘要

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.