Peter Chapman

at St Andrews

Addresses:

Paper Mail:
Room 1.11,
School of Computer Science,
University of St Andrews,
North Haugh, ST ANDREWS, Fife, KY16 9SX, Scotland.

Email: pc at cs.st-andrews.ac.uk

Phone: +44-1334-461639
Fax: +44-1334-463278 (work)

Proof theory, type theory, logic programming and automated reasoning. I am a member of the British Logic Colloquium, and an associate member of the London Mathematical Society. Click here for a poster displaying in more detail my research interests, whilst click here for my poster from a second year internal review. In the summer of 2007, I attended the TYPES Summer School 2007, whilst in April 2008, I attended the Midland Graduate School.

• A Formalised Proof of Craig's Interpolation Theorem in Nominal Isabelle. A paper and proof script, March 2008. Accepted for AISC 2008. (pdf), (proof script).
• Syntactic Conditions for Invertibility in Sequent Calculi. A paper, October 2008. Accepted for CATS 2009. (pdf), but had to be withdrawn owing to insufficient funding for my attendance

• An Automatic Prover for Sequent Calculus in Isabelle. A brief report on a small automatic proof tool to be used in Isabelle for a few calculi, and the theory files, March 2007. Report, G3cp, G3ip, G4ip.

• Mechanising Craig's Interpolation Theorem for Intuitionistic Logic in Isabelle. A report on the adaptation of Ridge's proof for the classical case, along with the proof script, May 2007. Report, Proof Script.

• A Formalised Proof of Cut admissibility for G3ip in Isabelle. There are two different Isabelle scripts, one which uses multisets, and one which uses sets for the contexts. A brief report on the differences between them can be found here. March 2008.

• A formalisation of Contraction admissibility for G4ip, May 2008. The two proof scripts show two different structures for the main proof, and the report details the differences between them. (proof script), (proof script), (report).

• Some lemmata for invertibility, July 2008. Some thoughts on syntactic conditions for a set of rules which will ensure the invertibility of those rules. (pdf) An updated version is here. The propositional results are formalised in these two files: (Definitions),(Theorems), whereas the first-order results are formalised in these two files: (Definitions),(Theorems). Most of these files have been superseded by those found here.

• Cut Elimination in G3i. A talk I gave for the Computational Logic Seminars in St Andrews, Nov 2006. (pdf)

• Cut Elimination in Sequent Calculi. A talk I gave at a Reading Party, Jan 2007. (pdf)

• A Formalised Proof of Craig's Interpolation Theorem in Nominal Isabelle. A talk for the University of St Andrews Computational Logic Seminar series, Jan 2008. (pdf).

• Constructive Mathematics and an Interpolation Result. A talk for a reading party, Jan 2008. The same talk was used for a talk given in the Mathematics Department of the University of St Andrews for the Pure Postgraduate Seminar series, Feb 2008.(pdf).

• A Formalised Proof of Craig's Interpolation Theorem in Nominal Isabelle. A talk given at the Technical University of Munich, which I visited for a week, Feb 2008. (pdf).

• Syntactic Conditions for Invertibility in Sequent Calculi. A talk given at the Structural Proof Theory workshop in Paris, November 2008. (pdf).

• Formalising Gentzen-style proof theory. A talk given at the Gentzen Centenary Symposium event in St Andrews, November 2009. (pdf).

• Annual Report. A copy of my first year annual report, submitted in May 2007. (pdf).

• Thesis Outline. A copy of my thesis plan, written 2½ years into my PhD, December 2008. (pdf).

• Algorithmic Game Theory in Communication Networks. MSc Dissertation, Sep 2005. Supervised by Prof. Luke Ong.