Seminars

It is therefore useful to estimate the cognitively adequate complexity of description logic so that the simplest justification(s) can be identified and selected. This work focusses on the cognitive complexity of deciding the consistency of ABoxes in the description logic $\mathcal{ALE}$. Conceptual considerations entail that the complexity of the ABox consistency problem is expressed as a linear preorder on a large enough set of ABoxes. This linear preorder can be estimated by an ACT-R model called SHARP. The model is a tableau algorithm implemented in a cognitive architecture, thereby modelling a human brain executing the tableau algorithm, which forms an approximation of the cognitive complexity ordering.

A complexity ordering that is a linear preorder can be obtained from experimental data by aggregating the different individual orders from a sample into one so-called proto-order, in which the largest transitive subrelation is the desired linear pre-order. The predicted complexity ordering by SHARP agrees well with the empirical data.

To enable applications in ontology debugging, a surrogate model is needed that accurately approximates SHARP’s output with great computational efficiency. Such a surrogate model can be obtained by the Random Forest algorithm trained on an appropriate dataset generated by SHARP. The complexity ordering thus obtained agrees well with the one predicted by SHARP but can be estimated in a fraction of the time enabling it for practical applications.

I will present the following results: (i) a set of non-nested conditional formulas each defining a different class of finite posets; (ii) a characterization theorem identifying the classes of finite posets that can be defined by a non-nested conditional formula; and (iii), a Sahlqvist-like theorem proving that every class of finite posets definable via a non-nested conditional formula is definable also by a first-order formula.

This talk is based on the paper Frame Definability in Conditional Logic, a joint work with Damiano Fornasiere and Johannes Marti, which was published at AiML 2024.

Base-extension semantics (BeS) is a strand of PtS where proof-theoretic validity is defined relative to a given collection of inference rules regarding basic formulas of the language. Although the BeS project has been successfully developed for intuitionistic propositional logic, first-order classical logic and the multiplicative fragment of linear logic among others, its progression as a comprehensive foundation for logical reasoning is still in its early stages.

In this talk, we will explore Pt-S with a focus on BeS. First, we will introduce an ecumenical perspective to BeS, inspired by Prawitz’s proposal of a system combining classical and intuitionistic logics. The aim is to deepen our understanding of logical reasoning disagreements by investigating the ecumenical approach and developing a unified proof-theoretic foundation for logical reasoning.

We will then address a major challenge in PtS, often called its “original sin”, which is its strong reliance on the natural deduction framework. To overcome this, we propose a version of BeS that employs atomic systems based on sequent calculus rules rather than natural deduction. In this approach, structural rules are treated as properties of atomic systems rather than the logical calculus itself. This allows for a semantics of substructural logics to emerge naturally by modifying the underlying atomic systems. Furthermore, this framework supports a Sandqvist-style completeness proof, but instead of extracting a proof in natural deduction, we obtain one in sequent calculus.

This is based is an ongoing and joint work with Victor Barroso-Nascimento, Luiz Carlos Pereira and Katya Piotrovskaya.

However, these logics are typically non-substitutional, limiting their algebraic treatment and preventing the development of schematic proof systems. This limitation can be attributed to the flatness principle which is commonly adhered to in many constructions of team semantics for logics.

In this talk, we approach the formation of propositional logic of teams from an algebraic perspective, explicitly discarding the flatness principle. We propose a substitutional logic of teams that is expressive enough to axiomatize key propositional team logics, such as propositional dependence logic.

Our construction parallels the algebraic construction of classical propositional logic from Boolean algebras. The algebras we are using are powersets of Boolean algebras equipped with both internal (pointwise) and external (set-theoretic) operations. The resulting logic is clearly substitutional, and is shown to be sound and complete with respect to a labelled natural deduction system.

If time permits, we will also discuss how we might do to extend this construction to the framework of first-order logic.

Recently, the above mentioned weighted complexity classes have been investigated in connection to classical counting complexity classes. Furthermore, several classical counting complexity classes have been characterized in terms of particular weighted logics over the semiring N of natural numbers. In this work, we cover several of these classes and obtain new results for others such as NPMV, ⊕P, or the collection of real-valued languages realized by nondeterministic polynomial-time real-valued Turing machines. Furthermore, our results apply to classes based on many other important semirings, such as the max-plus and the min-plus semirings over the natural numbers which correspond to the classical classes MaxP[O(log n)] and MinP[O(log n)], respectively.

Preservation theorems link semantics properties of formulas to their syntactic shape. The most famous example is the Łoś-Tarski theorem, which states that a first-order formula is preserved under induced substructures (i.e., remains true if one passes from a structure to an induced substructure) if and only if it can be written without using any existential quantifiers (assuming negation normal form). In this talk, we will review some recent results (both positive and negative) about the existence of preservation theorems for algebras of binary relations. (Algebraically, the results I will present can be equivalently viewed as addressing the question whether certain clones admit a finite set of generators).

Specifically, I will discuss results about Tarski’s relation algebra from a joint paper with Bart Bogaerts, Brett McLean, and Jan van den Bussche (LMCS 2024) as well as results about Kleene Algebra with Tests (KAT) from a joint paper with Tobias Kappé (POPL 2025).

We explore the possibility of extending this disquotational definition of truth via a principle of Generalised Induction introduced by Cantini. The principle is conservative over PA, meaning it preserves the epistemic status of a definition. Furthermore, we argue that the adoption of this principle is particularly motivated in the case of positive disquotational truth. Once this new truth predicate is allowed in the induction schema, we obtain significantly more justificatory power than the original disquotational theory. I conclude by sketching a possible strategy via a collapsing procedure to show that this result is sharp.

During the last years Tapani Hyttinen and I [2,3] have been looking at various models justifying the finite dimensional approaches from such textbooks. Our approaches are based on various embeddings of a Hilbert space into metric ultraproducts of finite-dimensional Hilbert spaces. In this talk I will present the basic ideas, their benefits and limitations. Time permitting, I will also contrast our approach to Boris Zilber’s work on the same questions, that was the original inspiration for us.

1. P.A.M. Dirac. The principles of Quantum Mechanics, 3rd ed, Clarendon Press, Oxford, 1947.
2. Å. Hirvonen, T. Hyttinen, On eigenvectors, approximations and the Feynman propagator, Ann. Pure Appl. Logic 170 (2019).
3. Å. Hirvonen, T. Hyttinen, On Ultraproducts, the Spectral Theorem and Rigged Hilbert Spaces, to appear in J. Symb. Log.
4. L. Schwartz, Théory de Distributions, Hermann, Paris, 1950.