Student research opportunities
Formalised Cut Elimination Proofs
Project Code: CECS_888
This project is available at the following levels:
CS single semester, Honours, Summer Scholar, Masters, PhD
Keywords:
Modal Logic, Proof Theory, Theorem Proving
Supervisors:
Professor Rajeev GoreDr Dirk Pattinson
Outline:
Theorem provers are devices that scrutinize, and certify, mathematical proofs. We want to use theorem provers to get certainty about proofs about proofs: we want to formalise, in a theorem prover, certain meta-statements (in particular cut elimination) about modal logics.
Goals of this project
To obtain a fully certified proof of cut elimination for a range of rank-1 logics. This will be achieved by instantiating an already formalised meta-theorem, together with (formalised) proofs that the prerequisites of the meta-theorem are met.
Requirements/Prerequisites
Keen interest in theoretical aspects, knowledge in (modal) logic. Experience in theorem proving can be aquired on the way.
Student Gain
Very good understanding of applied proof theory, experience in theorem proving environments.
Background Literature
Background on Modal Logics:
Blackburn, de Rijke, Venema. Modal Logic, CUP 2008.
Meta-theorem on Cut Eliminatin:
Pattinson and Schröder. Cut elimination in coalgebraic
logics. Information and Computation, 208:1447-1468, 2010
