Imperial College London Featured PhD Programmes
Gdansk University of Technology Featured PhD Programmes
Solent University Featured PhD Programmes

Computational Logic: Adventures with the Fluted Fragment


   Department of Computer Science

This project is no longer listed on FindAPhD.com and may not be available.

Click here to search FindAPhD.com for PhD studentship opportunities
  Dr I Pratt-Hartmann  Applications accepted all year round  Competition Funded PhD Project (Students Worldwide)

About the Project

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.


Funding Notes

Applications are invited from self-funded students. This project has a Band 1 fee.
Equality, diversity and inclusion is fundamental to the success of The University of Manchester, and is at the heart of all of our activities. The full Equality, diversity and inclusion statement can be found on the website https://www.bmh.manchester.ac.uk/study/research/apply/equality-diversity-inclusion/

How good is research at The University of Manchester in Computer Science and Informatics?


Research output data provided by the Research Excellence Framework (REF)

Click here to see the results for all UK universities
PhD saved successfully
View saved PhDs