 |  |  |
 |  |  |
2023 Workshop on Proof Theory and its Applications
When: From Thursday, July 13 until Friday, July 14, 2023.
Venue: Faculty of Mathematics and Informatics, University of Barcelona: Gran Via de les Corts Catalanes, 585, 08007 Barcelona.
Overview:
The 5th International Workshop on Proof Theory and its Applications will take place the 13th and 14th of July 2023 in Barcelona, Spain, under the auspices of the Proof Society. The workshop will bring together researchers on proof theory and its applications through a programme based on invited and contributed talks 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.
We invite proposals for contributed talks at the workshop. These can be on published or unpublished work, as well as work in progress. The best talk presented by a student will receive an award from The Proof Society.
The Workshop will be co-located with the 5th Proof Society Summer School. The location of the Workshop is the historical building of the Faculty of Mathematics and Informatics which belongs to the Universitat de Barcelona, at the heart of the city.
- Registration details can be found here.
Registration closes: June 26th, Extended to July 2th AoE.
Previous editions can be found at the Proof Society webpage.Programme:
Please download the workshop programme and schedule here.The duration of invited talks is expected to be 1 hour and the duration of contributed talks is expected to be 20 minutes, both including Q&A. There would be parallel sessions for the talks in rooms B5 and B6 of the Faculty of Mathematics and Informatics, University of Barcelona (see Contact & Travel Info).
| Authors | Contributed talks | Schedule label |
|---|---|---|
| Sayantan Roy | Rule-Elimination Theorems | S1 |
| Gianluca Curzi and Anupam Das | Computational expressivity of (circular) proofs with fixed points | PC3 |
| Giti Omidvar and Lutz Straßburger | Combinatorial Flows | ML4 |
| Gabriele Buriola and Andreas Weiermann | Ordinal Analysis of Labelled Kruskal’s Theorem | O2 |
| Hina Kosaihira, Yuta Takahashi and Daisuke Bekki | Implementation of Anaphora Resolution Using the Refine Tactic of Coq | CS/LL1 |
| Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales and Lutz Straßburger | To prove or not to prove that IS4 | ML3 |
| Giovanni Solda | A natural combinatorial principle that is weak over weak theories yet strong over strong theories | O1 |
| Mojtaba Mojtahedi | Reduction of arithmetical completenesses | PL1 |
| Will Stafford | The Proof-Theoretic Criteria of Logic and the Logicality of Arithmetic | P1 |
| Sam Buss and Emre Yolcu | Regular resolution effectively simulates resolution | PC1 |
| Stepan Kuznetsov | Proof Disbalancing for Proving Complexity Results: Towards Infinitary Focusing | CS/LL2 |
| Sofía Santiago Fernández and Joost J. Joosten | Tree rewriting system for RC | PL3 |
| Matteo Acclavio, Davide Catta, Federico Olimpieri and Lutz Straßburger | Proof Equivalences in Constructive Modal Logic | S2 |
| Takahiro Yamada | Completeness Proof of Strict Finitistic Predicate Logic | P2 |
| Piotr Gruza | The structure of the definability relation between definitions of truth | A3 |
| Edi Pavlovic and Norbert Gratzl | Neutral free logic: Proof theory and its applications | S3 |
| Robin Martinot | (The philosophy of) translating first-order natural deduction proofs | P3 |
| Mojtaba Mojtahedi, Fedor Pakhomov, Philipp Provenzano and Albert Visser | Reflection and Induction for subsystems of HA | A2 |
| Maciej Głowacki | Implicit Commitments, Reflection, and Believability | A1 |
| Fedor Pakhomov, Albert Visser and Juvenal Murwanashyaka | There are no minimal essentially undecidable theories | A3 |
| Konstantinos Papafilippou and David Fernández | Succinctness of the fixed point theorem for GL | PL2 |
| Raheleh Jalali | Surprising or Predictable? Weak Systems Have Hard Theorems | PC2 |
| Alakh Dhruv Chopra and Fedor Pakhomov | Finite Labeled Trees Ordered By Non-Inf-Preserving Embeddings | O3 |
| Anupam Das, Abhishek De and Alexis Saurin | On the complexity of muMALL proof systems | CS/LL3 |
| Anupam Das and Sonia Marin | On intuitionistic diamonds (and lack thereof) | ML2 |
| Anupam Das, Iris van der Giessen and Sonia Marin | Towards Intuitionistic Gödel-Löb Logic (with a capital ‘I’) | ML1 |
Schedule:
The Workshop takes place in rooms B5 and B6 of the Faculty of Mathematics and Informatics, University of Barcelona (see Contact & Travel Info).
| Thursday, July 13 | Room B5 | Room B6 | |
|---|---|---|---|
| 9:20 - 9:50 | Registration | ||
| 9:50 - 10:00 | Opening | ||
| 10:00 - 11:00 | Ramsey-theoretic principles and proof size in second-order arithmetic - Leszek Kolodziejczyk | ||
| 11:00 - 11:30 | Coffe break | ||
| Modal Logic contributed talks | Arithmetic contributed talks | ||
| 11:30 - 11:50 | ML1 | A1 | |
| 11:50 - 12:10 | ML2 | A2 | |
| 12:10 - 12:30 | ML3 | A3 | |
| 12:30 - 12:50 | ML4 | A4 | |
| 12:50 - 15:00 | Lunch | ||
| Provability logic contributed talks | Structural Proof theory contributed talks | ||
| 15:00 - 15:20 | PL1 | S1 | |
| 15:20 - 15:40 | PL2 | S2 | |
| 15:40 - 16:00 | PL3 | S3 | |
| 16:00 - 16:30 | Coffee break | ||
| 16:30 - 17:30 | Automatability and Weak Automatability of Propositional Proof Systems - Maria Luisa Bonet | ||
| 17:30 - 17:40 | Pause | ||
| 17:40 - 18:40 | TPS AGM |
| Friday, July 14 | Room B5 | Room B6 | |
|---|---|---|---|
| 10:30 - 11:30 | Bounded Arithmetic and a Consistency Result for NEXP not contained in P/poly - Sam Buss | ||
| 11:30 - 12:00 | Coffee break | ||
| Proof complexity contributed talks | Philosophy contributed talks | ||
| 12:00 - 12:20 | PC1 | P1 | |
| 12:20 - 12:40 | PC2 | P2 | |
| 12:40 - 13:00 | PC3 | P3 | |
| 13:00 - 15:00 | Lunch | ||
| CS and Linear Logic contributed talks | Orderings contributed talks | ||
| 15:00 - 15:20 | CS/LL1 | O1 | |
| 15:20 - 15:40 | CS/LL2 | O2 | |
| 15:40 - 16:00 | CS/LL3 | O3 | |
| 16:00 - 16:40 | Coffee break (+ deliberations of the jury) | ||
| 16:40 - 17:30 | Best Student Award delivery + closing |
SUBMISSION INFORMATION:
You may submit your proposals for contributed talks to the conference management system EasyChair . The length of your abstract should not exceed four pages. Contributed talks are expected to last 20 minutes, including Q&A. Please upload your abstract as a PDF. After submission, authors of accepted manuscripts will be required to provide a tex file, using the template that can be downloaded here, so that we can compile a book of abstracts. Authors are required to use this template at the time of submission.Please be aware of the following deadlines related to proposal submissions:
- Extended abstract submissions deadline: May 15th, Extended to May 22th, AoE
- Acceptance notification: June 5th
Speakers
Confirmed invited speakers:
- Leszek Aleksander Kołodziejczyk (Institute of Mathematics, University of Warsaw) : Ramsey-theoretic principles and proof size in second-order arithmetic;
- Maria Luisa Bonet (Technical University of Catalonia) : Automatability and Weak Automatability of Propositional Proof Systems;
- Samuel R. Buss (University of California) : Bounded Arithmetic and a Consistency Result for NEXP not contained in P/poly.
Talks
Abstracts:
Posters:
Posters designs by Isabel Hortelano Martín, June 2023.
Committee
| Program Committee | |
|---|---|
| Bahareh Afshari, University of Gothenburg | |
| Albert Atserias, Technical University of Catalonia | |
| Matthias Baaz, Technical University of Wien | |
| Arnold Beckmann, Swansea University | |
| Lev D. Beklemishev, Steklov Mathematical Institute of Russian Academy of Sciences | |
| Ilario Bonacina, Technical University of Catalonia | |
| David Fernández-Duque, Universitat de Barcelona (chair) | |
| Balthasar Grabmayr, University of Haifa | |
| Rosalie Iemhoff, Utrecht University | |
| Joost J. Joosten, Universitat de Barcelona (chair) | |
| Antonina Kolokolova, Memorial University of Newfoundland | |
| Brett McLean, Ghent University (contributed program chair) | |
| Cosimo Perini Brogi, IMT School for Advanced Studies Lucca | |
| Norbert Preining, Mercari Inc., Japan | |
| Sofía Santiago-Fernández, Universitat de Barcelona | |
| Andreas Weiermann, Ghent University |
| Local Organising Committee | |
|---|---|
| Albert Atserias, Technical University of Catalonia | |
| Ilario Bonacina, Technical University of Catalonia | |
| David Fernández-Duque, Universitat de Barcelona (chair) | |
| Damiano Fornasiere, Universitat de Barcelona | |
| Petia Guintchev, Universitat de Barcelona | |
| Isabel Hortelano Martín, Universitat de Barcelona | |
| Joost J. Joosten, Universitat de Barcelona (chair) | |
| Miriam Kurtzhals, Universitat de Barcelona | |
| Miguel Martins, Universitat de Barcelona | |
| Tommaso Moraschini, Universitat de Barcelona | |
| Vicent Navarro Arroyo, Technical University of Catalonia | |
| Sofía Santiago-Fernández, Universitat de Barcelona |
Contact & Travel Info
The Workshop will be held in parallel sessions in both rooms B5 and B6 of the Faculty of Mathematics and Informatics, University of Barcelona: Gran Via de les Corts Catalanes, 585, 08007 Barcelona.
Useful phone numers:
- Citizen inquiries: 012
- Emergency: 112
- Health related issues: 061
For questions please contact one of the Local Organising Committee members.
Social Events
There will be a social dinner which will take place Thursday 13th July evening in En Ville restaurant.