Back to Search
Start Over
Modular normalisation of classical proofs
- Publication Year :
- 2019
- Publisher :
- University of Bath, 2019.
-
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.
Details
- Language :
- English
- Database :
- British Library EThOS
- Publication Type :
- Dissertation/ Thesis
- Accession number :
- edsble.774182
- Document Type :
- Electronic Thesis or Dissertation