View: session overviewtalk overviewside by side with other conferences
09:00  Welcome SPEAKER: Organizers 
09:05  Semantics and Proof Theory in Team Play: the case of Paraconsistent Logics SPEAKER: Anna Zamansky ABSTRACT. A useful modular semantics is an important property of any proof system: it can be used to characterize important syntactic properties of the system, provide insights into its underlying logic, and in many cases induce a decision procedure for it. Recent developments in the field of paraconsistent logics are an interesting case which exemplifies the crossfertilization between semantic explorations and proof theoretical developments. In this talk I will survey the framework of nondeterministic semantics and its prooftheoretical applications, and demonstrate how nondeterministic semantics pushed forward the development of analytic Gentzentype calculi for the large family of Logics of Formal Inconsistency. 
09:50  On the Construction of Analytic Sequent Calculi for Subclassical Logics SPEAKER: Ori Lahav ABSTRACT. We study the question of when a given set of derivable rules in some basic analytic propositional sequent calculus forms itself an analytic calculus. First, a general syntactic criterion for analyticity in the family of pure sequent calculi is presented. Next, given a basic calculus admitting this criterion, we provide a method to construct weaker pure calculi by collecting simple derivable rules of the basic calculus. The obtained calculi are analyticbyconstruction. While the criterion and the method are completely syntactic, our proofs are semantic, based on interpretation of sequent calculi via nondeterministic valuation functions. In particular, this method captures calculi for a wide variety of paraconsistent logics, as well as some extensions of Gurevich and Neeman's primal infon logic. 
10:45  Comparing Sequent Calculi via Hilbertstyle Axioms SPEAKER: Björn Lellmann ABSTRACT. In this talk I will consider the question of how to compare and evaluate the expressive strength of different formats of Gentzenstyle systems. More precisely, the general question is which logics can be captured in the different frameworks. Of course some results are clear: e.g. since every standard sequent can be seen as a hypersequent with only one component or as a nested sequent without the nesting, every logic which can be captured in the framework of standard sequent calculus can be captured in the framework of hypersequent or nested sequent calculi as well. Other results are given by explicitly translating one framework into another, see e.g. [Goré and Ramanayake:2012]. While such results certainly establish important connections between the different frameworks, they only provide information on the expressive strength of one Gentzenstyle framework relative to another one. Yet we are also interested in the absolute expressive strength and in particular the limits of what can be expressed in the different frameworks in a meaningful way. The qualification "in a meaningful way'' here is important, since of course given any set A of formulae the sequent calculus with groundsequents =>a for every a in A will serve to derive exactly the formulae in A, even in a cutfree way. Thus to make this question nontrivial we also need to restrict the format of the rules in the different frameworks. Comparing the different frameworks and formats of rules finally can be done by identifying characterisations for them in a single common framework. Since we would like to compare extensions of sequent calculus, this should be a framework outside the class of Gentzenstyle frameworks, and ideally the characterisations should provide a way of quickly determining which Gentzenstyle framework is suitable for a particular logic. For this purpose here we choose the framework of Hilbertstyle axiom systems. This gives a high degree of flexibility and allows in particular to capture nonnormal modal logics and logics based on other than classical propositional logic. A characterisation of a specific Gentzenstyle framework together with a specific format of rules then is given by an ideally purely syntactically defined class of axioms together with translations from rules of the considered format and framework into axioms of this class and vice versa. The prime example for this method is Kracht's result characterising those modal temporal logics which can be captured by structural rules in a display calculus satisfying Belnap's conditions for cut elimination as exactly the logics axiomatisable by primitive axioms [Kracht:1996]. Another example is the characterisation of structural rules in a sequent or hypersequent calculus for substructural logics by certain levels of the substructural hierarchy from [Ciabattoni et al:2008]. Apart from providing a first step for the construction of analytic calculi from Hilbert axioms, this method also yields a way to show limitative results: By showing that a certain logic cannot be axiomatised by axioms of a specific (syntactically given) form we can show that the logic cannot be captured by the framework and format of rules corresponding to this class of axioms. In this talk I will discuss some recent results in this spirit concerning logical rules of different formats in the frameworks of standard sequent calculi and hypersequent calculi. The logics under consideration are propositional modal logics such as Gödel Löb logic GL or the logic of 2transitive Kripke frames, and more generally, extensions of classical or intuitionistic propositional logic with additional not necessarily unary connectives. 
11:10  Sequent Systems for Classical Modal Logics SPEAKER: Paolo Maffezioli ABSTRACT. This paper develops sequent calculi for several classical modal logics. Utilizing a polymodal translation of the standard modal language, we are able to establish a base system for the minimal classical modal logic from which we generate extensions in a modular, and uniform, manner. We also briefly suggest potential applications to epistemic logic. 
11:35  Lyndon Interpolation for the Modal MuCalculus SPEAKER: Daniyar Shamkanov ABSTRACT. We prove Lyndon interpolation for the modal mucalculus by applying socalled circular proofs. One of the proof systems for the modal mucalculus is based on nonwellfounded derivation trees with a global condition which roughly says that in each infinite branch, there must be an outermost greatest fixed point unfolded infinitely many often. We analyse regular proof trees (socalled circular proofs) in this proof system and obtain the Lyndon interpolation for the modal mucalculus. 
12:00  On cuts and cutelimination in modal fixed point logics SPEAKER: Thomas Studer ABSTRACT. We present recent developments and discuss open questions concerning syntactic cutelimination for modal fixed point logics. 
12:25  Displaytype calculi and their cut elimination metatheorem SPEAKER: Giuseppe Greco ABSTRACT. The range of nonclassical logics has been rapidly expanding, driven by influences from other fields which have opened up new opportunities for applications. However, the hurdles preventing a standard prooftheoretic development for these logics are due precisely to some of their defining features which make them suitable for applications, such as e.g. their not being closed under uniform substitution, or the fact that (the semantic interpretations of) key connectives are not adjoints. These difficulties caused the existing proposals in literature to be often ad hoc, not easily generalisable, and more in general lacking a smooth prooftheoretic behaviour. In particular, the difficulty in smoothly transferring results from one logic to another is a problem in itself, since these logics typically come in large families (consider for instance the family of dynamic logics), and hence prooftheoretic approaches which uniformly apply to each logic in a given family are in high demand. In this talk we focus on the core technical aspects of a prooftheoretic methodology and setup closely linked to Belnap's display logic and Sambin's basic logic. The present setup, which we refer to as displaytype calculi, generalizes display calculi in two aspects: by allowing multitype languages, and by dropping the full display property. The generalisation to a multitype environment makes it possible to introduce specific tools enhancing expressivity, which have proved useful e.g. for a smooth prooftheoretic treatment of multimodal and dynamic logics. The generalisation to a setting in which full display property is not required makes it possible to account for logics which admit connectives which are neither adjoints nor residuals. One technical aspect which guarantees the cut elimination metatheorem to go through for displaytype calculi, even in the absence of the full display property, concerns the strengthening of the separation property (requiring principal formulas in introduction rules to appear in isolation) to the visibility property. Visibility requires all active formulas in introduction rules to occur in isolation. This property was recognized to be crucial for the cut elimination theorem of basic logic. However, in the present setup of displaytype calculi, visibility is also weakened, in the sense that, in order to account for logics that are not closed under uniform substitution, principal formulas in axioms are not required to occur in isolation. In the proposed talk, we will illustrate the basic principles of the multitype environment, and also how the above combination of weakenings, strengthenings of the separation property concurs to guaranteeing the cut elimination metatheorem for displaytype calculi. Time permitting, we will also discuss some difficulties that still arise in the case of PDL and some ideas towards treating predicative logics. 
14:30  Cyclic proof for quantitative logics SPEAKER: Alex Simpson ABSTRACT. I will talk about ongoing work with Matteo Mio (University of Cambridge) to build useful proof systems for quantitative fixedpoint logics. Our approach adapts cyclicproofbased sequent calculi to the quantitative setting. Several technical issues arise, not all of which have been resolved. The overall aim of the programme is to develop machinery for reasoning about probabilistic concurrent systems. But the talk will focus on prooftheoretic issues, in a purely logical setting. 
15:15  Modular Systems for Intuitionistic Modal Logics in Nested Sequents SPEAKER: Sonia Marin ABSTRACT. In this talk we show for each of the modal axioms d, t, b, 4, and 5 an equivalent set of inference rules in a nested sequent system, such that, when added to the basic system for the intuitionistic modal logic IK, the resulting system admits cut elimination. The result is similar to the one presented at "Gentzen Systems and Beyond 2011" about classical modal logics. We use a combination of structural and logical rules to achieve modularity. 
15:40  An Intuitionisticaly based Description Logic SPEAKER: Alexandre Rademaker ABSTRACT. This article presents iALC, an intuitionistic version of the classical description logic ALC, based on the framework for constructive modal logics presented by Simpson (1994) and related to description languages, via hybrid logics, by de Paiva (2006). This article corrects and extends the presentation of iALC appearing in de Paiva et al (2010). It points out the difference between iALC and the intuitionistic hybrid logic presented in de Paiva (2006). Completeness and soundness proofs are provided. A Sequent Calculus for iALC and a discussion on the computational complexity is taken. It is worth mentioning that iALC is used to formalize legal knowledge, and in fact, was specifically designed to this goal.

