Computational Logic: Adventures with the Fluted Fragment

Many problems in computational logic reduce to the 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 such fragment is the fluted fragment, which originated in the work of W. Quine in the 1960s, and which in recent years has attracted renewed interest. Unlike many decidable fragments---in particular, the vast majority of so-called description logics---the fluted fragment is not limited in the number of variables or the arity of the predicates appearing in its formulas. Much is known about its computational properties: thus, for example, the satisfiability problem for its m-variable sub-fragment is in (m-2)-NExpTime (for m > 2) and is m/2-NExpTime hard (for even m > 1). Very recently, two extensions of the fluted fragment have been shown to be decidable: one with counting quantifiers, the other with a single transitive relation.

Yet many questions remain. For instance, it has not yet been possible to close the complexity gap mentioned in the previous paragraph. The extensions with counting quantifiers are still poorly understood (and only weak complexity results are available). It is not known whether satisfiability for fluted logic with two transitive relations (but without equality) is decidable. And the same holds for the extension with both counting quantifiers and a single transitive relation. The aim of this project is to resolve as many of these issues as possible, and, additionally, to forge links with fragments of first-order logic, notably, description logics, which have been developed with a more application-oriented agenda in mind. The research may be 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 model theory and computational complexity theory.