Spring Semester FS2024

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

Schedule

Abstracts

The intuitionistic modal logic IK is obtained by extending IPC with necessitation and five axioms k1,k2,k3,k4, and k5. Dropping k4, we obtain the intuitionistic modal logic IK^-. We present G3IK^-, a (cut-free) sequent calculus for IK^- that admits weakening, contraction and cut. Since the left implication rule in G3IK^- is not terminating, we extend Dyckhoff's work and consider G4IK^-, the sequent calculus obtained by replacing the left implication rule in G3IK^- by six left implication rules, each corresponding to the outermost symbol of the antecedent of the implication. We prove that G3IK^- and G4IK^- are equivalent.

Intuitionistic propositional logic with second order quantifiers (IPL2) is a logic whose semantics have been thoroughly studied. However none of the work so far on its proof theory has ventured far enough to contend with the question of cut elimination. We present a sequent calculus for IPL2, along with our attempts to prove cut elimination for it and its fragments. In doing so, we introduce a new procedure for cut elimination, which uses hydra games to ensure a decrease in the cut measure.

An idempotent semifield is an idempotent semiring such that its multiplicative reduct is a group. In this talk I will present several results about equational theories of idempotent semifields. The results include that no non-trivial class of idempotent semifields has a finitely based equational theory; that there are continuum-many equational theories of idempotent semifields; and that the equational theory of the class of all idempotent semifields is co-NP-complete. This is joint work with George Metcalfe.

It is well-known that many modal logics are not complete w.r.t. Kripke semantics. Fine introduced the degree of (Kripke) incompleteness, which measures the number of logics which share their frame class. Blok famously proved that this degree is always one or continuum, now known as the dichotomy theorem. However, when restricting to extensions of K4, degrees of incompleteness are far less well-understood. We investigate degrees where instead of the entire frame class, we consider only conversely wellfounded frames. In particular, we will see that there exist continuumly many continuum such degrees.

The theory of inconsistency lemmas has not been systematically investigated so far, with only a few notable exceptions. Raftery proved that for a finitary protoalgebraic logic to have a (global) inconsistency lemma amounts to the demand that the join semilattice of compact deductive filters in each algebra of the corresponding type should be dually pseudocomplemented. Subsequently, Lávička and Přenosil introduced the local and parametrized local versions in a similar fashion to the hierarchy of deduction-detachment theorems and presented, for a class of logics that they called protonegational, the algebraic counterpart of the local inconsistency lemma, the so-called maximal consistent filter extension property.

In this talk we will present the existing results translated to the framework of finitary protoalgebraic logics. Additionally, we will introduce two new notions: the in- consistency by cases property and (first-order) definable maximal consistent filters. In parallel to the connection between the proof by cases property and filter-distributivity, we will prove that the corresponding bridge theorem arises between the inconsistency by cases property and the notion of 1-distributivity.

Finally, crossing back and forth over the bridge to the syntactical and algebraic setting, we will show that a finitary protoalgebraic logic has an inconsistency lemma if and only if it has the maximal consistent filter extension property, for every algebra A the deductive filter A is finitely generated, it has definable maximal consistent filters and it is filter-1-distributive.

The manual correction of programming exercises is a time-consuming and repetitive task at universities and other scholarly institutions. CodeGrader simplifies this task by providing a safe, scalable and easy to maintain Application for automated execution and evaluation of programming exercises.

Non-wellfounded proof theory results from allowing proofs of infinite height in proof theory. To guarantee that there is no vicious infinite reasoning, it is usual to add a constraint to the possible infinite paths appearing in a proof. Among these conditions, one of the simplest is enforcing that any infinite path goes through the premise of a rule infinitely often. Systems of this kind appear for modal logics with conversely well-founded frame conditions like GL (Gödel-Löb logic) or Grz (Grzegorczyk logic).

We provide a uniform method to define proof translations for such systems, guaranteeing that the condition on infinite paths is preserved. In addition, as particular instances of our method, we establish cut-elimination for non-wellfounded systems of the logics Grz and wGrz (weak Grzegorczyk logic). Our proof relies only on the categorical definition of corecursion via coalgebras, while an earlier proof by Savateev and Shamkanov uses ultrametric spaces and a corresponding fixed point theorem.

This is joint work with Thomas Studer and Lukas Zenger.

RUNVERSPACE addresses the systematic engineering of contemporary small-scale flight- and space- software, arguing that integrating runtime verification facilities is crucial for increased operational requirements assurance. RUNVERSPACE will focus on defining suitable programming abstractions and specification notations in tandem with development of architectural support, with an overall goal of demonstrating the potential that runtime verification can bring. Finding a proper logical framework to formulate mission requirements, by using the temporal logic family is an initial state of the project. However, to formulate some requirements we might need new logical frameworks to formulate software requirements.

The increasing applications of AI systems require personalized explanations for their behaviors to various stakeholders since the stakeholders may have various backgrounds. In general, a conversation between explainers and explainees not only allows explainers to obtain the explainees' background, but also allows explainees to better understand the explanations. In this paper, we propose an approach for an explainer to communicate personalized explanations to an explainee through having consecutive conversations with the explainee. We prove that the conversation terminates due to the explainee's justification of the initial claim as long as there exists an explanation for the initial claim that the explainee understands and the explainer is aware of.

Intuitionistic linear temporal logic iLTL extends intuitionistic propositional logic with the temporal modalities 'next', 'eventually' and 'henceforth'. Formulas are evaluated over expanding models, i.e. intuitionistic Kripke models equipped with an order-preserving function representing the temporal dynamics. The mathematical theory of iLTL has been studied extensively in recent years, resulting, amongst others, in a decidability proof for iLTL over expanding models. However, providing a sound and complete axiomatisation has remained an open problem.

In this talk I will first summarize the state of the field, including some of the main results about the proof theory and model theory of (fragments of) iLTL. I will then propose an extension of iLTL with the co-implication connective of Heyting-Brouwer logic called bi-intuitionistic linear temporal logic biLTL. By using the technical notion of a quasimodel, I will show that this extension is still decidable for the class of expanding models. Moreover, I present a sound and complete Hilbert-style calculus for biLTL, the first for any logic extending iLTL. As an unexpected corollary, I will show that no notion of co-implication is definable in a topological setting validating bi-intuitionistic logic.

This is joint work with David Fernández-Duque (University of Barcelona) and Brett McLean (Ghent University).

The Boolean satisfiability (SAT) problem asks if, given a propositional formula, there is some way to assign truth values to its variables that render the formula true. SAT is NP-complete, so a general efficient algorithm for solving it may not exist. However, industrial SAT problems tend to exhibit some structure that make them efficiently solvable in practice. In this BSc thesis presentation, I will present a popular approach to solving such SAT problems that is based on so-called conflict-driven clause learning (CDCL). I will also touch on a few tweaks that are commonly implemented in CDCL-based SAT solvers. Finally, depending on how well I progress with my thesis, I may discuss how SAT solvers can be used to solve planning problems (i.e., how to get from state A to state Z by locally permissible actions).