Title :
A Tetrachotomy for Positive First-Order Logic without Equality
Author :
Madelaine, Florent ; Martin, Barnaby
Author_Institution :
LIMOS, Clermont Univ., Clermont, France
Abstract :
We classify completely the complexity of evaluating positive equality-free sentences of first-order logic over a fixed, finite structure D. This problem may be seen as a natural generalisation of the quantified constraint satisfaction problem QCSP(D). We obtain a tetrachotomy for arbitrary finite structures: each problem is either in L, is NP-complete, is co-NP-complete or is P space-complete. Moreover, its complexity is characterised algebraically in terms of the presence or absence of specific surjective hyper-endomorphisms, and, logically, in terms of relativisation properties with respect to positive equality-free sentences. We prove that the meta-problem, to establish for a specific D into which of the four classes the related problem lies, is NP-hard.
Keywords :
computational complexity; constraint theory; formal logic; NP-complete; P space-complete; arbitrary finite structures; co-NP-complete; complexity; positive equality-free sentences; positive first-order logic; quantified constraint satisfaction problem; Complexity theory; Computer science; Context; Electronic mail; Games; Robustness; Upper bound; Computational Complexity; Galois connection; Logic in Computer Science; Quantified Constraint Satisfaction; Universal Algebra;
Conference_Titel :
Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on
Conference_Location :
Toronto, ON
Print_ISBN :
978-1-4577-0451-2
Electronic_ISBN :
1043-6871
DOI :
10.1109/LICS.2011.27