Hubie Chen

Decomposing quantified-conjunctive logic

Model Checking, by which we mean the problem of deciding if a logical sentence holds on a finite structure, is a basic computational task which is well-known to be computationally intractable in general. We study model checking on the quantified-conjunctive fragment of first-order logic, by which is meant the class of formulas built using conjunction as the only connective, and both quantifiers. We present complexity classification results which systematically identify tractable cases of model checking on this fragment. One recent such classification result involves an algebraic understanding of logical equivalence in this fragment, which understanding we discuss.