ABSTRACT. In the formal verification of security protocols, one uses an abstract model where all messages are cast as terms in an algebra. This complicates the specification of protocols involving certification, where certificates end up with large, complex terms representing them, which makes analysis hard and divorces the abstract specification from the intended operational meaning. We present a new abstraction where certificates are modelled using assertions, which are formulae from a positive fragment of FOL. We show that this model makes specification and analysis easier, and might also provides insights into properties like privacy. Such properties typically require the simultaneous examination of multiple runs (in the terms-only model without assertions), but assertions might allow us to formulate them as safety properties, requiring the examination of only one run at a time.

ABSTRACT. The diversity of proof-output formats of automated and interactive reasoning systems hinders independent proof verification and interoperability. The Dedukti framework addresses this by implementing the λΠ-calculus modulo theory, enabling proofs from different frameworks to be expressed, combined, and checked automatically. Automated higher-order logic (HOL) provers are still absent from this ecosystem. We report work towards closing this gap with Leo-III, an automated theorem prover for extensional HOL.

ABSTRACT. We present the latest developments in HOLMS (HOL Light Library for Modal Systems), which now features a verified automated prover for Grzegorczyk logic and explores a novel implementation strategy: modal translation. This approach is illustrated by embedding Grzegorczyk logic into Gödel–Löb logic, and leverages the existing mechanisation for GL.

ABSTRACT. There is a strong separation between formal mathematical proofs and their equivalents written in natural language. When working with proof assistants, we need to translate mathematical reasoning in a formal language. This passage is not always trivial and can lead to a loss of information. One key point in this translation is that we need to represent the whole text, the discourse, and not just the isolated propositions. One of the main problem is that we need to resolved anaphoras, bindings whose scope is not a single sentence but rather the entire discourse. A classic example of the difficulty to represent anaphoras are donkey sentences, that are sentences of the shape "The equation has two roots. They are both real". In the second sentence there is an anaphoric reference to "roots". Different linguistic theories have been proposed to represent discourse in the last 40 years. We work with the theory proposed by Kamp and Reyle, Discourse Representation Theory (DRT) (Kamp 1981, Kamp 1993) and the variation by Lascaries and Asher, Segmented Discourse Representation Theory (SDRT) (Asher 2005). Some works have already tried this aproach using different formalisms (Ranta 1997, Ganesalingam 2013). In this ongoing work, we started investigating how to represent the statements and proofs of the theorems from Godement's Algebra. We focus on the discourse relations, the links between propositions inside a discourse, as defined in SDRT.

ABSTRACT. We describe a categorical model of MALL (Multiplicative Additive Linear Logic) inspired by the Heisenberg-Schrödinger duality of finite-dimensional quantum theory. Proofs of formulas with positive logical polarity correspond to CPTP (completely positive trace-preserving) maps in our model, i.e. the quantum operations in the Schrödinger picture, whereas proofs of formulas with negative logical polarity correspond to CPU (completely positive unital) maps, i.e. the quantum operations in the Heisenberg picture. The mathematical development is based on noncommutative geometry and finite-dimensional von Neumann (co)algebras, which can be defined as special kinds of (co)monoid objects internal to the category of finite-dimensional operator spaces. The full version is accepted to FoSSaCS 2026, see https://arxiv.org/abs/2601.15832 for extended version with appendices.

ABSTRACT. Free logics reject the classical assumption that all singular terms refer to existing objects, allowing sentences containing empty singular terms to be truth-apt. This paper focusses on positive free logics, i.e. the subset of free logics that allow empty-termed statements to be true. However, assigning truth-values (in particular, true) to such formulas may appear arbitrary. Moreover, the standard dual-domain semantics for positive free logics faces criticism on ontological grounds. To address these challenges, this paper proposes an alternative semantics built on Fine’s (2017) exact truthmaker semantics. After providing generalised semantic rules, a correspondence result between dual-domain and truthmaker models is established. In the last part, it is argued that this approach enables a principled account of the truth of empty-termed statements while avoiding reference to non-existing objects.

