Unless stated otherwise, all talks will take place in room A97 of the Exakte Wissenschaft Building (ExWi) at the University of Bern.
Schedule
| Date | Time | Speaker | Title |
|---|---|---|---|
| 16.11.2023 | 13:30-15:00 | Borja Sierra-Miranda, University of Bern | Cyclic Proofs for iGL via Corecursion |
| 30.11.2023 | 13:30-15:00 | Nina Frasa | Relativized proofs and the P ≠ NP-conjecture (Bachelor Thesis) |
| 4.12.2023 | See at SGSLPS webpage | Mirna Džamonja | Logic Transfer Principles in Mathematics and Computer Science; Abstract Logics, Infinite and Finite Models |
| 7.12.2023 | 13:30-15:00 | Noah Maggio, Raphael Feer |
Analysing FastPay (Bachelor Thesis) Analysing Inter-Blockchain Communication (Bachelor Thesis) |
| 14.12.2023 | Set at APT webpage | - | Symposium: Advances in Proof Theory |
Abstracts
Cyclic Proofs for iGL via Corecursion
Borja Sierra-Miranda
Non-well founded proofs are a generalization of the traditional notion of proof. The main idea of this generalization is to allow proofs to have infinite height. Cyclic proofs are non-well founded proofs which can be described finitely by loops that repeat infinitely many times. Daniyar Shamkanov proved an equivalence between finitary, non-well founded and cyclic proofs for GL (provability logic) using corecursion. Rosalie Iemhoff extended this result to the intuitionistic case, without using corecursion. In this talk we prove the equivalence between finitary and cyclic proofs for intuitionistic GL keeping the corecursion method. In order to do this we will need to contract the sequents in the proof while performing the corecursion. We will discuss the differences that this produces from Shamkanov's original work and how we can try to extend it to other admissible rules, like cut. This last part is still a work-in-progress.