Mechanised Foundations of Proof Calculi

Many applications of logic in computer science require deciding automatically whether a formula follows logically from some assumption formulae using a proof-calculus of proof-rules. The proof-rules themselves are proved correct manually but such meta-level proofs are error prone and difficult since the proof-rules reflect the complexity of modern programming languages. We will develop a general methodology for proving the correctness of many different proof-calculi used by academic researchers and developers of commercial software verification tools. We will verify our methodology by developing self-checking computer code which will be usable via the Internet so non-specialists can prove properties of their own proof-calculi.