This workshop is the fourth in a series of meetings that brings together researchers in different areas of proof theory. The main interest is in new algebraic and geometric results in proof theory which expand our abilities to manipulate proofs, help to reduce bureaucracy in deductive systems, and ultimately lead to new methods for proof search and new kinds of proof certificates.
There have been three previous editions of Structures and Deduction, the last of which occurred in 2014. Since then there has been a tremendous amount of progress in the area, witnessed by multiple recent funded projects. As well as theoretical work in the form of regular papers, we encourage submission of implementations, tools and system descriptions.
Themes of the workshop include but are not limited to:
The up-to-date workshop programme is available on the FSCD main programme page. To view it, select the box for "SD".
The conference will be held in Lecture Theatre B at the Department of Computer Science, University of Oxford.
We do not intend to have published proceedings, as we encourage people to present work in progress, or material that is already submitted. If there is a strong demand among the participants we may organise a special issue of an open access journal for full papers.
Almost all modal logics are well-known to admit finite cut-free sequent calculi with modal mu-calculus being a notable exception. This calculus extends the basic modal logic K by least and greatest fixed points for all monotone propositional operators. I will present a finitary cut-free axiomatisation for the mu-calculus that features a strengthening of the standard induction rule for greatest fixed point. The system is readily seen to be sound and its completeness is established by utilising a novel calculus of circular proofs which will also be discussed. Furthermore, I will look at how these new calculi relate to Kozen’s original axiomatisation (1983) and the semi-formal system of Jaeger, Kretz and Studer (2008).
Notions of circular or infinitary (non-well-founded) deductive systems naturally arise when one considers fixed point logics, and they have been used for decades in tableaux and sequent calculi for various mu-calculi. However, it is only much more recently that these notions have entered the realm of proofs as computations. In other words, circular proofs have generally been used as an algorithmic trick rather than a proper proof theoretic notion. In this talk, I will describe a general infinitary proof theory. I will attempt to illustrate its beauty and usefulness through various results: cut elimination, translation to finitary proofs, connections with infinite automata theory and completeness for the the linear-time mu-calculus. I will also describe several questions that remain to be explored.
We study a way of expressing all provably total maps of second order arithmetic, which is a possible alternative to system F and to the use of polymorphism. We propose a system we call system N, including data types for well-founded trees, and a recursion schema for data types and all simple types. The recursion schema in system N defines maps on a given data type D and a structure S. The schema simultaneously defines a total map on all possible extensions of the structure S and of the data type D. The schema is used to interpret impredicative definitions in second order arithmetical proofs. In system N we program by extending data structures and maps, in a way which we could be closer to real programming than the use of the entire polymorphism available in system F.
Bi-Intuitionistic Linear Logic (BILL) is an extension of Intuitionistic Linear Logic with a par, dual to the tensor, and subtraction, dual to linear implication. It is the logic of categories with a monoidal closed and monoidal co-closed structure that are related by linear distributivity, a strength of the tensor over the par. It conservatively extends Full Intuitionistic Linear Logic (FILL), which includes only the par.
Giving a satisfying proof-theoretic account of FILL has proven hard. The natural sequent rules do not give cut-elimination, and a relational annotation to the rules is needed.
In this talk I will discuss proof nets for the multiplicative, unit-free fragment MBILL that are canonical for the semantics: proof nets in normal form correspond one-to-one to categorical maps. This gives a pertinent interpretation of the relational annotation, as connectedness in the proof net. Correctness is by local rewriting in the style of Danos contractibility, which directly gives sequentialization into the relational sequent calculus. I will also present a second, geometric condition, via Danos-Regnier switching.
This is joint work with Gianluigi Bellin.
Modal logics have been extensively used for representing and reasoning about complex computational systems. The reasoning tasks for those logics are, however, far from trivial: the local and global satisfiability problems for the basic multimodal propositional logic K are PSPACE-complete and EXPTime-complete, respectively. Given the inherent intractability of the reasoning problems and also the wide range of applications to which those logics can be applied, the development of automatic, efficient tools for theorem proving is highly desirable. In this talk, we will discuss some successful strategies for classical theorem-proving and how they can be adapted for the modal case. We will also report on successful techniques for a resolution-based calculus we have recently developed and implemented for those logics.
In this talk I'll introduce the notion of expansion tree for linear logic. As in Miller's original work, we have a shallow reading of an expansion tree that corresponds to the conclusion of the proof, and a deep reading which is a formula that can be proved by propositional rules. We focus our attention to MLL2, and we also present a deep inference system for that logic. This allows us to give a syntactic proof to a version of Herbrand's theorem.
All questions about submissions should be addressed to firstname.lastname@example.org, or directly to one of the co-chairs.