Program & Zoom

Types are fundamental for conceptual domain modelling and knowledge representation in computer science.  In the past decades, there has been a growing interest in providing support for representing not only first-order types (i.e., types whose instances are individuals), but also higher-order types (i.e., types whose instances are other types). Domains such as software development, product design and biological taxonomies are filled with rich multi-level classification schemes in which first-order and higher-order types as well as their ties have to be properly represented. Despite the fundamental role played by types of all levels in modelling practices, from an ontological point of view, there has been a lack of theoretical support for precisely defining a consensual view on types. From an ontological perspective, fundamental questions include: are types just equivalent to (unary) logical predicates? are types abstract or concrete entities? can types change and, if so, in which ways? are there multiple types of types? how different identity and individuation criteria relate to different types of types?  In this talk, I defend that properly answering these questions is fundamental for the theory and practice of (multi-level) modelling. To do that, I discuss the theory of types behind the Unified Foundational Ontology (UFO). UFO is an axiomatic ontological theory combining results from formal ontology, cognitive sciences, logics and linguistics to provide foundations for modelling constructs and tools. Thus, the theory of types in UFO is ontologically well-founded, psychologically informed, and formally characterized. Moreover, it has been systematically employed to generate several methodological and computational tools including a modelling language,  but also instruments for pattern-based model construction, formal verification and validation, anti-pattern detection and rectification, constraint learning and model repair, automated reasoning, complexity management and code generation. As I shall demonstrate, these results offer a sophisticated theory, as well as concrete engineering support for creating and reasoning with ontologically sound taxonomic structures, type-characterizing properties, as well as multi-level schemes.

We extend Savage's classic result (which shows that if a decision-maker's preferences over acts satisfy the appropriate postulates, then the decision maker is acting as if she has a probability on states, a utility on outcomes, and is maximizing expected utility) and show that it is possible to understand and identify a decision maker's subjective causal judgements by observing her preferences over acts that involve interventions. Following Pearl, we represent causality using  causal models (also called structural equations models), where the world is described by a collection of variables, related by equations. We show that if a preference relation over interventions satisfies certain axioms (related to standard axioms regarding counterfactuals), then we can define (i) a causal model, (ii) a probability capturing the decision-maker's uncertainty regarding the external factors in the world and (iii) a utility on outcomes such that each intervention is associated with an expected utility and such that intervention A is preferred to B iff the expected utility of A is greater than that of B.  In addition, we characterize when the causal model is unique.  Thus, our results allow a modeler to test the hypothesis that a decision maker's preferences are consistent with some causal model and to identify causal judgements from observed behavior. 

In this talk, I present formal argumentation as a logical foundation for explainable and ethical AI. As a core form of human reasoning and communication, argumentation offers a structured approach to handling incomplete, inconsistent, and uncertain knowledge, thereby complementing deep learning systems. I review key developments spanning abstract and structured argumentation—including Dung’s framework, ASPIC+, DeLP, and base argumentation—as well as extensions such as prioritized normative reasoning, probabilistic models, and dynamic frameworks that support modular and scalable reasoning. I further illustrate how argumentation facilitates explainable and ethical AI by enabling logical mechanisms for justification, transparency, and value-based decision-making. Recent advances, such as explanation semantics, attack-defense semantics, and the integration of quantitative argumentation with machine learning, are also discussed, highlighting their role in improving interpretability and collaboration with large language models.

Suppose a committee, expert panel, or other group is making judgments on some issues, where these may be not just yes/no-questions, such as whether a defendant is guilty or innocent, but include variables with many possible values, such as macroeconomic or meteorological variables or travel directions. Furthermore, there may be interconnections between different issues, as in the case of economic or climate variables. How can the group arrive at “intelligent” collective judgments, based on the group members’ individual judgments? We investigate three challenges raised by this judgment-aggregation problem. First, reasonable methods of aggregation (such as defining the collective judgment for each issue as the average or median judgment) can produce inconsistent collective judgments. Secondly, many methods of aggregation are manipulable by strategic voting. Finally, not all methods of aggregation are conducive to tracking the truth on the issues in question. We prove new impossibility or possibility theorems on all three challenges, identifying what it takes to produce collective judgments in a consistent, truth-tracking, and non-manipulable manner and thereby to achieve collective intelligence through aggregation. Overall, the median method, though imperfect, performs reasonably well. We also note the relevance of our analysis for non-human group decisions.