ABSTRACT. Reflexivity, expressed by the identity rule A ⊢ A, is typically taken to be a basic principle of logical consequence. In this paper, we reconsider this assumption by examining its role in the derivation of semantic paradoxes in formal theories of truth. We argue that the identity rule encodes a proof-theoretic commitment: formulas, once introduced, remain unconditionally available for further inference. In formal theories of truth, when a transparent truth predicate is present, this unrestricted availability may contribute to circular reasoning and non-terminating derivations, as in the liar-type paradoxes. We show that standard triviality derivations from liar-type sentences make essential use of the identity rule. Working in a sequent calculus framework, we demonstrate that such derivations systematically fail in systems without the identity rule, even when other structural rules are retained. This provides a proof-theoretic strategy for blocking semantic paradox. Our approach complements existing substructural theories, which primarily restrict contraction or transitivity, by isolating the role of reflexivity. This suggests that reflexivity is a revisable structural principle rather than a default rule.

ABSTRACT. It is widely accepted in the cognitive reasoning community that human reasoning is non- monotonic and thus classical logic is not adequate in modeling episodes of human reasoning. On the other hand, Answer Set Programming (ASP) is a popular declarative modeling language and solving framework with its roots in non-monotonic logics. We investigate whether ASP could also be suitable for learning and training purposed at high school level. One of the authors, a high school student, is working on a school project to solve a room allocation problem for the schedules at their school. This is a classical problem in computer science and can be solved through various approaches. As shown in the literature, Answer Set Programming seems to be suitable for such problems. We will investigate whether it is also intuitively applicable from a high school students’ point of view. This implies understanding the language, encoding the problem such that it is scalable for the real case instance. Furthermore, we define objective functions, which are in conflict with each other, and investigate the concept of a pareto front.

ABSTRACT. In manufacturing supply chains, such as those operated by Airbus, routing parts through a logistics network requires complex decisions regarding packing, routing, and dispatch frequency. Traditionally, these decisions aim to minimise costs; however, a purely cost-optimal solution often lacks a resilience metric. If a disproportionate share of a part's supply is concentrated on a single transport resource or trip, a disruption could severely compromise the network's ability to meet demand. In this paper, we address the Multi-Batching Problem using Answer Set Programming (ASP). The problem fundamentally consists of two sub problems. The first addresses network-level flow conservation, ensuring that the total supply and demand within the network remains balanced. The second sub problem is the bin packing problem, which ensures that the cumulative size of packed parts does not exceed the transport vehicle's capacity. To connect these two levels, the total parts transported along a route must be greater than or equal to the flow assignment, introducing a multiplicative constraint. Our initial monolithic approach encoded both flow and package assignment simultaneously; however, satisfying these constraints resulted in a multiplicative blow-up and grounding issues. To alleviate this, we explored the use of clingcon to leverage lazy grounding and linear constraints, yet to encode the multiplicative constraint connecting the two sub problems, we needed to define more rules which ultimately affecting the grounding. To overcome these scalability limitations, we propose a two-stage approach using clingcon that separates the network flow stage from the packing stage. This hybrid model successfully scaled to industry-sized network instances provided by Airbus. Upon examining the generated solutions, we identified structural vulnerabilities inherent to purely cost-optimised packings, such as uneven load distributions on arcs and mono-part trips. To mitigate these vulnerabilities, we introduce weighted soft constraints to penalise load imbalances and overly concentrated packages. Defining these soft constraints allowed for encoding resilience within the packing strategies. To measure the effectiveness of the soft constraints, we define two novel resilience metrics that quantify the worst-case demand coverage in the event of a disruption, demonstrating the trade-off between supply chain resilience and transportation costs. Our experimental evaluations demonstrate the efficacy of these constraints; on small and medium networks, network-level constraints improved worst-case demand coverage from 36\% to 63\%, successfully quantifying the trade-off with a 23\% increase in transportation costs. At the packing level, heterogeneous package configurations improved disruption tolerance without increasing baseline costs. While the two-stage model finds feasible solutions for industry-scale datasets, optimising these resilience-weighted constraints on massive instances within strict computational time limits remains a scalable challenge for future work.

