Student research opportunities
Interpolation in Non-Iterative Modal Logics
Project Code: CECS_887
This project is available at the following levels:
CS single semester, Honours, Summer Scholar, Masters, PhD
Keywords:
Modal Logic, Automated Reasoning, Interpolation
Supervisor:
Dr Dirk PattinsonOutline:
Non-Iterative Logics are a special, resetricted class of modal logics that most notably comprise so-called conditional logics that formalise statements of the kind `if A then normally B', i.e. various forms of `exceptions to the rule'. There is growing evidence that meta-logical properties of these logics can be established uniformly and irrespective of the concrete logic at hand. One such important property is interpolation that, among other things, allows for compositional theorem proving.
Goals of this project
The goal of the project is to determine to what extent, and under what conditions, all non-iterative logics have the interpolation property. Depending on the nature of the project, this can be a theoretical investigation leading up to a Phd, or a more practical approach where interpolants are actually computed.
Requirements/Prerequisites
Familiarity with basic concepts of (modal) logics. If a practical angle is pursued, additionally good programming skills. In any case, a keen interest in theoretical/logical questions.
Student Gain
Exposure to key concepts of modal logic and automated theorem proving.
Background Literature
Modal Logics in General:
Blackburn, de Rijke, Venema, Modal Logic, CUP.
Interpolation:
D. Pattinson, The Logic of Exact Covers: Completeness and Uniform Interpolation, Proc. LICS 2013.
