Computational Logic: Super-Counting Quantifiers

Many problems in computational logic reduce to the so-called satisfiability problem: given a formula of some logic, determine whether that formula is satisfiable (i.e., represents a logically possible situation). It is well known that, for first-order logic as a whole, this problem is undecidable; however, for various fragments of first-order logic, it admits of an algorithmic solution. One large such fragment is the two-variable fragment with counting quantifiers, usually denoted C2. In this fragment, only two logical variables, x and y may appear; however, we can use counting quantifiers of the form "There exist M x such that ....", where M is a natural number. The complexity-theoretic properties of this fragment have been understood for some years.

Very recently, it has been shown that counting quantifiers can be generalized without losing decidability. Thus, for example, C2 can be extended with counting modulo k for some fixed k, thus giving us expressions like "There exist an even number of x such that ....". It seems clear that this extension is a special case of a more general kind of quantifier in which certain "local patterns" of relations are specified using various computational models. The aim of this project is to establish the extent to which counting quantifiers can be thus generalized. It is expected that this work will have an impact developements in description logics and related applications. The research may taken in either a purely theoretical direction, or via a mixture of theory and implementation.

The project requires a good understanding of logic, and the willingness to learn the necessary mathematical background in graph theory, model theory and comptational complexity theory.