Anybody with a keen interest in automated reasoning, logic and intelligent knowledge processing will enjoy these projects. Implementation work is optional (but welcome).
Since every year PhD studentships are awarded on a first come first serve basis and the deadlines for the President's and Faculty awards are normally in December to February it is advisable to apply early in the academic year. For School awards there are usually no deadlines, but do refer to the PhD application pages on the School website and contact someone in the admissions team for the most up-to-date information.
If you want further information on the following projects 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.
All projects have the potential to lead to a PhD research project.
Ontologies are formal frameworks to organize terminological information and are used in a range of areas including artificial intelligence, semantic web, biomedical informatics, systems engineering and many more. Similar to thesauri, ontologies are used to define the meaning of concepts and describe properties and interrelationships between concepts. Various editors and visualisation tools exists for ontologies. Unfortunately they cannot handle very large ontologies containing 100,000s of concept definitions.
To address this problem the aim of this project is to design and develop a viewing and navigation toolkit for large ontologies. The idea is to develop tools that can be integrated with other tools and APIs that will make it easier for users and ontology engineers to zoom in on potentially problematic parts of a large ontology (or large collection of ontologies) where they want to gain a better understanding (e.g., of the relationship between concepts), or suspect modeling defects. The tool could be either something similar to the Unix less command for paging and navigating through ontology specification files; or it could be something to the Graph API to get data from Facebook's social graph; or it could be graph visualisation and navigation tool.
Possible features that come to mind are the following (note not all of these have to be realised):
Ontologies are knowledge systems that organise terminological information, and are used in a variety of areas including medicine, bio-informatics, the semantic web, software engineering, and many more. For ontology engineers and users to be able to understand the information content of potentially large ontologies it is important to provide convenient and reliable ontology analysis tools. Currently, editors and browsers such as the very popular, Manchester-Stanford developed Protege system supports ontology engineers with integrated standard reasoning services, explanation finding, useful refactoring methods and visualisations. The GUI assists developers to find uses of specific concept symbols with relative ease. However, in order to get a deeper understanding of the relationships between the terms in an ontology, further analysis tools are needed.
The aim of this project is to develop a prototypical ontology-browser in the form of a web-application with advanced analysis functionalities. The ontology browser would allow users to zoom into certain terms and parts of an ontology in order for users to get a deeper understanding of the logical structure of ontologies and the relationships between the terms in an ontology. For example, this is useful when a user updates an ontology with new information in order to inspect that important parts of the information in the original ontology (relevant to their domain of expertise) is not lost in the updated ontology.
The student will be provided with a software library built within the research group that can compute such restricted views for parts of an ontology on demand. Depending on the size and the structure of the ontology, the computations performed to create the views can be expensive. It would therefore be useful to develop ways of organising queries to the library in a way that allows for fast browsing of the ontology. The ontology views should be visualised in an appropriate way, allowing for user-friendly browsing and understanding. Ontology editors such as Protege or Web-Protege could serve as an orientation on how the views are represented.
Depending on the students capabilities, there are various directions in which the project can be expanded. One such expansion would be to provide automated support to users for repairing an ontology if essential information is presently missing from the ontology. This would again exploit the provided software package. Another possibility is to extend the ontology-browser with simple editing-facilities.
Model generation is useful for fault analysis, verification of systems and validation of data models. In general a satisfiable formula or set of clauses (representing a property of a system or an ontology) has many models. These models can be large. In COMP60332 we discuss the construction of candidate models for the model existence theorem used to prove refutational completeness of resolution. Candidate models can be viewed as being minimal/optimal with respect to the given ordering.
This project is concerned with the generation and manipulation of candidate models. The aim is to implement a tool for the construction of candidate models and support for querying the constructed model, that is, to determine whether a formula is true in the candidate model. In particular, the input to the tool is a set of clauses and an atomic formula, while the output is the candidate model and an answer to whether the query holds in it, if the set of clauses is saturated, and a minimal exception clause, otherwise.
The deliverable is a tool for generating and querying a candidate model for a set of clauses (i.e., formulas in simplified form).
The project is suitable for anyone interested in logic and automated reasoning. Some background in either is an advantage.
A previous very successful third year project has implemented an automated theorem prover for modal logic which is based on the semantic tableau approach (Beth-tableau). Modal logic is an extension of propositional logic (i.e. Boolean logic) with two operators (the diamond and box operator) that allow for restricted forms of existential and universal quantification.The goal of an automated theorem prover is to determine whether a given formula is a theorem or not (or equivalently, to determine whether there is a satisfying truth assignment for the negation of the formula). Semantic tableau provers produce derivations that have the form of trees, thus their name. The branches in the tree derivations represent attempts to compute a satisfying assignment for the given formula. If a branch has been exhaustively explored backtracking occurs and an alternative branch is computed and explored. The prover is implemented in Java.
The aim of this project is to extend and enhance this prover with new functionalities. For this there are a variety of possibilities (it is not required that all these are tackled):
There may be aspects of logic and automated reasoning that you find interesting and wish to explore further, but which are not covered by any of the project proposals. You may also be interested in related topics not covered. I am happy to supervise projects other than those proposed that are related to my research interests. Please contact me in advance of the MSc project selection deadline so that we can discuss your ideas.