Wolfgang Pauli Institute (WPI) Vienna

Home WPI in a nutshell Practical Information Events People WPI Projects
Login Thematic Programs Pauli Fellows Talks Research Groups

Informatics and Logic (2019/2020)

Organizers: Agata Ciabattoni (WPI c/o TU Wien), Vera Fischer (WPI c/o U. Wien), Laura Kovacs (WPI c/o TU Wien), Stefan Szeider (WPI c/o TU Wien), Stefan Woltran (WPI c/o TU Wien)

Talks


Revantha Ramanayake (TU Wien) WPI, OMP 1, Seminar Room 08.135 Mon, 1. Jan 01, 0:00
Bunched Hypersequent Calculi for Distributive Substructural Logics (with Agata Ciabattoni)
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)

Matthias Baaz (TU Wien) WPI, OMP 1, Seminar Room 08.135 Mon, 11. Nov 19, 9:40
Note on Globally Sound Analytic Calculi for Quantifier Macros (joint work with Anela Lolic)
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)

Dominique Larchey-Wendling (LORIA - CNRS) WPI, OMP 1, Seminar Room 08.135 Mon, 11. Nov 19, 11:00
Hilbert's Tenth Problem in Coq (joint work with Yannick Forster)
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)

Francesca Gulisano (Scuola Normale Superiore, Pisa) WPI, OMP 1, Seminar Room 08.135 Mon, 11. Nov 19, 11:45
Resolving conflicting obligations in Mimamsa: a sequent-based approach
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)

Daniel Mery (LORIA - Université de Lorraine) WPI, OMP 1, Seminar Room 08.135 Mon, 11. Nov 19, 14:30
Relating Labelled and Label-Free Bunched Calculi in BI Logic (joint work with Didier Galmiche)
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)

Timo Lang (TU Wien) WPI, OMP 1, Seminar Room 08.135 Mon, 11. Nov 19, 15:45
Bounded sequent calculi via hypersequents (joint work with A.Ciabattoni and R.Ramanayake)
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)

Sara Negri (University of Helsinki) WPI, OMP 1, Seminar Room 08.135 Tue, 12. Nov 19, 10:00
Proof analysis for the logics of agency: the deliberative STIT (joint work with Edi Pavlovic)
TBA
  • Thematic program: Informatics and Logic (2019/2020)
  • Event: Workshop on "TICAMORE - Translating and Discovering Calculi for Modal and Related Logics" (2019)

Kees van Berkel (TU Wien) WPI, OMP 1, Seminar Room 08.13 Tue, 12. Nov 19, 11:30
Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for (Deontic) STIT Logics (joint work with Tim Lyon)
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)

Luigi Santocanale (Aix-Marseille University) WPI, OMP 1, Seminar Room 08.135 Tue, 12. Nov 19, 12:15
Residuated lattices of join-continuous endofunctions of chains, ... and the Fibonacci numbers.
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)

Roman Kuznets (TU Wien) WPI, OMP 1, Seminar Room 08.135 Tue, 12. Nov 19, 16:00
Translating Quantitative Semantic Bounds into Nested Sequents
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)

Tim Lyon (TU Wien) WPI, OMP 1, Seminar Room 08.135 Tue, 12. Nov 19, 16:45
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems
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)

Guido Governatori (Data61, Brisbane) WPI, OMP 1, Seminar Room 08.135 Wed, 13. Nov 19, 9:30
Combining Modalities and Substructural conclusions with non-monotonic reasoning using Defeasible Logic.
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)

Bjoern Lellmann (TU Wien) WPI, OMP 1, Seminar Room 08.135 Wed, 13. Nov 19, 14:15
Nested sequents and countermodels for monotone modal logic
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)

Tiziano Dalmonte (Aix-Marseille University) WPI, OMP 1, Seminar Room 08.135 Wed, 13. Nov 19, 15:00
Countermodel construction via optimal hypersequent calculi for non-normal modal logics (joint work with Björn Lellmann, Nicola Olivetti, and Elaine Pimentel)
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)

Impressum webmaster [Printable version]