2013 seminar talk: Model Checking Quantified-Conjunctive Formulas

Talk held by Hubie Chen (Universidad del País Vasco, Spain and Basque Foundation for Science, Spain) at the KGRC seminar on 2013-04-18.


Model Checking, the problem of deciding if a logical sentence holds on a 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.

Bottom menu

Kurt Gödel Research Center for Mathematical Logic. Währinger Straße 25, 1090 Wien, Austria. Phone +43-1-4277-50501. Last updated: 2010-12-16, 04:37.