Theses

Representation Matters in Cyclic Proof Theory

Type: Licentiate thesis
Supervisors: Graham E. Leigh and Bahareh Afshari
Digital copy: Available on GUPEA

A compilation thesis, consisting of two research articles, exploring cyclic proof theory from the perspective of proof representation, and an accompanying kappa.

More details here.

An Abstract Framework for the Analysis of Cyclic Derivations

Type: Master’s thesis
Supervisor: Bahareh Afshari
Digital copy: Available on the ILLC eprints server

We propose a categorical framework characterizing the traces through the pre-proofs of cyclic proof systems. This allows many aspects of cyclic proof theory to be studied in a general manner.

More details here.

A Constructive Analysis of First-Order Completeness Theorems in Coq

Type: Bachelor’s thesis
Advisors: Dominik Kirst and Yannick Forster
Supervisor: Gert Smolka

We mechanize various completeness results for first-order logic in the interactive theorem prover Coq. The focus is on pinning down when and which non-constructive principles are needed to obtain these results.

More details here.