Modular Normalisation of Classical Proofs

Student thesis: Doctoral ThesisPhD


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 Award3 Apr 2019
Original languageEnglish
Awarding Institution
  • University of Bath
SupervisorJames Laird (Supervisor) & Alessio Guglielmi (Supervisor)


  • proof theory
  • deep inference
  • normalisation
  • propositional logic
  • first-order logic
  • herbrand's theorem

Cite this