# 2021 Workshop on Proof Theory and its Applications

The **3rd Workshop on Proof Theory and its Applications** will take place from **Dec 2 to Dec 4** at the University of Madeira under the auspices of the Proof Society and is organized by the Kurt Gödel Society.

The workshop will bring together researchers on proof theory and its applications through a series of invited and contributed talks as well as panel discussion, aiming to fulfil the mission of The Proof Society:

*To support the notion of proof in its broadest sense, through a series of suitable activities; to be therefore inclusive in reaching out to all scientific areas which consider proof as an object in their studies; to enable the community to shape its future by identifying, formulating and communicating it most important goals; to actively promote proof to increase its visibility and representation.*

The Workshop will be co-located with the 3rd Proof Society Winter School.

#### Invited Speakers

Eduardo Fermé (Madeira)

David Fernández Duque (Ghent)

Fedor Pakhomov (Ghent)

Stepan Kuznetsov (Moscow)

Michael Rathjen (Leeds)

###### Special outreach speaker

Andrei Voronkov (Manchester)

#### Contributed Talks

Submission of abstracts for the workshop is closed!

The duration of the contributed talks will be 30 minutes, including questions.

**At least one author per submitted abstract has to be registered.**

More details on the registration page.

#### Schedule

###### Thursday, Dec 2

time | Speaker | Title |
---|---|---|

9.10 - 10.00 | David Fernández Duque | Giant Steps for Goodstein Walks |

10.00 - 10.30 | Robin Martinot | Purity for formal proofs: when does a proof belong to the content of a theorem? |

10.30 - 11.00 | Avgerinos Delkos | Proof Complexity of Positive Branching Programs |

11.00 - 11.30 | coffee break | |

11.30 - 12.00 | Dominik Wehr | Abstract Cyclic Proofs |

12.00 - 12.30 | Guillermo Menéndez Turata | Uniform interpolation from cyclic proofs |

12.30 - 13.00 | Jan Rooduijn | Making infinitary annotated proofs concise |

13.00 - 14.30 | lunch break | |

14.30 - 15.20 | Eduardo Fermé | Belief Change with Limits of Credibility |

15.30 - 16.00 | Michael Bernreiter | Sequent Calculi for Choice Logics |

16.00 - 16.30 | coffee break | |

16.30 - 17.00 | Mikheil Rukhaia | A Fuzzy Logic with Sequence Variables and Flexible-arity Symbols |

17.00 - 17.30 | Esaïe Bauer | Provability of Functionnal Reactive Programming type system |

17.30 - 18.00 | Johannes Kloibhofer | A Fixed-point Theorem for Horn Formula Equations |

###### Friday, Dec 3

time | Speaker | Title |
---|---|---|

9.00 - 9.30 | Jannik Vierling | Some observations on induction in saturation theorem proving |

9.30 - 10.00 | Lorenzo Sauras-Altuzarra | Divisibility criteria for Fermat numbers |

10.00 - 10.30 | Iris van der Giessen | Proof Theory for the Admissible Rules in Lax Logic |

10.30 - 11.00 | Takahiro Yamada | A Reconstruction of Strict Finitistic First-Order Logic |

11.00 - 11.30 | coffee break | |

11.30 - 12.00 | Matteo Tesi | Terminating calculi for a class of intermediate logics |

12.00 - 12.30 | Ana Borges | QRC_1 in Coq, Formalizing a quantified modal logic |

12.30 - 13.00 | Jan Bydzovsky | A non-arithmetical Gödel Logic |

13.00 - 14.30 | lunch break | |

14.30 - 15.20 | Stepan Kuznetsov | Complexity of Logics with Kleene Star |

15.30 - 16.00 | Konstantin Shishov | Logical Calculus for Effect Algebras |

16.00 - 16.30 | coffee break | |

16.30 - 17.00 | Katarzyna W. Kowalik | A non-speedup result for the chain-antichain principle over a weak base theory |

17.00 - 17.30 | Pablo Dopico | What’s so special about ε_0? Making sense of the boundaries of finite mathematics |

17.30 - 18.00 | Best Student Presentation Award |

###### Saturday, Dec 4

time | Speaker | Title |
---|---|---|

9.00 - 9.50 | Fedor Pakhomov | Fast growing hierarchy, ordinal collapsing functions, and Π¹₁-CA₀ |

10.00 - 10.30 | Joost J. Joosten | Finite for some practical purposes |

10.30 - 11.00 | Marianna Girlando | Cyclic Hypersequents for Transitive Closure Logic |

11.00 - 11.30 | coffee break | |

11.30 - 12.00 | Allard Tamminga | Two-sided sequent calculi for FDE-like four-valued logics |

12.00 - 12.30 | Will Stafford | Decidability of proof-theoretic validity |

12.30 - 13.00 | Gianluca Curzi | Cyclic Implicit Complexity |

13.00 - 13.30 | Matteo Acclavio | An Analytic Proof System on Graphs |

13.30 - 14.00 | coffee and closing |

###### Best Student Presentation Award

The best student presentation based on scientific content and quality of the presentation will be selected from the contributed talks. The winner will be awarded a certificate and a Kurt Gödel medal.

#### Program Committee

Bahareh Afshari, University of Gothenburg

Matthias Baaz, TU Wien (chair)

Arnold Beckmann, Swansea University

Lev D. Beklemishev, Steklov Mathematical Institute

Balthasar Grabmayr, Humboldt University of Berlin

Rosalie Iemhoff, Utrecht University

Joost Joosten, University of Barcelona

Antonina Kolokolova, Memorial University of Newfoundland

Anela Lolic, TU Wien

Norbert Preining, Fujitsu

Andreas Weiermann, Ghent University

#### Organizing Committee

Nino Antidze

Matthias Baaz (co-chair)

Ketevan Gognadze

Benedikt Hartl

Joost Joosten

Anela Lolic (co-chair)

Ilma Lolic

Eduardo Marques

Maurício Reis

Vesna Sabljakovic-Fritz