Kurt Gödel Research Center

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.

Abstract

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.