Modular Normalisation of Classical Proofs

Abstract

The main contribution of this thesis is to present a study of two normalisation theorems and proofs in classical logic: one propositional, one first-order. For propositional logic, we show a local cycle removal procedure through reductions on merge contractions that ensures that proofs can be decomposed—that contractions can be pushed to the bottom of a proof—in a straightforward way. For first-order logic, we show how decomposition of proofs can correspond to two presentations of Herbrand’s Theorem, and how we can use translations into expansion proofs to give a new, indirect cut elimination theorem for first-order logic.
In addition, an old but interesting cut elimination method for propositional logic, the experiments method, is formally presented for the first time, and we extend the theory of merge contractions to first-order logic.

Date of Award	3 Apr 2019
Original language	English
Awarding Institution	University of Bath
Supervisor	James Laird (Supervisor) & Alessio Guglielmi (Supervisor)