Solving decidability problems using automated reasoning techniques

Project description

Decidability problems are among the most important and deeply studied problems in computer science, mathematics and logic. Decidability problems involve finding a decision procedure for a problem or proving that no decision procedure exists. Procedures that can determine in a finite number of steps whether a property (expressed as a formula) is true, or not, in a formalisation are decision procedures.

In this project the aim is to use automated reasoning techniques as tools to solve decidability problems related to modal logics, description logics and solvable fragments of first-order logic and applications such as ontology engineering and agent-based systems.
Because we are interested in having actually running systems the aim will be to develop practical, i.e. implementable, decision procedures.
Using techniques from automated reasoning has the advantage that practical decision decision procedures can often be obtained with modest implementation effort. Our interest is, in particular, developing resolution decision procedures. Resolution provides a very powerful theoretical framework for developing decision procedures and many well-developed resolution theorem provers exist which follow this framework and provide platforms for obtaining practical decision procedures.Currently, I am particularly interested in

- Developing practical decision procedures for solvable fragments
related to modal and description logics for which no practical
decision procedures are known yet.

- Generalisation and strengthening of existing decidability results and
decision procedures.

- Making first-order theorem provers more intelligent and automatically
use a resolution strategy that is known to be decision procedure for
the input problem.

- Non-standard decision problems such as ontology slicing, query
answering, etc.

This list is just indicative of the kind of research that might be undertaken. It is certainly not expected that all these aspects will be investigated.

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