We introduce a new proof-theoretic framework which enhances the expressive power of bunched sequents by extending them with a hypersequent structure. We prove a general cut-elimination theorem that applies to bunched hypersequent calculi satisfying general rule conditions and then adapt the methods of transforming axioms into rules to provide cutfree bunched hypersequent calculi for a large class of logics extending the distributive commutative Full Lambek calculus DFLe and Bunched Implication logic BI. The methodology is then used to formulate new logics equipped with a cutfree calculus in the vicinity of Boolean BI.

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

This paper focuses on a globally sound but possibly locally unsound analytic sequent calculus for the quantifier macro Q. It is demonstrated that no locally sound analytic representation exists.

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq's constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem - in our case by a Minsky machine - is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway's FRACTRAN language as intermediate layer.

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

Over the course of more than two millennia, the philosophical school of Mimamsa has thoroughly discussed and analyzed the prescriptive portion of the Vedas, the sacred texts of Hinduism, in order to make sense of it as a consistent corpus of rules. We present a formalization of the deontic system applied by Mimamsa authors for resolving conflicts between normative statements by giving preference to the more specific ones. Finally, we show how to use the resulting system to provide a better understanding of these philosophical texts.

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

In this talk we discuss proof translations between labelled and label-free calculi for the logic of Bunched Implications (BI). We first consider the bunched sequent calculus LBI and define a labelled sequent calculus, called GBI, in which labels and constraints reflect the properties of a specifically tailored Kripke resource semantics of BI with two total resource composition operators and explicit internalization of inconsistency. After showing the soundness of GBI wrt our specific Kripke frames, we show how to translate any LBI-proof into a GBI-proof. Building on the properties of that translation we devise a tree property that every LBI-translated GBI-proof enjoys. We finally show that any GBI-proof enjoying this tree property (and not only LBI-translated ones) can systematically be translated to an LBI-proof.

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

Many substructural, intermediate and modal logics have found cut-free presentations in the hypersequent calculus. We demonstrate that for many such logics, this cut-freeness at the level of hypersequents also implies completeness with respect to a sequent system where only cuts of a certain shape are allowed. The restriction on the cuts thus obtained is often strong enough to allow for proofs of metalogical properties such as decidability, or embeddability into a weaker base logic. Our method also allows for a new proof of the fact that the modal logic S5 has a sequent calculus in which only analytic cuts are needed.

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

TBA

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

The logic of STIT (`seeing to it that') is an agency logic for reasoning about agents that make choices at certain moments in time. This class of modal logics has received considerable attention in the past decades with formal application in epistemic-, legal-, and deontic reasoning. Furthermore, in relation to the increasing development of autonomous systems assisting and interacting with humans, the need for automated normative reasoning with STIT logics has been stressed in the literature. Our present research addresses this issue. In this talk we will set out the concrete aims of our STIT project and discuss some of the results obtained so far. We will first provide an introduction to the logic of STIT and discuss our recently proposed Temporal Deontic extension STIT. Second, we provide labelled sequent calculi for the class of multi-agent STIT logic with limited choice axioms and show how these calculi can be refined with the use of propagation rules, enabling us to reduce the structure of sequents and to make the proofs more compact. For the class of refined calculi we obtain automated proof-search and counter-model extraction. We will conclude by discussing some open problems.

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

I shall expose recent advances on exploring the equaltional theories of the residuated lattices Q(C) made of join-continuous endofunctions of a complete chain C. On one side, when investating congruences, we observed that the number of idempotents in the residuated lattice Q({0,1,...,n}) is the 2n+1-th Fibonacci number. Our proof yields a combinatorial interpretation of results due to Howie and Laradji-Umar. If C is a finite chain or the interval [0,1] of the reals, Q(C) is an involutive residuated lattice. Generalizing this fact, we shall present the following result : for a complete lattice L, the residuated lattice Q(L) of join-continuous endofunctions of L is involutive if and only of L is a completely distributive lattice. Thus, the step from ILL to MALL requires, for those residuated lattices, also a classical structure on the additives. It also holds that Q(L) is an involutive mix residuated lattice if and only if L is a complete chain.

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

As follows from their name, tree-hypersequents (also known as nested sequents) were created to represent the tree structure of underlying Kripke models. While this approach works well on modal and intermediate logics complete w.r.t. many types of tree-like frames, it is not directly suited to encode quantitative restrictions on these frames, e.g., bounded depth and/or bounded number of children per node. In order to capture these restrictions, we add the injectivity condition to nested sequents requiring different sequent nodes to correspond to distinct worlds in the underlying Kripke model. The downside is the loss of the formula interpretation. On the plus side, we show how the injective nested sequents can be used to constructively prove the Craig interpolation property for all interpolable intermediate logics strictly between the intuitionistic and classical propositional logics that are complete with respect to tree-like models, i.e., Smetanich logic (also known as the logic of here and there), the greatest semiconstructive logic, logic BD_2 of bounded depth 2, and Gödel logic. For the last one, we obtain a stronger form of interpolation called Lyndon interpolation.

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

In this talk we look at how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. As a consequence of the extraction process, each nested calculus inherits favorable proof-theoretic properties from its associated labelled calculus.

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

Defeasible Logic is a simple practical computationally oriented (sceptical) non-monotonic formalism that proved (i) to be flexible to capture different facets of non-monotonic reasoning and (ii) to be extensible. The logic is based on a constructive proof theory. We are going to show to use the proof theory to extend the logic with modalities, and to capture some aspects of substructural logic. We also show how to use some of these features to address some paradoxes of deontic logic.

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

In this talk I will present a nested sequent system for a combination of (non-normal) monotone modal logic M and normal modal logic K. The system is fully internal, can be used for proof search, and is suitable for countermodel construction. I will also consider some deontic extensions and present a prototype implementation.

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

We develop semantically-oriented calculi for the cube of non-normal modal logics and some deontic extensions. The calculi manipulate hypersequents and have a simple semantic interpretation. Their main feature is that they allow for direct countermodel extraction. Moreover they provide an optimal decision procedure for the respective logics. They also enjoy standard proof-theoretical properties, such as a syntactical proof of cut-admissibility.

• Thematic program: Informatics and Logic (2019/2020)
• Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)