Systematic development and synthesis of deduction approaches

Project description

A strong focus of our current research is the synthesis of tableau and other deduction calculi, a new research topic posing interesting and challenging problems in the field of automated reasoning. In general, we cannot expect to be able to synthesise deduction calculi fully automatically for every logic or every logical theory. Our recent work has however shown automated tableau synthesis (and even tableau prover generation) is now within the realm of what is possible for well-defined logics. This presents exciting opportunities for significant advances in proof theory and automated deduction for applications requiring logical reasoning in many subareas of computer science and mathematics.

The aim of the project is to contribute to research on the systematic development and synthesis of deduction approaches by focussing on some relevant subproblems, which may involve:

- extending our tableau synthesis framework;
- case studies and its use in agent-based systems or another application;
- studying and developing new decision procedures;
- investigating the relationship of the generated calculi to existing calculi and algorithms implemented in current tools;
- incorporating and devising new refinements and optimisation techniques;
- implementation and practical evaluation.

This list is not exhaustive and it is not expected that all these aspects will be explored. Depending on the interest of the student the focus may be on some non-classical logics, e.g., modal logics, multi-agent logics, description logics, intuitionistic logics, or something else.

The project is ideal for someone with a keen interest in computational logic, artificial intelligence, formal methods and automated reasoning.

To discuss the project please contact Renate Schmidt.

▲ Up to the top