Dr Jeremy Dawson

Research Fellow

jeremy.dawson@anu.edu.au

Bio
Research interests

Now (2022) recently retired, for 24 years I was at the Logic and Computation Group in the Research School of Information Sciences and Engineering at the Australian National University, subsequently in the Research School of Computer Science, part of the College of Engineering and Computer Science.

My work was primarily using computer theorem provers, Isabelle, HOL4 and Coq, to prove meta-logical results, mostly cut-admissibility theorems, and also results in the area of term-rewriting and its termination.

Formal verification; Automated theorem proving, especially in relation to metalogic and cut-elimination, termination of term-rewriting; Functional programming.

Research Description

My current research is directed towards proving the interpolation property for Propositional Dynamic Logic, or establishing that it does not hold. To this end, I have formalised the proof of interpolation for the display calculus for classical propositional logic, and tried (unsuccessfully) to extend this particular proof method to tense logic.