ABSTRACT. Description logic reasoners are widely used in OWL-based semantic systems to derive implicit knowledge from explicitly asserted facts. In semantic web infrastructures, knowledge graphs, and ontology-based integration frameworks, these inference procedures support tasks such as consistency checking, classification, semantic interoperability, and automated decision support. Because inferred relations are often reused by downstream applications and validation pipelines, the correctness and completeness of the reasoning process are critical for ensuring the reliability of semantic technologies in practice. At the same time, supporting expressive ontology languages requires balancing inference power against the computational constraints of automated reasoning procedures. The description logic SROIQ, which forms the logical foundation of OWL 2 DL, introduced expressive role constructs such as complex role inclusion axioms, transitivity, asymmetry, irreflexivity, and role disjointness. To preserve termination and practicability of tableau-based reasoning procedures, SROIQ also introduced a distinction between simple and non-simple roles in order to control the interaction between complex role inclusions and other expressive constructs. In particular, roles participating in complex role inclusion axioms are classified as non-simple and are therefore prohibited from occurring in certain restrictive role conditions, including asymmetry, irreflexivity, and role disjointness. Horrocks, Kutz, and Sattler introduced these restrictions in the setting of tableau-based reasoning, where controlling the interaction between complex role inclusions and restrictive role constructs was required to preserve decidability and practicability. Crucially, however, they did not present all restrictions to simple roles as permanently settled: they explicitly state that “it is part of future work to determine which of these restrictions to simple roles is strictly necessary in order to preserve decidability or practicability”. We take this open question as a starting point for reconsidering, in light of later reasoning and validation technologies, whether the same restrictions must still determine the architecture of practical OWL reasoning systems. In particular, advances in semantic-based technologies and tooling motivate re-examining whether these restrictions remain necessary in practice, or whether they primarily reflect the operational assumptions of classical tableau-based reasoners. To revisit this question, we first performed a code-level analysis of Pellet, a widely used tableau-based OWL reasoner supporting SROIQ(D). Our focus is the interaction between complex role inclusion axioms (property chains, with transitivity treated as the special case R◦R ⊑ R) and restrictive role characteristics such as asymmetry, irreflexivity, and role disjointness. We show that Pellet enforces the OWL 2 DL simple-role restrictions during preprocessing, prior to tableau expansion. When a role occurs as the super-property of a complex role inclusion axiom and is simultaneously declared asymmetric, irreflexive, or disjoint, Pellet classifies the role as non-simple while also requiring it to remain simple. As a result, the ontology is conservatively rejected or weakened during preprocessing in order to preserve the operational assumptions of the tableau procedure. We show that this behavior suppresses entailments that are nevertheless valid under the OWL 2 Direct Semantics. The observed incompleteness therefore does not arise from semantic impossibility, but from implementation decisions inherited from classical tableau-based reasoning architectures. More generally, the work highlights the distinction between semantic constraints required by the logic itself and syntactic restrictions introduced for the practical limitations of the reasoning technology available at the time SROIQ was developed. Our findings also connect to recent work showing that implementation-level reasoning failures remain an active issue in contemporary OWL reasoners. Motivated by this observation, we propose a two-phase reasoning approach that separates structure-generating inference from restrictive role checking. In the first phase, expressive OWL axioms such as property chains and transitivity are used to materialize all derivable assertions. In the second phase, restrictive role conditions are evaluated over the materialized interpretation as explicit integrity constraints. We operationalize this second phase using SHACL/SPARQL validation rules, thereby allowing semantically valid entailments to be preserved while still making violations of asymmetry, irreflexivity, and role disjointness explicit. We highlight three main contributions. First, we identify an implementation-level source of entailment loss caused by the interaction between non-simple roles and restrictive role conditions. Second, we demonstrate the value of white-box analysis of reasoner internals for understanding practical reasoning behaviour beyond standard black-box evaluation techniques. Third, we propose a practical reasoning architecture that revisits the original open question posed in the SROIQ literature concerning the necessity of simple-role restrictions in contemporary semantic reasoning systems.

