Model Checking Positive Equality-free FO: Boolean Structures and Digraphs of Size Three
Computational Complexity
2008-08-06 v1 Logic in Computer Science
Abstract
We study the model checking problem, for fixed structures A, over positive equality-free first-order logic -- a natural generalisation of the non-uniform quantified constraint satisfaction problem QCSP(A). We prove a complete complexity classification for this problem when A ranges over 1.) boolean structures and 2.) digraphs of size (less than or equal to) three. The former class displays dichotomy between Logspace and Pspace-complete, while the latter class displays tetrachotomy between Logspace, NP-complete, co-NP-complete and Pspace-complete.
Cite
@article{arxiv.0808.0647,
title = {Model Checking Positive Equality-free FO: Boolean Structures and Digraphs of Size Three},
author = {Barnaby Martin},
journal= {arXiv preprint arXiv:0808.0647},
year = {2008}
}