Autumn Semester HS2025

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

Schedule

Abstracts

Paraconsistent logics provide a framework for reasoning in contexts where classical principles for negation, like the explosion principle, fail. Such non-classical negations can be interpreted as negative modalities in Kripke models. Logics of formal inconsistency enrich this with an additional “consistency operator” which allows for the recovery of classical inferences. In this talk I will introduce a notion of (bi)simulation for such logics and show how these can be used to establish a Van Benthem style characterisation theorem.

Dynamic topological logic (DTL) refers to a family of multimodal logics, motivated by theoretical computer science, that combine a normal unimodal logic with a linear temporal logic. These logics come with 3 (unary) modalities: one normal "modal box", a "temporal next" and its reflexive transitive closure "temporal box”. The terminology derives from the standard semantics for these logics: the modal box is interpreted topologically (using closure semantics), and the temporal next by a continuous endo-function on the space (representing the "dynamics" of the system through time). For Alexandroff spaces this semantics reduces to a Kripke semantics on S4-frames with a monotone endo-function to interpret next. This Kripke semantics can be generalized to arbitrary frames.

Many DTL-logics fail to be decidable. For example, DTL over arbitrary topological spaces is known to be computably enumerable but undecidable. Over Alexandroff spaces, or equivalently S4-frames, DTL is again known to be undecidable, but enumerability is open. When the continuous function is replaced by a homeomorphishm, DTL over either arbitrary topological or Alexandroff spaces even fails to be computably enumerable. In this talk we give sufficient conditions on classes of (weakly) transitive frames for DTL over them to be computably enumerable.

We study notions of (virtual) group knowledge and group belief within multi-agent evidence models, obtained by extending the topological semantics of evidence-based belief and fallible knowledge from individuals to groups. We completely axiomatize and show the decidability of the logic of (``hard'' and ``soft'') group evidence, and do the same for an especially interesting fragment of it: the logic of group knowledge and group belief. We also extend these languages with dynamic evidence-sharing operators, and completely axiomatize the corresponding logics, showing that they are co-expressive with their static bases.

Provability logics are a class of modal logics where the modal operator is interpreted as provability in some formal mathematical theory such as Peano Arithmetic or ZFC. The set of axioms ocurring in these logics, specially when considering multiple modalities at one, are incompatible with the Kripke semantics. In other words, these logic lack of a nice Kripke semantics, usually requiring more structure on top of them such as a topology. This motivates to do a proof theoretical study of them, without relying on semantical aspects as long as possible and looking for uniformity.

In this talk we will see how non-wellfounded proofs are of great help for this purpose. We will also show the current problem we are trying to solve, the (in)existence of a (non-nested) cut-free sequent calculi for GLP, and the complications related to solving it.

The possible states of a distributed system at a given time can be elegantly represented by a simplicial complex—a downward-closed collection of vertex sets. Each vertex encodes the local view of an agent, while each maximal simplex (facet) corresponds to a global state of the system. In fault-free settings, every facet contains exactly one vertex per agent, yielding a pure simplicial complex; when agents may crash, the structure becomes impure.

Recent work has established a categorical correspondence between chromatic simplicial complexes and a class of Kripke frames, providing a natural semantics for epistemic logic on pure simplicial complexes. Building on this foundation, I will present a three-valued logical framework that captures reasoning about knowledge and crash failures in distributed systems, extending the combinatorial-topological semantics to impure simplicial complexes.

 In this talk, I will introduce a new approach to axiomatizing logics of the ∀∃ relation lifting and proving completeness results. This is made possible by observing that the comparative operator for ∀∃ relation lifting can be viewed as a parametrized modal operator in modal logic. Using this method, a series of new completeness results can be obtained in a systematic way. I will also demonstrate that under certain conditions the logic of ∀∃ relation lifting can be taken as the logic of conditionals.

Recent years have seen the emergence of simplicial semantics for various systems of multi-agent epistemic logic. In contrast to relational models, the primary building blocks of simplicial models are not possible worlds (i.e., global states of the system), but local states of agents. Recently, a more general semantics has been developed that is based on directed hypergraphs, a generalization of ordinary directed graphs in which edges are able to connect more than two vertices. Directed hypergraph models preserve the characteristic features of simplicial models (such as their geometric nature and the precedence of local states over global states), but also allow to account for the beliefs of agents. So far, however, only a specific notion of accessibility between global states in directed hypergraph models has been considered. In the talk, we investigate a large class of accessibility relations for hypergraph models and provide sound and complete axiomatizations for the resulting logics. We also identify various limitations of the general framework: certain logics of interest do not allow for a "natural" hypergraph semantics.

Fagin's seminal result characterizing NP in terms of existential second-order logic started the fruitful field of descriptive complexity theory. In recent years, there has been much interest in the investigation of quantitative (weighted) models of computations. In this talk I will present a study of descriptive complexity based on weighted Turing machines over arbitrary semirings. We provide machine-independent characterizations (over ordered structures) of several weighted complexity in terms of definability in suitable weighted logics for an arbitrary semiring. In particular, we prove weighted versions of Fagin's theorem (even for arbitrary structures, not necessarily ordered, provided that the semiring is idempotent and commutative), the Immerman--Vardi's theorem (originally for P) and the Abiteboul--Vianu--Vardi's theorem (originally for PSPACE). After that, I will discuss another machine model (Semiring Turing Machines) that also incorporates quantitative information in computations improving on some earlier limitations in the model from Eiter & Kiesel (Semiring Reasoning Frameworks in AI and Their Computational Complexity, J. Artif. Intell. Res., 2023). We solve an open problem proposed in Eiter & Kiesel by providing a Fagin-style theorem for the quantitative version of the complexity class NP, using another version of weighted existential second-order logic that allows predicates to be interpreted as semiring-annotated relations.