Logics with counting.
In recent years, much progress has been made in determining the computational complexity of decidable logics with arithmetic constructions (those which talk about the numbers of objects possessing certain properties). Many such logics are now known to lie in surprisingly low complexity classes. Nevertheless, the inference algorithms for these logics exhibiting optimal theoretical complexity are, almost without exception, difficult to implement effectively. The aim of this project is to investigate further the mathematics of logics with arithmetic constructions, and to develop practically implementable inference methods with optimal theoretical complexity.