Dagstuhl Seminar 24341
Proof Representations: From Theory to Applications
( Aug 18 – Aug 23, 2024 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/24341
Organizers
- Carlos Areces (National University - Córdoba, AR)
- Anupam Das (University of Birmingham, GB)
- Elaine Pimentel (University College London, GB)
- Lutz Straßburger (INRIA Saclay - Île-de-France, FR)
Contact
- Marsha Kleinbauer (for scientific matters)
- Susanne Bach-Bernhard (for administrative matters)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Schedule
Dagstuhl Seminar 24341 was organized in response to growing interest in the representation of formal proofs. Its primary aim was to bring together theorists and practitioners who are exploring various proof representations, with the goal of identifying new applications while simultaneously creating new theoretical directions. A key focus of the seminar was to explore the interface between proof normalization and proof search traditions, by examining proof representations from both perspectives.
The seminar focused on the relation between various new developments in the field, including: the more philosophical direction of proof-theoretic semantics; the upcoming unifying research program of universal proof theory; and the study of non-standard proof formats, such as non-well--founded proofs. Individual talks covered a broad array of topics relevant to these developments, such as the particulars of certain variants on standard proof calculi (calculi including witness operators, calculi for inconsistent logics and logics with numerical quantification, calculi for second-order logic, and ``exotic'' proof calculi, e.g. labelled calculi for modal and intuitionistic logics), but also various connections of proof theory to computational applications (verification logic, propositional dynamic logic, tableaux using SAT solvers, and interactive theorem provers). To do justice to these complex topics, researchers from proof theory, computational logic, and philosophical logic were invited to collaborate and provide insights. The seminar also identified several research gaps across these areas. One important takeaway was the importance of utilizing different representations of proof systems to address emerging open questions in the field, and to prioritize the need for unification.
The seminar itself was structured to encourage extensive interaction among participants, both formally and informally. Participants were given considerable freedom in preparing their contributions and during the seminar itself, including the option to give talks in a variety of formats. Several in-depth special sessions were organized to focus on the most important developments in the field, and longer individual talks by experts covered specific topics in greater detail. Evening sessions, dubbed ``beer talks'', provided a relaxed environment for casual discussions, allowing participants to explore topics of shared interest and build connections across different areas of research.
The discussions from the seminar reflect the key interests of the community and provide valuable topics for ongoing research. At the end of the seminar, participants agreed to stay in contact to continue their discussions and foster new collaborations. Already various initiatives are being taken. For instance, Fernando Raymundo Velazquez Quesada, Carlos Olarte, and Elaine Pimentel began a promising collaboration on Epistemic Propositional Dynamic Logic following discussions at Dagstuhl. They recently held an in-person meeting in Bergen, Norway, and plan to apply for a European grant in the near future. Additionally, collaborations have among others been started by Lutz Straßburger and Revantha Ramanayake on modal logic, and by Lutz Straßburger and Matteo Acclavio on linear logic. We look forward to seeing how the results of these efforts will further shape the field.
Creative Commons BY 4.0
Areces, Anupam Das, Elaine Pimentel, and Lutz Straßburger
Proof theory is the study of formal proofs as mathematical objects in their own right. The subject has enjoyed continued attention among computer scientists in particular due to its significance for formalization, metalogic, and automation. In recent decades there has been a surge of interest on the representations of formal proofs themselves. The outcomes of these investigations have been remarkable, in particular extending the scope of structural proof theory to novel and richer settings:
- Richer line structures (e.g. hypersequents, nested sequents, labelled sequents) have resulted in a uniform treatment of standard modal logics, streamlining their metatheory and providing new tools for metalogical problems.
- Richer proof structures (e.g., cyclic proofs, annotated systems, infinitely branching proofs) have significantly advanced our understanding of fixed points and (co)induction. Indeed, we are now seeing many of these previously disjoint techniques being combined to push the boundaries of proof theoretic approaches to computational logic.
- Graphical proof representations (e.g., proof nets, atomic flows, combinatorial proofs) originating from “linear” logics, now not only comprise a well-behaved computational model for resource-sensitive reasoning, but also provide an impressively uniform treatment for logics across the board.
In fact, we are now seeing many of these previously disjoint techniques being combined to push the boundaries of proof theoretic approaches to computational logic, which has produced deep and fruitful cross-fertilizations between programming languages and proof theory. Arguably, the most well-known is the Curry-Howard correspondence (“propositions-as-types”) where (functional) programs correspond to formal proofs and their execution to normalization. A complementary tradition, proof-search-as-computation (“propositions-as-processes”), instead interprets (logic) programs to formulas and their execution to proof search.
The point of this Dagstuhl Seminar is twofold. First and foremost, we want to bring together theorists and practitioners exploiting proof representations to identify new directions of application and, simultaneously, distill new theoretical directions from problems “in the wild”. At the same time, this seminar will expose the interface between the proof-normalization and proof-search traditions by probing proof representations from both directions.
Carlos Areces, Anupam Das, Elaine Pimentel, and Lutz Straßburger
Please log in to DOOR to see more details.
- Matteo Acclavio (University of Southern Denmark - Odense, DK) [dblp]
- Bahareh Afshari (University of Gothenburg, SE) [dblp]
- Sara Ayhan (Ruhr-Universität Bochum, DE) [dblp]
- Eben Blaisdell (University of Pennsylvania - Philadelphia, US) [dblp]
- Yll Buzoku (University College London, GB) [dblp]
- Kaustuv Chaudhuri (INRIA Saclay - Île-de-France, FR) [dblp]
- Zhibo Chen (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Anupam Das (University of Birmingham, GB) [dblp]
- Abishek De (University of Birmingham, GB)
- Amy Felty (University of Ottawa, CA) [dblp]
- Alexander Gheorghiu (University College London, GB) [dblp]
- Marianna Girlando (University of Amsterdam, NL) [dblp]
- Rajeev P. Gore (Turner, AU) [dblp]
- Tao Gu (University College London, GB)
- Andrzej Indrzejczak (University of Lodz, PL) [dblp]
- Raheleh Jalali (The Czech Academy of Sciences - Prague, CZ) [dblp]
- Timo Lang (University College London, GB) [dblp]
- Anela Lolic (TU Wien, AT) [dblp]
- Bruno Lopes (Fluminense Federal University - Rio de Janeiro, BR) [dblp]
- Robin Martinot (Utrecht University, NL) [dblp]
- Dale Miller (INRIA Saclay - Île-de-France, FR) [dblp]
- Victor Nascimento (Universidade do Estado do Rio de Janeiro, BR)
- Sara Negri (University of Genova, IT) [dblp]
- Carlos Olarte (Université Sorbonne Paris Nord - Villetaneuse, FR) [dblp]
- Edi Pavlovic (LMU München, DE) [dblp]
- Elaine Pimentel (University College London, GB) [dblp]
- Ian Pratt-Hartmann (University of Manchester, GB) [dblp]
- Revantha Ramanayake (University of Groningen, NL) [dblp]
- Alexis Saurin (CNRS - Paris, FR) [dblp]
- Peter M. Schuster (University of Verona, IT) [dblp]
- Sana Stojanovic-Djurdjevic (University of Belgrade, RS) [dblp]
- Lutz Straßburger (INRIA Saclay - Île-de-France, FR) [dblp]
- Iris van der Giessen (University of Birmingham, GB) [dblp]
- Fernando Velázquez Quesada (University of Bergen, NO) [dblp]
- Heinrich Wansing (Ruhr-Universität Bochum, DE) [dblp]
- Richard Zach (University of Calgary, CA) [dblp]
Classification
- Artificial Intelligence
- Logic in Computer Science
- Programming Languages
Keywords
- proof theory
- proof calculi
- computational interpretations
- proof semantics
- dynamic operators
