Student research opportunities
Efficient Compositional Theorem Proving
Project Code: CECS_886
This project is available at the following levels:
CS single semester, Honours, Summer Scholar, Masters, PhD
Keywords:
Modal Logic, Automated Reasoning, Implementation of Logics, Knowledge Representation
Supervisor:
Dr Dirk PattinsonOutline:
Modal (and Description) logics are formalisms that are well-suited for knowledge representation as they combine expressive power with good computational properties. This project contributes to determining to what extent these formalisms are capable of handling heterogeneous domains where different aspects of knowledge (such as causality, temporality etc.) are combined.
Goals of this project
The goal of the project is to extend an already existing theorem prover by implementing additional modal logics which can then be modularly combined within an expressive platform.
Requirements/Prerequisites
Good programming skills and a keen interest in theoretical questions.
Student Gain
Development of programming skills, exposure to logical foundations in knowledge representation, bridging a theory/practise gap.
Background Literature
Modal Logics in General:
Blackburn, de Rijke, Venema, Modal Logic, CUP.
Position Paper:
Cîrstea, Kurz, Pattinson, Schröder, and Venema. Modal
logics are coalgebraic. Comput. J., 54(1):31-41, 2011.
Technical background:
Kupke and Pattinson. Coalgebraic semantics of modal
logics: an overview. Theoretical Computer Science,
412(38):5070-5094, 2011