(with Franz Dietrich)

Fundamental logic is a non-classical logic based only on the introduction and elimination rules for the connectives in a Fitch-style proof system (see https://arxiv.org/abs/2207.06993). Building on previous work that added modalities to fundamental logic (https://arxiv.org/abs/2403.14043), in this talk I will discuss the addition of a necessity operator to fundamental logic that makes possible a full and faithful translation of intuitionistic logic into fundamental logic. The main results concern relational semantics for this fundamental logic with necessity.

Tba

I will present a Priestley-style duality for the classes of algebras that according to abstract algebraic logic are canonically associated with the congruential, finitary and filter distributive logics with theorems. I will also discuss some correspondence between logical properties of a logic, like enjoying a deduction theorem or the property of the disjunction and properties of the dual spaces.

The content of the talk is joint-work with María Esteban.

This talk introduces a general, non-modal, proof-theoretic framework for deontic reasoning based on default logic. Its central notion is that of controlled sequent, namely a sequent annotated with sets of formulas (control sets) that specify what should or should not follow from the formulas in the antecedent. Combined with extra-logical rules for defaults and norms, these control sets track applicability conditions and constraints, enabling local soundness checks. We show that controlled sequent calculi offer a flexible and expressive foundation for resolving deontic conflicts and modelling dynamic deontic notions through appropriate extra-logical rules.

Tba

Tba

In [2], we extended the logical categories framework to first order modal logic. In our modal categories, modal operators are applied directly to subobjects and interact with the background factorization system. We prove a Joyal-style representation theorem into relational structures formalizing a ‘counterpart’ semantics. We investigate saturation conditions related to definability questions and we enrich our framework with quotients and disjoint sums, thus leading to the notion of a modal (quasi) pretopos.

In [1], we refine modal categories so as to obtain an embedding theorem into (powers of) the category of topological spaces. The required extra axioms, besides the Kuratowski closure (namely S4) axioms, are a “product independence” and a “loop contraction” principle.

We finally show a way to build syntactic categories out of our first order modal theories.
----
[1]  S. Ghilardi and J. Marques. A completeness theorem for topological doctrines, July 2025. https://arxiv.org/abs/2507.20768.
[2]  S. Ghilardi and J. Marqu`es. First order modal logic via logical categories. J. of Symbolic Logic, November 2025. https://doi.org/10.1017/jsl.2025.10161.

The talk addresses the challenges inherent in incorporating axioms as rules within the framework of sequent calculi for intuitionistic logic.

The method of geometrization, which allows any first-order axiom to be replaced by geometric rules that preserve the structural properties of the underlying logical calculus, works for classical logic but fails intuitionistically because of the non-equivalence of certain classical transformations. The extent to which geometrization can be salvaged for intuitionistic logic is explored and it is shown that the method applies to generalized geometric axioms, thus providing a localized version of the non-local system-of-rules method. Further, a novel methodology is introduced for converting non-geometric axioms—those with negative occurrences of implications or universal quantifiers—into rules with context-sensitive premisses.  Finally, it is shown how this latter approach can be localized, yielding conservative extensions of the original theories through geometric rules with possible context restrictions.

(Joint work with Matteo Tesi)

Computable set theory studies decidable and semi-decidable fragments of set theory, primarily from a foundational perspective, and, when available, their applications to (semi-)automated proof verification.

In this talk, I will survey some of the main milestones in the area, focusing on Multi-Level Syllogistics (MLS) and its extensions for reasoning with sets, membership, equality, Boolean set operators, finite sets, unary union, powerset, and related constructors. These fragments admit concrete satisfiability procedures whose complexity bounds are often tight (in many cases matching NP-completeness), and some of them have already been used as the logical core of (semi-)automated proof-checking tools.

Leaving the membership predicate aside, I will then discuss a collection of small set-theoretic fragments of Boolean Set Theory (BST), involving union, intersection, difference, and predicates such as inclusion, emptiness, and disjointness. I will present a taxonomy of these fragments into polynomial-time and NP-complete cases and indicate how their satisfiability procedures can be used within a semi-automated proof verification tool.

Finally, I will report on ongoing work toward a general decidability theorem for so-called "factorizable operators", yielding a uniform proof scheme for all extensions of BST obtained by adding a single such operator. This framework generalizes the recent decidability result of Cantone and Ursino for BST with the unordered Cartesian product and represents the first contribution of this kind in computable set theory.

The foundational result in proof theory is cut-elimination, introduced by Gentzen in the 1930s. This is the algorithm that eliminates instances of the cut-rule from a formal proof. It is well-known that cut-elimination fails for most non-classical logics in the setting of the sequent calculus. Since the 1960s, the response was to introduce more complex formalisms such hypersequent, labelled and display calculi to regain cut-elimination. Although this programme has seen many successes, a recent alternative [1] shows that it is possible to retain the advantages of the sequent calculus, by transforming---when elimination is not possible---the cut-formulas into simpler ones. In particular, cut-restricted sequent calculi have been obtained for infinitely many logics, starting from a cut-free hypersequent calculus. As with cut-elimination, the final goal is to limit the proof search space to support proof-theoretic and meta-logical investigation. Subsequent work [2, 3] has shown how, for certain types of restrictions, the detour through the cut-free hypersequent calculus can be avoided altogether. This algorithm is called cut-restriction. I will survey these developments and discuss the challenge of a general cut-restriction algorithm.

---

[1] A. Ciabattoni, T. Lang, RR: Bounded-analytic Sequent Calculi and Embeddings for Hypersequent Logics. J. Symb. Log. 86(2): 635-668, 2021

[2] A. Ciabattoni, T. Lang, RR: Cut-Restriction: From Cuts to Analytic Cuts. LICS 2023: 1-13

[3] A. Ciabattoni, T. Lang, RR: Analytic Proofs for Tense Logic. TABLEAUX 2025: 220-237

The importance of taking individual, potentially conflicting perspectives into account when dealing with knowledge has been widely recognised. Many existing knowledge management approaches fully merge knowledge perspectives, which may require weakening in order to maintain consistency; others represent the distinct views in an entirely detached way. This talk presents an alternative, referred to as Standpoint Logic, a simple, yet versatile multi-modal logic “add-on” for existing logical languages intended for the integrated representation of domain knowledge relative to diverse standpoints, which can be hierarchically organised, combined, and put in relation with each other.

My talk will introduce the general logical framework of Standpoint Logic and discuss variations which differ in expressivity and computational complexity of automated reasoning.

JThe combination of probability and nondeterminism in state-based systems is a notoriously challenging problem, mainly due to the known lack of a distributive law between the powerset and probability monads. In this talk I will describe an alternative approach introduced by Ong, Ma, and Kozen (PLDI 2025) that models nondeterministic choice with multisets instead of sets. I will describe a class of probabilistic automata with nondeterminism modeled by multisets and a corresponding class of expressions analogous to regular expressions that are equivalent in expressive power. I will also describe a decision procedure the equational theory. The decision procedure is reminiscent of that for weighted automata, but based on polynomial algebra instead of linear algebra.

(Joint work with Shawn Ong and Stephanie Ma)

As an example of mathematics engineering, we will show how to refactor Birkhoff's completeness proof for equational logic along two dimensions. The first dimension consists of 'boilerplate' organizing notions such as terms, congruences, and substitutions. The second dimension parameterizes the construction by a notion of exactness in the category-theoretic sense (Barr exactness in the classical case). We will show how parameterization by a notion of exactness can lead to new Birkhoff style completeness theorems. 

(This is joint work with Yiwen Ding)