View: session overviewtalk overviewside by side with other conferences
09:00  Title TBA  Invited talk ABSTRACT. Abstract TBA 
10:00  SPEAKER: Tim Lyon ABSTRACT. We begin with display and labelled calculi for a certain class of tense logics. These tense logics are extensions of Kt with any finite number of general path axioms, which are axioms of the form Xp > Yp, where X and Y represent sequences of black and white diamonds. For the minimal tense logic Kt, I provide a bidirectional embedding between display calculus proofs and labelled calculus proofs. It is then shown how to translate display proofs for Kt extended with general path axioms into labelled proofs. Providing a reverse translationtranslating labelled proofs into display proofs for Kt extended with general path axiomshas proven to be much more difficult because certain labelled structural rules do not correspond well to the display variants of such rules. Nevertheless, for a certain subclass of general path axioms a translation from labelled calculus proofs to display calculus proofs can be provided. Through the addition of special rules, referred to as "propagation rules," we can prove that the problematic structural rules are admissible in the resulting calculus. Every proof of a formula in this calculus contains sequents whose structure corresponds to a tree with two types of edges. This specific structure allows us to translate these proofs into display proofs, which gives an answer to an open question of translating labelled proofs to display proofs for extensions of the minimal tense logic Kt. 
11:00  SPEAKER: Tiziano Dalmonte ABSTRACT. We propose a minimal nonnormal intuitionistic modal logic. We present it by Hilbert axiomatisation and an equivalent cutfree calculus. We then propose a semantic characterisation of this logic in terms of bineighbourhood models with respect to which the logic is sound. We finally present a cutfree labelled calculus matching with the bineighbourhood semantics. 
11:30  Proof theory for quantified monotone modal logics SPEAKER: Eugenio Orlandelli ABSTRACT. This paper provides the first prooftheoretic study of quantified nonnormal modal logics. It introduces labelled sequent calculi for the first order extension, both with free and with classical quantification, of all the monotone nonnormal modal logics, as well as of some interesting extensions thereof, and it studies the role of the Barcan Formulas in these calculi. It will be shown that the calculi introduced have good structural properties: they have invertibility of the rules, heightpreserving admissibility of weakening and contraction, and syntactic cut elimination. It will also be shown that each of the calculi introduced is sound and complete with respect to the appropriate class of neighbourhood frames with either constant or varying domains. In particular the completeness proof constructs a formal proof for derivable sequents and a countermodel for underivable ones, and it gives a semantic proof of the admissibility of cut. Finally, some preliminay results on the extension of our approach to the nonmonotonic case are discussed. 
12:00  Sequent Calculi for Logic that Includes an Infinite Number of Modalities ABSTRACT. Multimodal logic has been studied for various purposes. 
14:00  Cyclic proofs, hypersequents and Kleene algebra  Invited Talk ABSTRACT. Logics arising from automaton theory, relational algebra and formal language theory are still not well understood in prooftheoretic terms. However, there is increasing evidence to suggest that emerging trends in structural proof theory, namely richer proof calculi and nonwellfounded proofs, possess the capacity to capture these fundamental frameworks, and even deliver important metalogical results of independent interest. In this talk I will speak about a recent line of work that uses a combination of internal calculi and cyclic proofs (arguably an external feature) to recover proof theoretic treatments for Kleene algebras (KA) and action lattices (AL). Starting with KA, I show how a natural sound and complete nonwellfounded system can be made regular via enriching the syntax of proof lines to hypersequents. This takes advantage of several basic techniques on the cyclic proof side as well as known normal forms from automaton theory, morally corresponding to the use of hypersequents. This calculus exhibits optimal proofsearch complexity and, as an application, I will briefly present work in progress on how to recover an alternative proof of the completeness of KA with respect to inclusions of rational languages. I will also speak about a proof theoretic account of AL, which is of natural interest to structural proof theorists since it extends the full Lambek calculus by a single fixed point: the Kleene star. The main result here is cutelimination, which requires a sophisticated computational interpretation into a higherorder language. As an application we are able to recover an (optimal) complexity bound for *continuous action lattices. The aim of this talk is to give a concrete showcase of modern trends structural proof theory, and moreover to leave the audience with some motivational problems for the area at large. At a highlevel, I also hope to explore a moral connection, in certain settings, between the richness of a proof calculus and succinct representations arising from automaton theory, which could direct a line of future research for the area.

15:00  Proof Translations in BI logic SPEAKER: Daniel Mery ABSTRACT. In order to study proof translations in BI logic, we consider first the bunched sequent calculus LBI and then define a new labelled sequent calculus, called GBI. Therefore we propose a procedure that translates LBI proofs into GBI proofs and prove its soundness. Moreover we discuss some steps towards the reverse translation of GBI proofs into LBI proofs and propose an algorithm that is illustrated by some examples. Further work will be devoted to its proof of correctness and also to the design of translations of LBI proofs to TBI (labelledtableaux) proofs. 
16:00  Intuitionistic multiagent subatomic natural deduction for belief and knowledge ABSTRACT. We outline a prooftheoretic approach to the semantics of intensional operators for intuitionistic belief and knowledge, which does neither intend to capture a given target modal logic, nor to import ideas from relational modeltheoretic semantics (e.g., truth at indices, accessibility between indices) via labelled and relational formulae into the language. On this approach, the meaning of these intensional operators is explained exclusively by appeal to the structure of proofs which are unaided by such means. The prooftheoretic framework chosen for this purpose is subatomic natural deduction proposed by the author in earlier work. The resulting systems normalize and enjoy the subexpression property (a refinement of the subformula property). They can be used for the logical analysis of reasoning patterns which involve complex multiagent belief constructions (e.g., reciprocating or universal beliefs).

16:30  SPEAKER: Marianna Girlando ABSTRACT. The logic of Conditional Beliefs (CDL) has been introduced by Board, Baltag and Smets to reason about knowledge and revisable beliefs in a multiagent setting. Our aim is to develop standard internal calculi for this logic. As a preliminary result we propose an internal hypersequent calculus for it in the single agent case. 
17:00  SPEAKER: Camillo Fiorentini ABSTRACT. The inverse method is a saturation based theorem proving technique; it relies on a forward proofsearch strategy and can be applied to cutfree calculi enjoying the subformula property. Here we apply this method to derive the unprovability of a goal formula G in Intuitionistic Propositional Logic. To this aim we design a forward calculus FRJ(G) for Intuitionistic unprovability which is prone to constructively ascertain the unprovability of a formula G by providing a concise countermodel for it; in particular we prove that the generated countermodels have minimal height. Moreover, we clarify the role of the saturated database obtained as result of a failed proofsearch in FRJ(G) by showing how to extract from such a database a derivation witnessing the Intuitionistic validity of the goal. 