Autumn Semester 2020

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.

Schedule

Abstracts

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.

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.

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.

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.

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.

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.

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.

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.