Spring Semester HS2023

Unless stated otherwise, all talks will take place in room A97 of the Exakte Wissenschaft Building (ExWi) at the University of Bern.

Schedule

Abstracts

In this talk I am going to present a family of intuitionistic logics extended with both the co-implication connective from Hilbert-Brouwer logic and with diamond and box modalities from modal logic. The semantics for such logics is based on intuitionistic Kripke frames equipped with a binary accessibility relation for interpreting the modalities. The accessibility relation is required to satisfy two 'forth' confluence properties with respect to the intuitionistic relation. I am going to present a sound and complete axiomatization for entailment for this class of frames as well as axiomatizations for subclasses of such frames that satisfy any combination of reflexivity, transitivity and seriality. Afterwards, I will discuss how to prove decidability for such logics by proving the finite model property: every formula which is falsifiable over one of the discussed classes of frames is falsifiable over a finite frame with bounded size. This is joint work with David Fernández-Duque (University of Barcelona) and Brett McLean (Ghent University).

MV-algebras extend the theory of Boolean algebras by replacing the two-element set of truth values {0,1} with the unit interval [0,1]. They provide the algebraic semantics of Lukasiewicz many-valued logic. Inspired by the extensive study of bounded distributive lattices, which are the negation-free subreducts of Boolean algebras, we aim to develop the theory of the negation-free subreducts of MV-algebras, called positive MV-algebras. These algebras can be thought of as the many-valued version of bounded distributive lattices. We axiomatize positive MV-algebras via finitely many quasi-equations. Moreover, generalizing Mundici's celebrated equivalence for MV-algebras [4], we obtain a categorical equivalence between positive MV-algebras and certain lattice-ordered monoids with units. We provide some results that can help to develop the theory of these algebras: in particular, we exhibit a finite quasi-equational axiomatization for the class of positive MV-algebras and a categorical equivalence with certain lattice-ordered monoids with units.
This talk is based on [1], [2], and a joint work with P. Jipsen, T. Kroupa and S. Vannucci [3].
References
[1] M. Abbadini. Equivalence à la Mundici for commutative lattice-ordered monoids. Algebra Universalis, 82:45, 2021.
[2] M. Abbadini. On the axiomatisability of the dual of compact ordered spaces. PhD thesis, University of Milan, 2021.
[3] M. Abbadini, P. Jipsen, T. Kroupa, and S. Vannucci. A finite axiomatization of positive MV-algebras. Algebra Universalis, 83:28, 2022.
[4] D. Mundici. Interpretation of AF C∗-algebras in Lukasiewicz sentential calculus. J. Funct. Anal., 65(1):15–63, 1986.

In this talk, I will describe a computation model that generalizes a wide variety of computer models including Turing machine, Boolean circuit, quantum computer, BSS (Blum-Shub-Smale) model, artificial neural network (deep learning) and analog computing. I will describe how a computer 'program' and the corresponding computation can be thought of as a vector field and the integral curve along the vector field. I will explain how this viewpoint gives rise to a general notion of computational complexity, and describe several important issues that need to be resolved for this new theory to be more useful in practice.

In traditional justification logic, evidence terms have the syntactic form of polynomials, which are Scott-continuous with respect to a natural order. Setting the evidence terms equal to polynomial functions over a omega-continuous semiring therefore yields a fixed point for each evidence term by Kleene's fixed point theorem. The existence of such fixed points allows a realization procedure for common knowledge. In this talk I'm going to introduce the justification logic SEK and present the realization algorithm relating common knowledge and SEK.

In this talk we shall discuss two logics: Propositional Dynamic Logic (PDL), and Transitive Closure Logic (TCL). PDL is a modal logic allowing to reason about iterative execution of programs. TCL enriches the language of first order logic with a recursive operator, expressing the transitive closure of binary relations. The two systems are closely related, as PDL can be embedded into TCL modulo a formula translation. However, the translation does not lift at the level of sequent-style cyclic proofs, defined in the literature for both logics. Motivated by this observation, we present an innovative hypersequent-style cyclic proof system for TCL. We show that the cyclic hypersequent calculus for TCL is sound, and that it simulates PDL proofs, thus establishing cut-free completeness of a fragment of TCL. This talk is based on joint work with Anupam Das.

Im Rahmen der vorliegenden Bachelorarbeit ist eine Biologie-Lernapp für Computer zum Thema Genetik entstanden. Grundlegende biologische Vorgänge sind innerhalb von Tutorials illustriert und spielerisch zugänglich gemacht. Das Spiel basiert auf Java und simuliert die Zucht von Pflanzen. Es richtet sich an gymnasiale Lernende und ermöglicht so theoretisches Wissen praxisnah anzuwenden.

Propositional Dynamic Logic is a multimodal logic designed for reasoning about the interaction between propositions and programs. Its language consists of atomic programs and atomic propositions, extended by propositional and program operators as well as modalities for every program. Expressions are interpreted over Kripke frames consisting of a set of states K and a meaning function which assigns a subset of K to each proposition and a binary relation on K to each program. In this talk I will introduce the syntax and semantics of PDL, and use the process of filtration to establish the small model property of PDL, i.e. that every satisfiable formula is satisfied at a state in a finite Kripke frame.

Unreliable Gossip describes the spread of information throughout a network of agents, some of whom may lie about their information. The goal in Gossip is to introduce protocols that limit the allowed calls between agents, but are still successful, i.e., at the end of a maximal sequence of allowed call, everyone knows all information. I will show that protocols from the literature (for reliable Gossip) no longer work with unreliable agents and introduce new ones that give us similar results as in reliable Gossip. Finally, I will present an initial approach to connect unreliable Gossip and Friendship Logic, another way of modelling the spread of information throughout a network.

I will present the problem of unifiability in the modal logic K: given a modal formula, is there a substitution of its variables which turns it into a theorem of K? Using the normal forms of this logic, I will describe how to solve this problem for formulas in one variable of modal degree one. For the situation with multiple variables, I'll discuss the limitations of the above approach and an algorithm for deciding unifiability in K.