16:30  Link formulas in implication fragments of substructural logics SPEAKER: Tomasz Kowalski ABSTRACT. Two wellknown implication fragments of substructural logics are BCI (fragment of logic without contraction and weakening) and BCK (fragment of logic without contraction). The technique of link formulas was developed by the present author first for BCI, as a tool to solve an open problem. Then, a modification of the technique turned out to work for BCK and delivered a proof of its structural incompleteness. The technique can be used to obtain relatively easy proofs of admissibility of certain rules in BCK and BCI, yielding structural incompleteness proofs of several logics in the vicinity. I will present the technique in a uniform way, applicable to BCI and BCK, as well as to the implication fragments of the relevant logic R and the intuitionistic logic. Some applications (old and new) will be presented to illustrate the technique. 
16:55  A proof theoretic approach to standard completeness SPEAKER: Paolo Baldi ABSTRACT. We show extensions of the proof theoretic approach to standard completeness, based on the elimination of the density rule in suitable hypersequent calculi. 
17:20  On Affine Logic and Łukasiewicz Logic SPEAKER: Rob Arthan ABSTRACT. We report on a study of intutionistic fragments of Łukasiewicz logic. We present, in a structured human readable form, syntactic proofs of a number of important formulas originally found with the assistance of the Prover9 automated theorem prover. The identities include homomorphism properties that we put to work in an analysis of the double negation translations of Kolmogorov, Gödel, Gentzen and Glivenko. 
17:45  Simpler Proof Net Quantifiers: Unification Nets (Work in Progress) SPEAKER: Dominic Hughes ABSTRACT. Girard formulated an approach to proof net quantifiers over a series of three papers. Since the approach uses explicit witnesses for existential quantifiers, it suffers from two problems: limited proof identification and nonlocal cut elimination. This paper introduces a more abstract approach, unification nets, which solves these problems by leaving existential witnesses implicit: a unification net is merely an axiom linking. 