Autumn Semester 2020

Due to the of Coronavirus cases in Switzerland and university regulations, future seminars will take place online via Zoom. For further details, please contact George Metcalfe or Thomas Studer (contact details in the sidebar).

Unless stated otherwise, all talks will take place in room A97 of the Exakte Wissenschaft Building (ExWi) at the University of Bern. Please note that the university requires all seminar attendees to wear a mask.


Date Time Speaker Title
01.10.2020 13.30 - 14.15 Lea Keller - University of Bern Interpolation for integrally closed residuated lattices
14.15 - 15.00 Atefeh Rohani - University of Bern Neighbourhood Semantics for Justification Logics, A way to Deontic Justification Logics
22.10.2020 13.30 - 14.15 Naomi Tokuda - University of Bern Independence and Decidability
14.15 - 15.00 Michael Baur - University of Bern Semirings of Evidence
12.11.2020 13.30 - 14.15 Olim Tuyt - University of Bern Monadic Residuated Lattices
14.15 - 15.00 David Lehnherr - University of Bern A brief introduction to the Curry-Howard Isomorphism
03.12.2020 13.30 - 14.15 Lukas Zenger - University of Amsterdam Interpolation for a fragment of the modal mu-calculus using circular proofs
14.15 - 15.00 Veronika Wu - University of Bern Qualitative analysis of matching graphs


Interpolation for integrally closed residuated lattices

Lea Keller

In this talk we investigate the Craig interpolation property for the class of commutative integrally closed residuated lattices (cIcRL), their reducts and the class of abelian pregroups, whose structure is similar to those of a reduct of cIcRL. To do so, we make use of sequent calculi for the different structures. We will also show that Casari’s comparative logic, which has a close relationship to the variety of abelian pregroups, has the deductive interpolation property.

Neighbourhood Semantics for Justification Logics, A way to Deontic Justification Logics

Atefeh Rohani

An introduction to neighbourhood semantics in Modal logic and Justification logics is given. Neighbourhood models are defined in Justification logics which are shown to be sound and complete with respect to language of Justification Logics. Finally, Motivations for using neighbourhood semantics for Deontic logic is explained. Deontic logic is the logic of normative systems which can be viewed from different perspectives such as Modality.

Independence and Decidability

Naomi Tokuda

The notion of linear independence in vector spaces can be generalized to an arbitrary variety \(\mathcal{V}\) as follows: Terms \(t_1,\dots,t_n\) are called \(\mathcal{V}\)-independent if any equation in the variables \(y_1,\dots,y_n\) that becomes valid in \(\mathcal{V}\) when the \(y_i\) are substituted by the \(t_i\) is trivial, i.e., already valid in \(\mathcal{V}\). We investigate whether for certain varieties it is decidable if some \(t_1,\dots,t_n\) are \(\mathcal{V}\)-independent and give the respective algorithms. In particular, we consider the varieties of semigroups, modal algebras, lattices and distributive lattices.

Semirings of Evidence

Michael Baur

A novel semantic approach to justification logic that models evidence by a semiring is presented by introducing the logic SE. This provides an adequate semantics for evidence terms and clarifies the role of variables in justification logic. Moreover, the algebraic structure makes it possible to compute with evidence. Depending on the chosen semiring this can be used to model trust, probabilities, cost, etc. The most important theorems concerning SE are shown, including a realization theorem for the modal logic K.

Monadic Residuated Lattices

Olim Tuyt

Algebras that contain two unary S5-modalities have been widely studied in different contexts throughout the literature, usually under the name "monadic". Examples include monadic Boolean algebras, monadic Heyting algebras, monadic Godel algebras, monadic MV-algebras, monadic abelian l-groups, and more. Such algebras often occur in the context, or as a consequence, of the study of one-variable fragments of first-order logics. Indeed, there is a one-to-one correspondence between one-variable first-order formulas and modal formulas, where the universal and existential quantifier correspond to the box and diamond modality, respectively.

In this talk we will present an attempt to generalize and unify some of the known results for these "monadic algebras" by introducing monadic residuated lattices. All aforementioned monadic algebras are included in this class. We present some initial results: we show that for a monadic residuated lattice, the modalities are determined by a "relatively complete" subalgebra of the residuated lattice reduct. Moreover, congruences are determined by congruences of this relatively complete subalgebra.

A brief introduction to the Curry-Howard Isomorphism

David Lehnherr

The Curry-Howard Isomorphism is a fundamental result in logic and theoretical computer science. It describes the relation between formulas in intuitionistic logic and type theory. That is, a formula is true if the corresponding type has an inhabitant (a term belonging to this type). Moreover, this term is interpreted as a proof for the proposition.

In this presentation we will introduce Gentzen's sequent calculus for classical and intuitionistic logic and discuss the famous cut-elimination theorem. After that we will present Church's untyped lambda calculus and its properties. This naturally leads to the discussion of the (simply) typed lambda calculus that has some additional properties. We are then ready to state the Curry-Howard Isomorphism and show some parts of the proof.

Interpolation for a fragment of the modal mu-calculus using circular proofs

Lukas Zenger

The modal mu-calculus is an extension of propositional modal logic with a least and a greatest fixed point operator. The addition of fixed point operators substantially increases the expressive power of the logic. Despite its expressive power, the modal mu-calculus enjoys many desirable mathematical properties such as decidability or the finite model property.

In this talk we establish that the Craig interpolation property holds for a specific fragment of the modal mu-calculus. In order to do so, we introduce the idea of circular proofs and show how to obtain a sound and complete circular proof system for that fragment. We then show how to use this circular system to prove Craig interpolation.

Qualitative analysis of matching graphs

Veronika Wu

Given a novel approach for Graph Classification - the Matching of Matching-Graphs - a qualitative analysis will be performed on said Matching-Graphs.
In this talk there will be a short introduction to graph based pattern recognition as a subarea of Machine Learning and a brief description of a novel approach for Graph Classification. Further we will analyze the quality of the Matching-Graphs by means of an Algorithm for Subgraph Isomorphism by J.R. Ullman.