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.
Model Checking Quantified-Conjunctive Formulas
18.04.2013 15:00 - 16:30
Organiser:
KGRC
Location:
SR 101, 2. St., Währinger Str. 25