The following projects are suitable for anybody interested in automated reasoning, logic, semantic technologies, knowledge representation, agent-based systems, and automating mathematics. All projects have the potential to lead to PhD research project.
Further topics you might want to consider are the following.
If you want further information on these or you want to propose an own project relating to the above topics or my research interests please feel free to discuss them with me.
Modern highly optimised tableau provers for descrition and modal logics use combinations of clever optimisations and heuristics for restricting the search space of derivations. The aim of the project is to design and implement commonly used optimisations and heuristics such as backjumping and dynamic backtracking and incorporate them into the MetTeL system. MetTeL is a tableau-based reasoner which also provides a platform for developing new tableau reasoners for modal, description and other logics. It includes a generic core for tableau reasoning and can be used flexibly with separate plug-ins which specific the tableau rules of the underlying calculus. MetTeL is written in Java.
The project is a part of a bigger research project on automated synthesis of tableau provers. It is expected that if the test results are positive the written Java code could become part of the automated tableau synthesis project.
Prerequisites: knowledge of modal logic or description logic, tableau, Java, COMP61132 or COMP60421
References:
In an ongoing research project we are developing a theoretical framework and software for automatically synthesising tableau calculi and implemented tableau provers. The idea is that the user specifies the logic of interest and gives it to the tableau synthesis software and the output is a set of inference rules which form a sound and complete tableau calculus or implemented prover for the logic.
The aim of this project is to undertake case studies of different specifications of logics and the tableau calculi/provers generated. Depending on the interest and background of the student any logics can be considered. Our proposal is for the project to focus on modal logics or other non-classical logics. The research is expected to include a comparison between the generated tableau calculi and existing tableau calculi found in the literature.
This project is ideal for a mathematically inclined student who wants to do a more theoretical project.
Recommended background: COMP61111 or COMP61132 or COMP60421 or knowledge of tableau and logic (e.g. first-order logic, modal logic other non-classical logics)
This project will focus on the problem of computing first-order correspondence properties for modal axioms. Modal logics can be studied systematically by the class of frames they define. For example the modal logic K is characterised by the class of all frames, whereas the logic KT4 (= S4) is characterised by the class of all frames in which the accessibility relation is reflexive and transitive. In many extensions of the logic K with modal axioms such as KT4, the additional axioms correspond to certain constraints on the accessibility relations, called frame correspondence properties. There are ways of automatically computing first-order correspondence properties from modal axioms. The aim of the project is to study and implement an approach described in Schmidt (2008). This approach is based on a modal deduction calculus which attempts to transform a given modal axiom to its first-order correspondence property (if one exists) in a sequence of inference steps.
Depending on the interest of the student this can be be a more theoretical project or a more implementation focussed project.
The project is a part of a bigger research project on automated synthesis of tableau provers, where the aim is to generate tableau calculi and implemented tableau provers from the specification of a logic.
Recommended background: COMP61111 or COMP61132 or COMP60421 or knowledge of: first-order logic or modal logic or description logic.
References:
The aim of this project is to study and develop tableau-based decision procedures. Tableau approaches are popular, because they are easy to understand and users find them easy to learn, and they can be implemented efficiently. In general the models constructed by tableau approaches are infinite which means tableau approaches are not automatically decision procedures. To control the size of the models constructed various techniques have been developed. In the area of description and modal logics blocking techniques are used to find repetitions in models and limit the size of models generated. It this project the focus will be on these blocking techniques, in particular, the aim is to implement a tableau prover based on the unrestricted blocking technique. Unrestricted blocking is designed to be generic and not limited to certain applications or logics. Being based on a simple idea with the crucial property that it is monotone, it is intuitive, natural, and conceptually easy to add to existing tableau calculi. At the same time unrestricted blocking is a very powerful technique for developing tableau decision procedures.
The objective of the project is to implement a tableau prover with unrestricted blocking or extend an existing tableau prover with unrestricted blocking for a description logic or a modal logic, or another logic to be determined depending on the interest and background of the student. The evaluation is expected to include a comparison with other blocking techniques, which could be based on empirical testing but does not need to be.
The project is a part of a bigger research project on automated synthesis of tableau provers and thus provides an opportunity for contributing to this exciting new research area.
Recommended background: knowledge of first-order logic or modal logic or description logic, knowledge of tableau, COMP61111 or COMP61132 or COMP60421
Recommended background: knowledge of logic or automated reasoning or COMP61111 or COMP61132 or COMP60421