Abstract: A recent line of research has developed around logics of belief based on information confirmed by a reliable source. In this paper, we provide a finer analysis and extension of this framework, where the confirmation comes from multiple possibly conflicting sources and is of a probabilistic nature. We combine Belnap-Dunn logic and non-standard probabilities to account for potentially contradictory information within a two-layer modal logical framework to account for belief. The bottom layer is to be that of evidence represented by probabilistic information provided by sources available to an agent. The modalities connecting the bottom layer to the top layer, are that of belief of the agent based on the information from the sources in terms of (various kinds of) aggregation. The top layer is to be the logic of thus formed beliefs.

Abstract: We present a polyvariant semi-inversion algorithm for conditional constructor term rewriting systems. Inversion is an elementary program transformation and has been studied in various programming language paradigms. Semi-inversion is more general than traditional inversion that swaps the entire input and output; instead, parts of the input and output can be swapped. The semi-inverter makes use of local inversion, a simple but effective heuristic, and is proven to be correct. It has been applied to the inversion of a simple encrypter and of a program inverter for a reversible programming language. This presentation explains the principles behind the algorithm.

Abstract: Recent research in experimental biology as well as bioinformatics has uncovered large amounts of data, which now has to be understood, processed, and applied towards understanding existing cells (systems biology) and creating new cellular functions (synthetic biology). In this talk I will discuss how concepts borrowed from programming language theory and mathematical logic can be used in order to organise data on the various kinds of information about cellular processes in order to give a clear and robust foundation.

Abstract: Formal Languages and Automata Theory are important and fundamental topics in Computer Science. Due to their rigorous and formal characteristics, learning these becomes demanding. An important support for the assimilation of concepts is the possibility of interactively visualizing concrete examples of these computational models, thus facilitating their understanding. There are many tools available, but most are not complete or do not fully support the interactive aspect.

This project aims at the development of an interactive web tool to help understand, in an assisted and intuitive way, the concepts and algorithms in question, watching them work step-by-step, through typical examples pre-loaded or built by the user (an original aspect of our platform). The tool should therefore enable the creation and edition of an automaton or a regular expression, as well as execute the relevant classical algorithms such as word acceptance, model conversions, etc. Another important feature is that the tool has a clean design, in which everything is well organized and it is also extensible so that new features can be easily added later.

This tool uses the Ocsigen Framework because it provides the development of complete and interactive web tools written in OCaml, a functional language with a strong type checking system and therefore perfectly suitable for a web page without errors. Ocsigen was also chosen because it allows the creation of dynamic pages with a singular client-server system.

This document introduces a running version of the tool, its design aspects and its mechanisms and related functionalities.

Abstract: Partial Dynamic Epistemic Logic allows agents to have different knowledge representations about the world through agent awareness. Agents use their own vocabularies to reason and talk about the world and raise their awareness when confronted with new vocabulary. Through raising awareness the vocabularies of agents are extended, suggesting there is a dual, inverse operator for forgetting awareness that decreases vocabularies. In this paper, we discuss such an operator. Unlike raising awareness, this operator may induce an abstraction on models that removes evidence while preserving conclusions. This is useful to better understand how agents with different knowledge representations communicate with each other, as they may forget the justifications that led them to their conclusions.

Abstract: The aim of this talk is to develop six (hopefully) interesting implicative expansions of the well-known Anderson and Belnap's First Degree Entailment Logic (FDE) –also sometimes referred to as B4. The logics BN4 and E4 –which can be considered respectively as the 4-valued logic of the relevant conditional and (relevant) entailment– are indeed implicative expansions of FDE and will serve as the starting point. My purpose is to investigate the implicative variants of BN4 and E4 which verify Routley and Meyer's logic B (a central system among relevance logics and a proper extension of FDE) and endow them with a Belnap-Dunn type bivalent semantics (BD-semantics). In what follows, I mean to explain the importance of the mentioned systems among non-classical logics and to detail what makes the six developed systems (from now on, L4-logics) possibly interesting.

Abstract: We present some results in reverse mathematics of Ramsey-type combinatorial principles. We study the Cohesiveness Principle (COH) which is a consequence of the Ramsey's Theorem for pairs and two colours (RT^2_2). We answer an open question about the logical strength of COH over the weak base theory RCA*_0. We also show that RCA*_0 is too weak to prove that RT^2_2 implies COH.