ABSTRACT. We formulate and prove the generalizations of Friedman's free set and thin set theorems and of the rainbow Ramsey theorem to colorings of barriers. We analyze the strength of these theorems from the point of view of computability theory proving some upper and lower bounds on the complexity of solutions for computable instances and some uniform computable reductions. We obtain as corollaries some proof-theoretical results on the logical strength of the theorems, in the spirit of reverse mathematics.

ABSTRACT. We establish the decidability of the propositional fragment CL15 of Computability Logic (CoL) by presenting a decision algorithm that avoids infinite proof-search branches caused by the unrestricted application of the contraction rule. The result is obtained through a provably equivalent bounded version of the fragment and a novel recurrence-based complexity measure. These findings offer a constructive theoretical basis for applications of CoL in areas such as formal verification and strategy synthesis.

ABSTRACT. Partial proof terms were first developed in \cite{CICM2024, WOLLIC25} as a new methodology for the theoretical study of proof search, where the representation of partial proofs and their conversion into finished proofs is central. These partial proof terms extend the Curry-Howard \cite{SU2006} representation of proofs by incorporating formal occurrences of sequents within proof terms. Such generalized proof terms represent incomplete derivations, encoding both what has already been proved and, through the presence of formal sequents, what remains to be proved. Partial proof terms are then used to define proof search procedures through rewrite rules. Typing systems that extend the original proof systems are also developed to accommodate partial sequents. The resulting rewriting systems characterize the logic's derivability relation, as formalized in the ``proof search as normalization'' theorems. The methodology is illustrated through case studies in propositional intuitionistic and classical logics, with the sequent calculi $\LJT$ and $\LKT$, whose proof search procedure is focusing, and two bidirectional natural deduction systems, $\NJT$ and $\NKT$, whose proof search procedure follows the ideas of the Sieg's Intercalation Calculus \cite{SiegCittadini2005}, but is focused in a sense specific to natural deduction. In both systems, the right inversion and focus (left or down) phases of proof search are distinctly separated and proceed in a specific order. In this talk, we generalize the proof search system for $\NJT$ in order to capture Intercalation Calculus without restrictions. For that, we revisit the original formulation of the Intercalation Calculus for intuitionistic implicational logic, in which the bottom-up application of introduction inference rules from the conclusion and the top-down application of elimination inference rules from the hypotheses are mixed in arbitrary order to yield normal derivations in ordinary natural deduction. We show how partial proof terms can adequately represent this search procedure and that the obtained formalization is indeed a generalization of the focused proof search system for $\NJT$. The search procedure obtains total proof terms and the corresponding $\eta$-expanded derivations in $\NJT$. For this reason, we explain beforehand how to adapt the Intercalation Calculus to yield such a kind of derivation. This is a joint work with José Espírito Santo -- Centre of Mathematics, University of Minho.

ABSTRACT. Paradoxes, or inconsistencies, in higher-order logic have long been a topic over the past century, and have led to many developments in type theory in order to build consistent, normalizing proof systems for proof assistants. In this paper, we discuss a connection between type universe hierarchies in Martin-Löf type theory (MLTT), and Kripke possible worlds models of $\lambda$-calculi with mutable references (memory locations that can be accessed and updated). The connection lies in how the Kripke worlds are constructed to essentially contain themselves, much like how Girard's paradox is encoded in earlier developments of MLTT and Russell's paradox is encoded in set theory. While models of $\lambda$-calculi with mutable references have been able to circumvent the cycle, we instead develop a calculus of \emph{stratified} mutable references based on the type universe hierarchy of MLTT. We believe our calculus may lay a foundation for normalizing logics with mutable references, i.e., what are commonly referred to as ``pointers'' in programming.