Abstract: Uniform interpolation has recently been shown to be a powerful property in the study of the existence of proof systems. So-called negative results are established by Iemhoff, saying that whenever a certain logic does not have uniform interpolation, that logic cannot have a sequent calculus with certain `nice' properties. One very important nice property is termination. In the talk, I will discuss work in progress on the attempt of proving uniform interpolation for intuitionistic Gödel-Löb logic and strong Löb logic. I also want to address the role of terminating calculi.

Abstract: Uniform interpolation is a reasoning technique that allows us to express a theory using a subset of its symbols while maintaining our understanding of the theory. Much research efforts have been put into investigating different aspects of the uniform interpolation problem in propositional logic, first-order logic and description logics. Research in the area of modal logic has been mainly concentrated on uncovering theoretical results. In this work, our main focus of our work is to develop practical implementable systems that may be beneficial for application purposes. Our method for solving the uniform interpolation problem follows a resolution approach. The idea behind the elimination process is to exhaustively compute consequences and subsequently eliminate those that contain symbols outside the interpolation signature. As far as the authors know, our method is the first practical method to solve the uniform interpolation problem for local satisfiability in the modal logic K defined over Kripke frames.

Abstract: Unification and matching algorithms are essential components of logic and functional programming languages and theorem provers. Nominal extensions have been developed to deal with syntax involving binding operators: Nominal syntax is a generalisation of first-order syntax that includes names, a notion of name binding and an elegant axiomatisation of alpha-equivalence, based on nominal set theory. However, it does not take into account non-capturing atom substitution, which is not a primitive notion in nominal syntax.

We consider an extension of nominal syntax with non-capturing atom substitutions and show that matching is decidable and finitary but unification is undecidable in general. The proof of undecidability of unification is obtained by reducing Hilbert's tenth problem to unification of extended nominal terms.

We provide a general matching algorithm and characterise a class of problems for which matching is unitary, giving rise to expressive and efficient notions of rewriting.

This is joint work with Jesus Dominguez.

Abstract: Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Hoare, Struth, and collaborators proposed a concurrent extension of Kleene Algebra (CKA) as a first step towards developing algebraic reasoning for concurrent programs. Completing their research program and extending KAT to encompass concurrent behaviour has however proven to be more challenging than initially expected. The core problem appears because when generalising KAT to reason about concurrent programs, axioms native to KAT in conjunction with expected axioms for reasoning about concurrency lead to an unexpected equation about programs. In this talk, we will revise the literature on CKA(T) and explain the challenges and solutions in the development of an algebraic framework for concurrency.

The talk is based on a series of papers joint with Tobias Kappé, Paul Brunet, Bas Luttik, Jurriaan Rot, Jana Wagemaker, and Fabio Zanasi. Detailed references can be found on the CoNeCo project website: https://coneco-project.org/.

Abstract: We present MOILab, a prototype Prolog theorem prover implementing a labelled sequent calculus for IK, the basic system in the intuitionistic modal logics family. MOILb builds upon MOIN, a theorem prover implementing nested sequent calculi (both single-conclusion and multi-conclusion) for all the logics in the modal intuitionistic cube.

Abstract: In this talk, my aim is to give a philosophical reading of bilateralism by means of probabilism. That is to understand the main concepts of bilateralism, “acceptance”, “rejection” and “incoherence” in terms of the probabilistic notions of “credence” and “coherence”. Building on Field's paper, “What is logical validity?” (2015) my work will focus on what is the limit of acceptance and rejection when understood in terms of degree of belief. The obvious limitations of this work are the lottery/preface paradoxes, and for that I will appeal to Leitgeb's P-stability theory of belief, which I will redefine to make it suitable for a bilateralist approach. I will draw some philosophical morals out of these paradoxes regarding what is incoherent to accept and to reject that can be extended to some other non-paradoxical contexts.

Abstract: The discussion about how to put together Gentzen's systems for classical and intuitionistic logic in a single unified system is back in fashion. Indeed, recently Prawitz and others have been discussing the so called Ecumenical Systems, where connectives from these logics can co-exist in peace. In Prawitz' system, the classical logician and the intuitionistic logician would share the universal quantifier, conjunction, negation, and the constant for the absurd, but they would each have their own existential quantifier, disjunction, and implication, with different meanings.

Prawitz' main idea is that these different meanings are given by a semantical framework that can be accepted by both parties. In a recent work, Ecumenical sequent calculi and a nested system were presented, and some very interesting proof theoretical properties of the systems were stablished.

In this work we extend Prawitz' Ecumenical idea to alethic K-modalities.

Abstract: Christine Ladd-Franklin is often hailed as a guiding star in the history of women in logic---not only did she study under C.S. Peirce and was one of the first women to receive a PhD from Johns Hopkins, she also, according to many modern commentators, solved a logical problem which had plauged the field of syllogisms since Aristotle. In this paper, we revisit this claim, posing and answering two distinct questions: Which logical problem did Ladd-Franklin solve in her thesis, and which problem did she think she solved? We show that in neither case is the answer "a long-standing problem due to Aristotle''. Instead, what Ladd-Franklin solved was a problem due to Jevons that was first articulated

In this work we extend Prawitz' Ecumenical idea to alethic K-modalities.

Abstract: Developing efficient tools and techniques for propositional satisfiability (SAT) solving has long been recognized as impactful pursuit. Advances in SAT, and it's extension, Satisfiability Modulo Theories (SMT), directly translate to model checking, planning and scheduling, automatic test-case generation, combinatorial equivalence checking, graph coloring, software verification, and more. Temporal logic satisfiability checking, for example for Linear Temporal Logic (LTL) and its many derivatives such as Mission-time LTL (MLTL), has received considerably less attention.

The historic lack of attention to temporal logic satisfiability is surprising because it is impactful in a wide variety of domains, including those impacted by SAT and SMT. Perhaps one of the most wide-reaching applications of temporal logic satisfiability is specification debugging, which ensures that no requirement is accidentally unsatisfiable or valid, and that all requirements can be true of the same (reactive) system at the same time. Finding specification bugs early in the system design lifecycle, before systems are built off of faulty specifications, can have financial impacts in the millions of dollars. Temporal logic satisfiability is also central to the runtime verification (RV) problem, which asks whether the current, executing system upholds its (temporal logic) specification. RV algorithms would be improved by faster, more efficient temporal logic satisfiability solvers. Furthermore, such solvers are desperately needed for verification of RV engines, for example, via generating RV benchmarks. We briefly overview the state of the art in temporal logic satisfiability, and identify exciting future research directions with potential for interdisciplinary impact.