ABSTRACT. Process graphs that are interpretations of `1-free' regular expressions in Milner's process semantics for regular expressions have the Loop Existence and Elimination Property (LEE). Hereby a process graph satisfies LEE if the procedure of loop elimination, in which in every step a loop subgraph is decoupled by removing its entry transitions and then garbage collection is performed, terminates in a process graph without an infinite trace. Loop elimination on finite process graphs is a terminating, but typically not confluent. We explain that loop elimination can be turned into a confluent rewrite system on all process graphs by adding pruning steps that remove transitions to deadlocking states. For this purpose we perform a critical-pair like analysis that involves bi-loop subgraphs, and use the decreasing diagram method. This confluence result has two expedient consequences: for finite process graphs, LEE can be decided in polynomial time, and a layered version of LEE (no loops are eliminated from bodies of already eliminated ones) coincides with LEE.

ABSTRACT. The theory of arrays with select and store plays an important role in software verification and is therefore supported by virtually all state-of-the-art SMT solvers. There are many extensions, for instance by constant arrays, element-wise function applications, counting, or projections, that have been shown to preserve decidability. In recent work, a theory of arrays extended by constant arrays and sum predicates, called summation array logic (SAL), has been introduced and proven to be decidable in non-deterministic polynomial time. In SAL, it is possible to state assertions about the sum of all entries in a (finite or infinite) array of integers. This paper provides an eager approach to the satisfiability problem in SAL. The approach transforms a SAL formula to an equi-satisfiable formula in the theory of extensional arrays (extended with constant array operator), which can then be decided by an off-the-shelf SMT solver. The transformation produces a formula at most quadratic in the size of the input formula. Since there are no standard array benchmarks with sum constraints yet, the paper presents a new set of such benchmarks obtained by mutating existing SMT-LIB array benchmarks. The experiments show that the transformation-based decision procedure incurs only a relatively small overhead in terms of solving time.

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. Equational Theories Project is a collaborative effort, which explores the validity of certain first-order logic implications of certain kind. The project has been completed but triggered further research. This report investigates how much can be automatically proven and disproven by the automated theorem prover Vampire. An interesting conclusion is that Vampire can prove all the considered implications that hold and also is able to refute a vast majority of those that do not hold. A downside is that proofs coming out of Vampire do not give a direct proof artifact for models.

ABSTRACT. In saturation-based theorem proving, selecting the next clause for processing is a major concern. Twee has successfully applied the idea of preferring clauses that share terms with the conjecture by adding equational defintions to transform the problem. In this paper, we apply the idea to the full first-order case, and offer an alternative implementation based on shared terms that shows very promissing results.

ABSTRACT. Connection-tableau provers typically construct closed tableaux by backtracking search. This gives lightweight proof procedures, but their low-memory search state leaves little derived information to reuse after a failed attempt. SATCoP addresses this by retaining grounded tableau clauses in an incremental SAT solver, allowing the prover to refute the problem once the accumulated ground clauses become propositionally unsatisfiable. We introduce SATResetCoP, which relies more directly on this persistent SAT state by not backtracking on unproductive tableaux and instead starting new ones to generate further ground clauses for the SAT solver. On TPTP, SATResetCoP improves over our leanCoP-style baseline by 54% and our SATCoP-style baseline by 18%. On the bushy MPTP2078 benchmark, it solves 616 problems, a 49% improvement over our leanCoP-style baseline and a 12% improvement over our SATCoP-style baseline. These results suggest that changing tableau guidance to accumulate useful ground clauses faster improves the performance of the prover.

ABSTRACT. We complete Maksimova's classification of the normal extensions of S4 with interpolation. In particular, we prove Craig interpolation for the six extensions of S4 for which Craig interpolation was still open. The proof strategy builds upon the ideas of Smoryński, but employs a novel approach using Fine's frame formulas for splitting clusters.

ABSTRACT. This extended abstract summarizes previous results on the repair of inconsistent constraint networks from a viewpoint of explaining the inconsistency. We discuss how explanation could be defined using methods of formal argumentation and illustrate use cases of constraint-based approaches to planning.

ABSTRACT. In the literature, interactive ontology repair approaches assume that users can always decide whether an axiom should be included in a repair, i.e., either kept or removed. In this paper, we present an interactive approach for repairing ontologies in which users are assisted by various decision-support features that provide additional information in cases of uncertainty. This work has been submitted to the Description Logic Workshop 2026 and is currently under review.

ABSTRACT. The extraction of Minimal Unsatisfiable Subsets (MUSes) has been extensively studied in SAT for clauses as well as groups of clauses, but it is also useful in other formalisms such as pseudo-Boolean solving (PB) and constraint programming (CP), especially for explaining unsatisfiability. In this paper we focus on highly efficient deletion-based MUS extraction, where the main bottleneck is the number of solver calls needed to find a MUS. This number can be greatly reduced by techniques such as model rotation (MR), which manipulates a satisfying assignment to find new critical constraints. However, MR has mostly been studied only for (grouped) clausal constraints. We propose generalisations of MR for pseudo-Boolean and CP constraints, and empirically evaluate them on PB and CP instances, including SAT encodings with state-of-the-art SAT-based MUS extractors. Our results show that MR is most effective when applied directly at the level of the original formalism, increasing the number of solved instances for PB and reducing solving times for CP.

ABSTRACT. We report ongoing work on a framework that constructs a compact, formally certified surrogate of a large continuous-time Markov chain (CTMC) for transient reachability analysis: it takes a PRISM model as input and returns a small abstract PRISM model whose induced CTMC approximates the concrete one within a user-specified tolerance.The core idea is to lift predicate abstraction from program verification into the continuous-time stochastic setting, where the new semantic challenge is rate aggregation: choosing a single transition rate for a block of concrete states without losing formal guarantees.The presentation focuses on three ideas: a semantically derived rate aggregation theory; an automated, learning-inspired refinement loop; and an explicit output artifact that is reusable, inspectable, and diagnostic.The corresponding full paper is under review at a leading international conference on automated verification, and its core theorems have been machine-checked in the Lean 4 proof assistant.

ABSTRACT. We recall a connection made in a recent conference paper between the optimal repair property in knowledge engineering and the unification types unitary and finitary in unification theory. This connection is revealed when looking at repairs and unifiers from an order-theoretic point of view. The paper gives order-theoretic characterizations of the optimal repair property (and thus of unification types unitary or finitary), but also generalizes the optimal repair property to the notion of repair types, in analogy with the definition of unification types. Finally, it shows that (a generalization of) unification can actually be seen as a repair problem.

ABSTRACT. Finite multisets (also known as bags) are a fundamental data structure that generalizes finite sets to record the elements' multiplicities. In the Isabelle proof assistant, finite multisets are defined as the subtype of functions from elements to natural numbers consisting of functions that return non-zero multiplicities for finitely many elements. This representation is negative: the elements occur to the left of the function arrow. To allow (co)datatypes to (co)recurse through multisets, an alternative positive representation as quotients of finite lists of elements modulo permutations is used. Using Isabelle, we define two orthogonal generalizations of multisets and the respective positive and negative representations. First, we view countable multisets either as functions from elements to extended natural numbers that return non-zero multiplicities for countably many elements or, alternatively, as quotients of lazy lists modulo infinitary permutations. Second, we view weighted sets either as functions from elements to optional weights from a well-behaved algebraic structure that return None for all but finitely many elements or, alternatively, as quotients of element-weight lists modulo permutation and regrouping by element. For both types, we establish the necessary functorial structure to support (co)recursion and exemplify this support in two case studies.

ABSTRACT. This paper proposes a framework for database repairing that abstracts away from specific choices of language and structure, assuming only a primitive relation between a set of structures and a set of formulas. Within this framework, we define a family of belief change operators that capture an abstract notion of repair, characterized by partial orders and a set of admissible outcomes. This means that, given an initial structure and a set of constraints, the operator can impose extra-logical criteria on the class of admissible structures. In particular, this captures distance-based, subset, and superset repairing.

ABSTRACT. Functional dependencies are an important and well-studied class of database constraints that correspond to a notion expressed by dependence atoms in team logic. In practice, data often contain errors, so in some cases it might be useful to allow the database to have a small number of tuples that violate the desired dependency. Väänänen (2017) studied the axiomatization of a notion of approximate dependence that specifies for each dependence atom how much of the database can be disregarded. We demonstrate that the interaction of approximate dependence atoms is more complicated than previously thought in the sense that there is a semantic consequence that is not captured by the inference rules introduced before. We show that Väänänen's axiomatisation is still complete in the restricted case of unary dependencies. We also consider the complexity of model checking for approximate dependence: it is NP-complete for disjunctions of two atoms and LOGSPACE-hard for individual atoms.

ABSTRACT. We study inconsistency from the perspectives of knowledge representation and statistical inference, and propose a unified framework to relate the two. In statistics, inconsistency arises when data are impossible under a generative model and is typically addressed through flexible modeling or error mechanisms. In logic and computer science, inconsistency corresponds to violations of constraints and is handled via inconsistency-tolerant reasoning. We formalize inconsistency in statistical models in logical terms, enabling the use of repair-based semantics such as AR and CAR. We illustrate the approach in two settings: binary classification with a monotonicity assumption and preference learning with non-transitive comparisons.

ABSTRACT. Physical agents have limited resources and cannot compute all the logical consequences of their beliefs. They therefore possess incomplete deductive abilities, and thus may fail to recognise inconsistencies. This does not prevent them from using and revising their beliefs, and from possibly resolving the undetected inconsistency after some time. However, most multi-agent logics of beliefs represent an agent's beliefs as a logically closed set, and therefore cannot represent inconsistent beliefs without explosion. Here we present a multi-agent logic of belief that can represent agents with incomplete deductive abilities and inconsistent beliefs.

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. Okui proved that simultaneous critical pairs (SCPs) can be used as a sufficient criterion to ensure confluence of term rewrite systems. His definitions, lemmas and proofs where reformulated by Kirk and Middeldorp. They heavily utilize proof terms and finally arrive at a formalized proof of Okui's result in Isabelle/HOL. However, Kirk and Middeldorp's formalization lacks an executable algorithm to compute the set of proof term based SCPs in a verified way. In this work, we provide such an algorithm, and we further modify the formalization in such a way, that SCPs can also be used to show commutation, generalizing the confluence result. Our results have fully been integrated in the certifier CeTA, that now can deal with both commutation- and confluence-proofs by SCPs.

ABSTRACT. We generalize the confluence result for orthogonal higher-order pattern rewrite systems to higher-order rewrite systems whose left hand sides consist of Yokoyama et al.'s deterministic higher-order patterns.

ABSTRACT. We show that for the (untyped) bang-calculus β! is confluent modulo σ.

ABSTRACT. We describe a machine-checked proof of a result in Isabelle/HOL that implies that if the cardinality of a confluent abstract rewriting system (ARS) is below the first uncountable limit cardinal, then confluence of this ARS can be proved with the help of the decreasing diagrams method using 3 labels and such an ARS has a so-called almost deterministic Church-Rosser strategy (defined by weakening conditions of the definition of deterministic one-step Church-Rosser strategies). We also discuss consequences of this result. One consequence is that there is a statement that can be used as additional axiom to HOL that implies that every confluent ARS has an almost deterministic Church-Rosser strategy and that the decreasing diagrams method with 3 labels is complete without cardinality restrictions.

ABSTRACT. In syntactic anti-unification, one is concerned with finding the commonalities between terms, while (uniformly) abstracting their differences. The original goal of anti-unification development in the seventies was to automate inductive reasoning. Recent applications of anti-unification techniques include efficiently transforming sequential code into parallel code, detecting code clones, and preventing software failures. Previous work addressed the elements required to verify, in the Prototype Verification System (PVS), termination and soundness of a functional algorithm based on inference rules for syntactic anti-unification. This paper dissects all aspects required to formally establish the completeness of the rule-based algorithm, highlighting the significant differences in the formalizations of anti-unification and unification.

ABSTRACT. The challenges of formalization of lambda-calculi in proof assistants do not come only from the adequate representation of binding. Different kind of challenges come from substitution operations which are not based on the conventional replacement of a free occurrence of a variable by a term that lives in the same syntactic class of the variable. Example of such unconventional substitution operations are abundant. In this work we consider four systems with unconventional substitution, two of which are isomorphic to the ordinary lambda-calculus, as a case study in support provided by a mainstream assistant endowed with a library mechanizing a mainstream binding representation. Specifically, we develop a formalization of some basic metatheory in Rocq helped with the Autosubst library. The development profits from the support about binding, but the boilerplate relative to the unconventional substitutions benefits of no automation.

ABSTRACT. Autosubst enables automatic equality-checking up to the sigma-calculus for assumption-free equalities, allowing users to avoid cumbersome reasoning about de Bruijn indices. While effective in many cases, this approach is inapplicable when matching against typing rules, reduction relations, or lemmas, requiring users to either phrase typing rules in a way that they work with Autosubst or even stating explicitly an alternative de Bruijn term. But even without beta-reduction, solutions of matching may be non-unique. This paper presents a work-in-progress method for automatically pattern matching against assumptions, evaluated on standard case studies including the POPLMark and POPLMark Reloaded challenges.

ABSTRACT. In this work, we study the source-target control problem of Boolean networks, which has important applications for cellular re- programming. More specifically, we want to perturb the input Boolean network such that it leaves a predetermined source attractor to eventu- ally find itself in the target attractor. We use edge perturbations, which modify the update functions of a Boolean network without necessarily setting them to constants. This work improves an existing method in which edge perturbations are used to eliminate all but the target attrac- tor. Both approaches are based on Thomas’ first rule: the existence of at least one positive cycle in the interaction graph of a dynamical system is a necessary condition for the existence of multiple steady states. Thus, if all positive cycles are removed, the resulting dynamical system has a single steady state. This requires removing a subset of edges so that at least one edge of every cycle in the graph is perturbed: the feedback edge set. Information on the source and target attractors allows to reduce the number of relevant feedback edge sets and, subsequently, candidate perturbations. We propose a carefully designed strategy that combines exhaustive search and a heuristic inspired by Simulated Annealing to ef- fectively reduce the number of required perturbations with respect to the feedback edge set. We evaluate our method on a wide array of Boolean networks from the literature to demonstrate its efficacy and efficiency.

ABSTRACT. Biochemical systems involve both the flow of matter, in which entities transform into one another via reactions, and the flow of information, in which entities regulate which reactions may occur. Boolean networks capture the latter; reaction networks capture the former. Yet no unified qualitative formalism treats regulated reactions as its principal objects of study, despite their prominence in standards such as the Systems Biology Graphical Notation Process Description (SBGN-PD) language. We introduce modulation-reaction networks (MR-networks), a mathematical framework in which entities modulate reactions through activations and inhibitions, and study their synchronous Boolean semantics. To reason about MR-networks we develop Modulation-Reaction Logic (MRL), a hybrid modal mu-calculus whose modalities reason about the structure of the network and whose fixed-point operators capture temporal evolution of the computation. We establish a collection of validities, including a complete characterisation of the one-step update rule, and demonstrate the expressive power of MRL by formalising properties of biological interest such as reachability, sustained production, and presence of attractors. We show that MRL admits model-checking via an evaluation game, and introduce a bisimulation relation for MR-networks, which is proved to be invariant for all MRL-formulas. As a step towards a biologically more realistic computational model, we sketch the asynchronous semantics of MR-networks, and outline how the developments for the synchronous case transfer to the study of the asynchronous one.

ABSTRACT. Qualitative models provide crucial instruments for modelling complex biological systems. While advances in automated reasoning and symbolic encodings have enabled rigorous inference of these models from data, the process remains highly fragile. First, biological measurement errors inevitably propagate into formal model specifications. Second, when a specification becomes unsatisfiable, distinguishing between fundamental design flaws and minor technical errors is notoriously difficult. This uncertainty often leads to under-specification, as it is unclear which observations are still ``safe'' to incorporate. To overcome these challenges, we introduce a robust inference method based on weighted MaxSMT. By encoding uncertain biological observations as weighted soft constraints, our approach enables the solver to identify a model best reflecting the observations, even with some conflicting constraints. Our method allows for Boolean and multi-valued variable domains, alongside observations derived from discretisation (level constraints) and differential expression (ordering constraints). We show our approach can be used to successfully infer neural cell differentiation models from prior-knowledge networks with 200--1300 genes using ordering constraints on all included genes.

ABSTRACT. Biological regulatory networks can be represented by computational models, which allow the study and analysis of biological behaviours, therefore providing a better understanding of a given biological process. However, as new information is acquired, biological models may need to be revised in order to also account for this new information. Current model revision tools are scarce and often lack the flexibility to integrate with broader analysis workflows. Here, we present pyModRev, an enhanced iteration of the model revision tool ModRev, capable of verifying the consistency of Boolean regulatory models, and finding minimal repairs in case of inconsistency. pyModRev supports model validation against both steady state observations as well as time-series data, being able to consider different update schemes simultaneously. pyModRev supports different model formats, and is available as a Python package in PyPI, for easy integration with other model analysis tools, significantly improving accessibility and utility for the logical modelling community.

ABSTRACT. Automated Essay Scoring (AES) has achieved strong predictive performance with neural and large language models, but often remains opaque. We propose an interpretable AES framework based on Quantitative Bipolar Argumentation Frameworks (QBAFs), representing each essay as an argumentative graph of discourse units linked by support and attack relations. We further augment the graph with feature-derived arguments capturing interpretable essay-level and discourse-unit-level statistics. Experiments show that our approach achieves competitive performance against standard baselines while providing structured explanations, suggesting that QBAFs are a promising formalism for transparent AES.

ABSTRACT. This abstract extends our IJCNLP \& AACL paper published in 2025 with a new study that closes a gap in prior work. It has also been submitted to the 39th International Workshop on Description Logics (DL 2026). Large language models (LLMs) are increasingly applied in domains that demand reliable and interpretable reasoning. While formal reasoning methods can generate correct proofs, these proofs are often inaccessible to non-expert users. This raises a natural question: Can LLMs, when given a proof, faithfully interpret its reasoning and communicate it clearly? Recently, we have introduced \texttt{ProofTeller}, a benchmark that evaluates this ability across three tasks: (1) identifying key proof steps, (2) summarizing the reasoning, and (3) explaining the result in concise natural language. The benchmark covers three domains: \emph{Biology}, \emph{Drones}, and \emph{Recipes}, representing scientific, safety-critical, and everyday reasoning scenarios. We find a consistent near-conclusion bias: LLMs tend to focus on steps closest to the final proof conclusion rather than on the most informative ones. A targeted human study confirms that explanations based on such steps are rated less appropriate for end users. These findings indicate that even when reasoning is provided, current LLMs face challenges in communicating key information in a useful manner, highlighting the need for LLMs that can communicate important details reliably.

ABSTRACT. This is an extended abstract of a paper that has been submitted to the 39th International Workshop on Description Logics (DL 2026). Many techniques have been developed to explain logical reasoning, such as proofs or abduction. However, such methods are useful mainly for experts in logic, e.g., for debugging ontologies. For actually explaining logical consequences and missing consequences to end users of logic-based systems, e.g., in the Semantic Web, it is necessary to study how to adapt and present such explanations in an understandable way. We report on a series of user studies comparing abduction and counterexamples for explaining missing consequences in Description Logic (DL) ontologies, and evaluating the impact of prior knowledge on the level of detail an explanation needs to provide. While we did not find objectively quantifiable results, we analyse and discuss the results of detailed qualitative user interviews, and extract recommendations for executing user studies on logical reasoning systems.

ABSTRACT. Gradual argumentation is a sub-field of Computational Argumentation from symbolic AI which is attracting attention for its ability to support transparent and contestable AI systems. It is considered a useful tool in domains such as decision-making, recommendation, debate analysis, amongst others. The outcomes in such domains are usually dependent on the arguments' base scores i.e. their intrinsic strengths, which must be selected carefully. Often, this selection process requires user expertise and may not always be straightforward. However, organising the arguments by preference could simplify the task. In this work, we introduce \emph{Base Score Extraction Functions}, which provide a mapping from users' preferences over arguments to base scores. These functions can be applied to the arguments of a \emph{Bipolar Argumentation Framework} (BAF), supplemented with preferences, to obtain a \emph{Quantitative Bipolar Argumentation Framework} (QBAF), allowing the use of well-established computational tools in gradual argumentation. We outline the desirable properties of Base Score Extraction Functions, discuss some design choices, and provide an algorithm for base score extraction. Our method incorporates an approximation of non-linearities in human preferences to allow for better approximation of the real ones. Finally, we evaluate our approach both theoretically and experimentally in a robotics setting, and offer recommendations for selecting appropriate gradual semantics in practice.

ABSTRACT. In an era where data-driven machine learning (ML), large language models (LLMs), and agentic AI are clearly improving efficiency in solving complex problems—such as classifying images, answering questions, or playing complex games—solving NP-hard combinatorial problems remains largely dominated by long-developed methods like mathematical programming, constraint programming, or metaheuristics. In this preliminary work, we present two distinct approaches tested to tackle the RCPSP/Max problem, a classic scheduling benchmark that is notably challenging for mathematical programming to find even a feasible solution. One approach focuses on program synthesis using an evolutionary framework powered by an LLM, while the other is based on learning task ranking solutions from optimal solutions using graph neural networks (GNNs) coupled with a LLM-synthetized post-processing procedure to produce feasible schedules. We provide qualitative and empirical conclusions, discuss the true limits of LLM "creativity" and deep learning to solve challenging scheduling problems, and propose avenues for further work.

ABSTRACT. Algorithm selection is important in satisfiability and constraint solving, since no single solver performs best across all instances. Traditional learning-based approaches represent problem instances using expert-designed features to predict solver performance, while recent work explores graph representations derived from ASTs. However, most existing approaches overlook high-level contextual information, such as the application domain or the benchmark origin. In practice, such cues often help practitioners choose an appropriate solver. We present SMT-Select, a multimodal framework for SMT algorithm selection. It learns graph representations from formula ASTs and textual representations from natural-language context descriptions. These representations are then combined to guide solver selection. Evaluated across nine SMT logics, \textsc{SMT-Select} consistently outperforms existing selectors and SMT-COMP winning solvers. Across all evaluated logics, it closes at least 30% of the performance gap between the competition winner and the virtual best solver (VBS), and nearly matches the VBS in two logics.

ABSTRACT. Contrastive learning has recently emerged as a powerful paradigm for training discriminative policies by distinguishing good decisions from bad ones. In this paper, we exploit this idea to learn neighborhood selection in combinatorial optimization, specifically for the Cost Function Networks (CFNs) — a rich framework for representing a global probability distribution or energy function as a combination of local functions. A central inference task is to find a global assignment of all variables with maximum a posteriori probability, or equivalently, minimum energy. We build on \vnsldscp, an anytime incomplete method implemented in the Toulbar2 solver, whose performance hinges on selecting the right variables for repair. Rather than relying on problem-specific heuristics, we propose \clvns a pipeline that extracts positive and negative neighborhood samples from \vnsldscp search trajectories and uses them to train a Graph Neural Network (GNN) with graph attention and a contrastive objective. The resulting model learns to score variables by their relevance for improvement, and is integrated into the \vnsldscp loop to guide the neighborhood construction at inference time. We evaluate the proposed approach on \cfn instances, including challenging minimum-energy problems arising in Computational Protein Design. Experimental results show that \clvns consistently improves solution quality over time compared to the standard \vnsldscp baseline, demonstrating the promise of contrastive learning for guiding combinatorial search.

ABSTRACT. Machine-learned clause-selection heuristics for saturation-based theorem provers seem to follow a simple rule: prefer clauses similar to those that appeared in successful proofs before. Unfortunately, proof search is rarely that cooperative. A closer inspection of Vampire's successful runs reveals a number of surprises. Clauses may contribute to a proof without ever being selected themselves, thanks to simplifications. Under the AVATAR architecture, the situation may become stranger still, with moments in time with literally no future proof clause in sight (i.e., on the passive set). This talk showcases a collection of such phenomena and discusses their implications for learning-guided theorem proving. As we shall see, things can get surprisingly wild in just a few seconds of proof search.

ABSTRACT. We present ProofAtlas, an open-source saturation-based theorem prover for first-order logic with equality, built as an extensible platform for experimenting with neural clause selection. ProofAtlas implements the given-clause algorithm with superposition, and replaces the usual hand-tuned clause-selection heuristic with a neural encoder--scorer that embeds each clause and ranks the unprocessed set against the current proof state. The system is organised as a single Rust proving core exposed through three runtimes: native Python bindings for the command-line prover, the training pipeline, and large-scale evaluation; a WebAssembly build that runs the prover entirely in the browser; and a socket-based deployment that lets many prover workers share a small pool of GPU inference servers. A companion web interface offers both server-side and in-browser proving together with an interactive derivation inspector. We describe the architecture, the integration of neural inference into the saturation loop, and the supporting tooling, and we calibrate ProofAtlas's proving engine against the established provers Vampire and SPASS.

ABSTRACT. This work introduces a concurrent framework for lemma exploration over problems expressed in TPTP syntax. Given such a problem, the framework concurrently generates and performs proof search for multiple equivalent problem variants, where each variant is constructed by augmenting the original with sets of candidate lemmas. The aim of this approach is the effective discovery of proof-aiding lemmas. In this work, lemmas are generated by a large language model (LLM) and injected into their corresponding problem variant only if they are semantically certified using Vampire, i.e. provably entailed by the original problem axioms; Vampire is then used to perform proof search over these lemma-augmented problem variants. Concurrency is present within multiple levels of the framework: during the generation of candidate lemmas, the semantic certification of candidate lemmas, and proof search for lemma-augmented problem variants. This design is scalable and intended to provide a foundation for future work that will extend lemma exploration towards lemma mining, i.e. from the simple discovery of proof-aiding lemmas to their large-scale collection. Utilising GPT-5-mini as the underlying LLM, we evaluate our framework on $655$ group theory problems from the TPTP library. We find that candidate lemmas are: (a) very often syntactically correct, (b) often entailed by their original problem axioms, and (c) can reduce proof-search times. Additionally, we note several instances where a lemma-augmented problem variant obtains a proof, whilst the original problem does not -- including an instance for which Vampire had not previously recorded a proof\footnote{This work is currently under submission elsewhere, hence only the presenting author is included here. Before the Vampire workshop, we will likely expand upon the detailed experiments, such that a broader range of TPTP problems are accounted for, and a broader range of language models are evaluated.

ABSTRACT. We address the quantitative generalization problem in the variadic nominal language. The language combines variadic (i.e., flexible arity) functions with binding structures and freshness constraints. The quantitative generalization problem is concerned with discovering structural similarities of two input expressions, where proximity of function symbols is specified by a given fuzzy relation. We introduce a novel algorithm to compute quantitative generalizations of two variadic nominal input expressions. It combines techniques for handling variable binding with support for variadic expressions and fuzzy proximity.

ABSTRACT. The unification type of an equational theory is defined using a preorder on substitutions, called the instantiation preorder, whose scope is either restricted to the variables occurring in the unification problem, or unrestricted such that all variables are considered. Most of the results on the unification type of equational theories were shown for the restricted setting. In this extended abstract, we recall our recent results on how the unification type may change when going from the restricted to the unrestricted setting.

ABSTRACT. This paper discusses the proof of completeness of an inference-rule-based procedure for absorptive anti-unification. The procedure transforms an input configuration encoding a problem into a set of configurations from which an abstraction grammar produces generalizers. The completeness statement asserts that the procedure generates a complete set of least general generalizers regarding the class of relevant generalizers, which are generalizers restricted to the language of the input problem.

ABSTRACT. Large Language Models (LLMs) are increasingly integrated into organizational workflows, raising growing concerns about their potential abuse for fraud, security breaches, or intellectual property leakage. While LLMs embed protective mechanisms and organizations develop their own guardrails, many practical guardrail approaches remain stateless and lack formal temporal semantics, and existing formal methods are often domain-specific or rely on structured event representations. We propose a runtime verification (RV) framework that treats an LLM conversation as an execution trace that can be formally verified and develop a corresponding tool called Temporal Guard. It observes the stream of user messages and LLM-generated assistant responses, grounds each message into a set of atomic propositions, and thereby constructs a Boolean-labeled trace. Safety policies are specified as formulas in past-time linear temporal logic, and the monitor checks the evolving Boolean trace online to decide whether the conversation satisfies the policy. The central challenge is grounding: bridging the gap between the precise Boolean semantics of temporal logic and the ambiguity of natural language utterances. To address this, we developed a semantic grounding layer and experimentally evaluated a range of grounding strategies, including an embedding-based approach, Natural Language Inference (NLI), and LLM-based zero/few-shot classification. We demonstrate the effectiveness of Temporal Guard through grounding and end-to-end monitoring experiments.

ABSTRACT. Mixture-of-experts (MoE) architectures offer modularity and scalability, yet their robustness, and the practicality of certifying that robustness, in heterogeneous settings are not well understood. This work presents MetaMoE, a heterogeneous MoE framework designed for compositional formal verification. In MetaMoE, a neural network, called a router, classifies an input image's domain and routes it to the corresponding domain expert neural network for fine-grained classification; we study how robustness propagates compositionally across these router and experts and establish when system-level verification can be derived from component-level verification. In homogeneous MoE, all experts share the same task, so a misroute may still preserve correctness if the receiving expert classifies the input correctly; in heterogeneous MoE, experts operate on disjoint class spaces, making any misroute catastrophic. We prove that when the router maintains expert selection under hard routing (k=1) within a perturbation limit, and the selected expert also maintains its classification within that perturbation limit, the end-to-end system robustness is compositional. This enables scalability as the computational power needed for verification and re-verification does not snowball as the system expands. We further complement the formal verification results with empirical experiments, which support the same robustness trends observed under certification. Experiments across 8 MoE configurations and 3 perturbation budgets show that robustly trained (RT) experts improve adversarial accuracy by up to 13.1% over non-robustly trained (NRT) ones and are a prerequisite for formal certifiability -- NRT models on complex domains are completely unverifiable -- while router training paradigm has negligible impact (<0.1%), and verified routers achieve 100% certified robustness accuracy (RoCRA) at practical perturbation bounds. These results outline a principled path toward scalable, verifiable modular AI.

ABSTRACT. Probabilistic verification problems of neural networks are concerned with formally analysing the output distribution of a neural network under a probability distribution of the inputs. Examples of probabilistic verification problems include verifying the demographic parity fairness notion or quantifying the safety of a neural network. We present a new algorithm for solving probabilistic verification problems of neural networks based on an algorithm for computing and iteratively refining lower and upper bounds on probabilities over the outputs of a neural network. By applying state-of-the-art bound propagation and branch and bound techniques from non-probabilistic neural network verification, our algorithm significantly outpaces existing probabilistic verification algorithms, reducing solving times for various benchmarks from the literature from tens of minutes to tens of seconds. Furthermore, our algorithm compares favourably even to dedicated algorithms for restricted probabilistic verification problems. We complement our empirical evaluation with a theoretical analysis, proving that our algorithm is sound and, under mildly re- strictive conditions, also complete when using a suitable set of heuristics.

ABSTRACT. Autonomous systems operating in the real world encounter a range of uncertainties. Probabilistic neural Lyapunov certification is a powerful approach to proving safety of nonlinear stochastic dynamical systems. When faced with changes beyond the modeled uncertainties, e.g., unidentified obstacles, probabilistic certificates must be transferred to the new system dynamics. However, even when the changes are localized in a known part of the state space, state-of-the-art requires complete re-certification, which is particularly costly for neural certificates. We introduce VeRecycle, the first framework to formally reclaim guarantees for discrete-time stochastic dynamical systems. VeRecycle efficiently reuses probabilistic certificates when the system dynamics deviate only in a given subset of states. We present a general theoretical justification and algorithmic implementation. Our experimental evaluation shows scenarios where VeRecycle both saves significant computational effort and achieves competitive probabilistic guarantees in compositional neural control.

ABSTRACT. Current Deep Neural Network (DNN) verifiers are typically designed to prioritize scalability over reliability. Reliability can be reinforced through the generation of proofs that are checkable by trusted, external proof checkers. To date, only a handful of verifiers support proof production; and these rely on verifier-specific formats, and balance between scalability, proof detail, and the trustworthiness of their proof checker. In this tool paper, we introduce PICID, a DNN verifier that produces proofs in the standard Alethe format for SMT solving, checkable by multiple existing checkers. PICID implements a parallel CDCL(T) architecture that integrates a state-of-the-art, proof-producing SAT solver with the Marabou DNN verifier. Furthermore, PICID leverages UNSAT proofs to derive conflict clauses. Our evaluation shows that PICID generates valid proofs in the vast majority of cases and significantly outperforms existing tools that produce comparable proofs.

ABSTRACT. Formal verification of transformers has become increasingly important due to their widespread deployment in safety-critical applications. Compared to classic neural networks, the inferences of transformers involve highly complex computations, such as dot products in self-attention layers, rendering their verification extremely difficult. Existing approaches explored over-approximation methods by constructing convex constraints to bound the output ranges of transformers, which can achieve high efficiency. However, they may sacrifice verification precision, and consequently introduce significant approximation error that leads to frequent occurrences of false alarms. In this paper, we propose a transformer verification approach that can achieve improved precision. At the core of our approach is a novel usage of ReLU, by which we represent a precise but non-linear bound for dot products such that we can further exploit the rich body of literature for convex relaxation of ReLU to derive precise bounds. We extend two classic approaches to the context of transformers, a rule-based one and an optimization-based one, resulting in two new frameworks for efficient and precise verification. We evaluate our approaches on different model architectures and robustness properties derived from two datasets about sentiment analysis, and compare with the state-of-the-art baseline approach. Compared to the baseline, our approach can achieve significant precision improvement for most of the verification tasks with acceptable compromise of efficiency, which demonstrates the effectiveness of our approach.

ABSTRACT. The abstract of the talk can be found in the PDF file as requested.

ABSTRACT. Non-clashing teaching, introduced by Kirkpatrick et al. [ALT 2019] and Fallat et al. [JMLR 2023], is the most efficient batch machine teaching model satisfying the collusion-avoidance benchmark of Goldman and Mathias [COLT 1993]. In the past few years, (positive) non-clashing teaching for the concept class of balls in graphs has been thoroughly studied, yielding numerous algorithmic and combinatorial results. This concept class also exhibits broad generality, as any finite binary concept class can be equivalently represented by a set of closed neighborhoods in a graph. In this talk, I will survey the complexity landscape of non-clashing teaching in graphs. I will present some of our recent results, including near-tight running time upper and lower bounds for general graphs, parameterized algorithmic and hardness results, and combinatorial bounds for broader graph classes.

ABSTRACT. Gerrymandering, the process of deliberately redistricting via manipulation of boundaries to favor a chosen candidate, is a recurring issue in elections. A standard setting to model voting is when voters and ballot boxes are located in $\mathbb{R}^2$, distances are computed using $\ell_2$-norm, the voting rule is plurality and each voter is assigned to vote at the opened ballot box nearest to them. Eiben et al. [AAAI '20] designed an optimal algorithm for the question where given a set $\mathcal{B}$ of $m$ ballot box locations and a set $\mathcal{V}$ of $n$ voters with known preferences over a set of candidates $\mathcal{C}$, the computational question is to decide if some $k$ ballot boxes can be opened from $\mathcal{B}$ such that a chosen candidate from $\mathcal{C}$ wins in at least $\ell$ of these ballot boxes? Gerrymandering seeks to exploit the fact that \emph{``all ballot boxes are equal"}, i.e., it doesn't matter how few voters voted at a ballot box or how small was the margin of victory as long as your chosen candidate wins. This is reflected in the lower bound construction of Eiben et al. [AAAI '20] where one ballot box gets only 9 votes while another ballot box has more than $(3/4)$-fraction of the $2^{O(k)}$ voters voting in it. In this paper, we study the question of how the complexity of Gerrymandering changes if we enforce a fairness condition that any two opened ballot boxes cannot have a big difference in how many voters are voting in them? Formally, given any integer $\beta\geq 1$, the \fgm problem has the additional condition that the ratio of the number of voters voting in any two of the opened ballot boxes is at most $\beta$. We completely resolve the complexity of \fgm by: \begin{itemize} \item Designing an algorithm running in $(m+n)^{\beta\cdot |\mathcal{C}|\cdot O (\sqrt{k})}$ time \item Obtaining a lower bound that there is no $f(k,n)\cdot m^{o(\sqrt{k})}$ time algorithm (for any computable function $f$) under the Exponential Time Hypothesis (ETH) even when $|\mathcal{C}|=2$. \end{itemize} Our lower bound construction is able to reduce the number of voters $n$ to be $\text{poly}(k)$ whereas Eiben et al. [AAAI '20] required it to be $\text{exp}(k)$.

ABSTRACT. We present a variation of Maehara's method to construct Craig-Lyndon interpolants for the three-valued propositional logic of here and there (HT), also known as Gödel's G₃, a superintuitionistic logic of importance in logic programming. Our method adapts a recent interpolation technique that operates on classically encoded logic programs to a variation of Mints' sequent system for HT. The approach is characterized by two stages: First, a preliminary interpolant is constructed, a formula that is an interpolant in some sense but not yet the desired HT formula. In the second stage, an actual HT interpolant is obtained from this preliminary interpolant. With the classical encoding, the preliminary interpolant is a classical Craig-Lyndon interpolant for classical encodings of the two input HT formulas. In the presented adaptation, the sequent system operates directly on HT formulas, and the preliminary interpolant is in a nonclassical logic that generalizes HT by an additional logic operator.

ABSTRACT. In this paper we focus on the intersection of two important results: Russellian theory of definite descriptions (RDD) and Craig interpolation theorem (CIT). RDD provides the most recognisable approach to formalisation of complex terms. CIT is one of the most important metalogical results hence it is crucial to show that it holds for a theory like RDD. One of the possible ways of proof-theoretic characterisation of RDD was provided by means of a cut-free sequent calculus satisfying the subformula property. In the paper we apply this system to obtain a Maehara-style constructive proof of CIT for RDD.

ABSTRACT. We establish the Lyndon interpolation property for basic lattice expansion logics (LE-logics) in arbitrary signatures using display calculi. Our approach is {\em constructive}, yielding interpolants algorithmically from derivations, and {\em modular}, in the sense that interpolation for axiomatic extensions can be obtained by verifying a local interpolation property for the analytic structural rules corresponding to the additional axioms. To this end, we identify a class of \emph{interpolation-safe} structural rules preserving local Lyndon interpolation. As applications of the general framework, we show that the tense version of Holliday's fundamental modal logic enjoys the Lyndon interpolation property.

ABSTRACT. We present an approach that solves a general class of problems that require combinatorial and probabilistic reasoning, for example, synthesizing a policy that satisfies first-order logical constraints in an underlying uncertain environment modeled as a family of MDPs. Our approach is to embed probabilistic model checking as a theory within an SMT solver. This leverages the practical advantages of both tools. We use the resulting tool to find policies that are robust, i.e., they perform well on perturbations of the MDP, and that satisfy additional structural constraints regarding, e.g., their representation or implementation cost. These constraints can be flexibly specified in a first-order theory over a set of MDPs.

ABSTRACT. Stochastic processes give a mathematical representation of the probabilistic changes of a random system over time. Verification techniques use these representations to reason about quantitative behavioural properties, such as termination probabilities and probabilistic safety guarantees. Under the compositional view of probabilistic modelling in which probability is modelled by a monad, stochastic processes have a natural coalgebraic interpretation as coinductively generated stochastic structures. This allows for a structured and succinct expression of both discrete-time and continuous-time stochastic processes in higher-order probabilistic programming languages admitting lazy structures, such as LazyPPL. In this presentation, I will show that omega Qbs, a mixture of quasi-Borel spaces and complete partial orders, supports these higher order constructions of various stochastic processes, such as i.i.d measures, Markov chains, Brownian motion and stochastic differential equations.

ABSTRACT. We introduce the Causal Transition Calculus (CTC), a multi-layered framework that integrates intervention-based reasoning, process algebra and modal logic to characterise actual causality in concurrent systems. We show that CTC is sound and complete for the modified Halpern&Pearl notion of causality, providing a correspondence between causal reasoning over process-algebraic models and their induced labelled transition systems. This new framework for causality is work in progress.

ABSTRACT. Causal reasoning is central in many applications, but mechanized support for it in expressive logical environments remains limited. We present a shallow semantical embedding of recursive causal models in classical Higher-Order Logic (HOL) and a corresponding Isabelle/HOL implementation within the \logikey\ framework. The embedding represents causal formulas as HOL predicates over families of structural equations, interventions as updates of these families in HOL, and solutions of recursive models through a constructive solver based on a topological order over endogenous variables. This yields direct mechanized support for the language of causality with interventions. We validate the embedding by mechanically verifying the axioms of the language. The work extends \logikey\ with mechanized support for causal models and illustrates how HOL can be used to rapidly prototype logics together with reusable theorem proving and model finding support.

ABSTRACT. The philosophical analysis of actual causation has relied on neuron diagrams (NDs) and structural causal models (SCMs). Both have helped sharpen the concept, but they only represent the end states rather than the dynamic development of the system, and theories of causation often employ unlawful counterfactuals, requiring ad hoc repairs like normality orderings. We introduce models from the field of concurrency theory, a field that deals with dynamic processes. NDs are translated into labeled transition systems with histories and independence relations. The resulting model supports a temporal logic with backtracking modalities, reordering of independent events, and causal modalities. We define several formulae that capture different notions of causation and apply them to standard vignettes (preemption, conjunction, trumping, double prevention). Unlike most approaches, the analysis remains within lawful states.

ABSTRACT. We ask the question: given a rule, like `Do Not Walk on the Grass', how can we figure out when it's OK to relax it? This can be thought of as figuring out the \textit{reason} for the rule, with the rule itself being just a particular application of this reason to a given context. For instance, the reason for `Do Not Walk on the Grass' is that `The grass should be preserved for everyone to enjoy'. Figuring out the reason allows us then to properly decide whether it is OK to modify the rule or relax in a given context. We offer a formalization of this analysis in the language of counter-factual programming. Since our behavior (and intentional behavior in general) is caused by our reasons and not just by mechanical causes, this can be seen as a formalization of Aristotle's teleological cause. Elucidating reasons for behavioral rules could be combined with more classical mechanical causality analysis to yield better designs of artificially intelligent agents.

ABSTRACT. We discuss two influential views of unification: mutual information unification (MIU) and common origin unification (COU). We propose a simple probabilistic measure for COU and compare it with Myrvold's (2003, 2007) probabilistic measure for MIU. We then explore how well these two measures perform in simple causal settings. After highlighting several deficiencies, we propose causal constraints for both measures. A comparison with explanatory power shows that the causal version of COU is one step ahead in simple causal settings. However, slightly increasing the complexity of the underlying causal structure shows that both measures can easily disagree with explanatory power. The upshot of this is that even sophisticated causally constrained measures for unification ultimately fail to track explanatory relevance. This shows that unification and explanation are not as closely related as many philosophers thought.

ABSTRACT. We present IsaSearch, an automatic, self-contained system for natural-language search over Isabelle developments. The system extracts formal Isabelle content, translates it into informal descriptions using large language models, and indexes these descriptions for semantic search. At search time, the system optionally applies query expansion to improve robustness against short or imprecise queries. The system supports different Isabelle and Archive of Formal Proofs (AFP) versions, language models, and prompts without changes to the implementation. We evaluate the approach by searching the AFP using benchmarks derived from Wiedijk's "Formalizing 100 Theorems". The results show that semantic search over generated natural-language descriptions of Isabelle content is effective.

ABSTRACT. This paper reports on the design, content development, tooling, and first-year experiences of using the Isabelle Platform for a compiler construction course with fourth-year engineering students at Université Paris-Saclay/Polytech. The course covers formal grammars, several parsing techniques, syntax-directed translation, and code generation for a fragment of a processor instruction set architecture (ISA). While formal proofs remain out of scope for this class, the Isabelle platform still offers numerous advantages: it is easy to install across major operating systems, features an IDE with relevant SML libraries, and can be set up to work with Lex/Yacc-like tools. Furthermore, we describe how Isabelle’s document-preparation facilities (via Isabelle/DOF) were deployed to provide students with a consistent, formally checked, and practically rewarding learning environment for both specification and implementation activities. Finally, we share observations and lessons learned from the initial run of this class within the fourth-year computer science program.

ABSTRACT. As the software industry shifts toward memory-safe languages, automated reasoning pedagogy must evolve to bridge the gap between industrial practice and formal verification. We explore the integration of AutoCorrode, a framework for reasoning about imperative Rust-like code within Isabelle/HOL into computer science curricula. We demonstrate its utility through a worked example of an iterative Fibonacci function, illustrating how students can apply Hoare logic and separation logic to modern imperative paradigms.

ABSTRACT. We explain that cautious and brave semantics in Consistent Query Answering naturally extend from Boolean queries to numerical queries, where they are known as range semantics. We then apply this extension to numerical queries that are conjunctive queries with aggregation, under primary key constraints. In particular, we highlight results from~\cite{DBLP:journals/pacmmod/KhalfiouiW24, DBLP:conf/icdt/KhalfiouiW26} on computing range semantics via rewriting in aggregate logic.

ABSTRACT. Abduction is the task of computing a sufficient extension of a knowledge base (KB) that entails a conclusion not entailed by the original KB. It serves to compute explanations, or hypotheses, for such missing entailments. Little is known about abduction when erroneous data results in inconsistent KBs. In this paper we investigate abduction under repair semantics, and discuss complexity results on deciding existence of and verifying abductive solutions fulfilling additional criteria that are useful in the presence of inconsistencies. In particular, we consider different repair semantics and the description logics DL-Lite and EL_bot.

ABSTRACT. We present our recent work towards an end-to-end ASP-based system for handling inconsistent data. Our first contribution introduces a declarative rule-based framework for specifying and computing a priority relation between conflicting facts. Such priority relations have been used to define three kinds of optimal repairs (Pareto-, globally-, and completion-optimal), which can be used in place of classical repairs to define repair-based semantics. Our second contribution is an implementation of the optimal repair-based variants of three such semantics (AR, brave and IAR) using answer set programming (ASP) and its extension ASP(Q). In particular, this is the first implementation of the globally-optimal repair-based semantics, which are computationally more challenging. We also implement the grounded semantics, a tractable under-approximation of the optimal repair-based semantics rooted in abstract argumentation. These two components are key steps towards a complete pipeline for handling inconsistent data using priority relations. This extended abstract summarizes the main ideas behind each component and the takeaways from our experiments.

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. Recent work on Vampire enabled checking of proofs in Lean end-to-end, greatly increasing trust in the found proof. This work presents an approach under development, which takes a generic TPTP proof in the CNF and FOF fragment, uses Vampire to reconstruct the inferences, and chain resulting Lean proofs to a single end-to-end Lean proof, transferring the increased trust to foreign ATP systems capable of producing suitable TSTP proofs.

ABSTRACT. The Thousands of Problems for Theorem Provers (TPTP) Problem Library constitutes the standard benchmark for automated theorem provers. We provide a tool that allows the import of TPTP Problem Library instances in first-order form (FOF), clause normal form (CNF) and monomorphic and polymorphic typed first-order form (TFF) as expressions in the interactive theorem prover Lean. This makes the TPTP Problem Library available as a benchmark for automation tools in Lean that aim to facilitate writing proofs in Lean. We compare the results of the tactics Duper, Lean-SMT and Grind with the results of Vampire.

ABSTRACT. First-order logic is the basis for many knowledge representation formalisms and methods. Providing technological support for learning to write first-order formulas for natural language specifications requires methods to test formulas for (non-)equivalence and to provide explanations for non-equivalence. We propose such methods based on both theoretical insights and existing tools, implement them, and report on experiments testing their effectiveness on a large educational data set with > 100.000 pairs of first-order formulas.

ABSTRACT. We present SigmaKEE-rs, a re-implementation of the Sigma Knowledge Engineering Environment (SigmaKEE) in the Rust programming language, designed to serve as an ontological datastore backed by embedded theorem proving. A key contribution of this work is the integration of the Vampire theorem prover as an embedded library rather than as an external process, via extended Rust–C++ Foreign Function Interface (FFI) bindings built on the vampire-rs Rust library. We extend these bindings with support for Vampire’s type system and clausification machinery. Using this strategy, the entire baseline ontology, the Suggested Upper Merged Ontology (SUMO), is eagerly normalized, deduplicated, and held in an in-memory datastore alongside an incrementally maintained SUMO Inference Engine (SInE) relevance index. Subsequent queries bypass Vampire’s parsing and the bulk of its preprocessing, invoking only clausification and the saturation engine on a relevance-filtered axiom set. We describe the engineering challenges encountered in adapting Vampire into a reusable component suitable for real-time, multi-query workloads, and report preliminary performance results comparing the embedded approach with the traditional process-based invocation model used in the original Java-based SigmaKEE.

ABSTRACT. Acquiring correct action theories from informal specifications remains a central challenge in KR. Large Language Models can generate plausible domain models from natural language, but the resulting theories frequently contain missing preconditions, incorrect effects, or superfluous actions. Existing refinement approaches either require human experts to correct these errors or assume that the input specification is itself correct. We present a framework that iteratively refines LLM-generated action theories using formal explanations grounded in SAT-based verification. Each candidate theory is encoded as a bounded SAT problem and tested against solvable tasks, which must admit a valid plan, and unsolvable tasks, which must be correctly rejected. When a test fails, we extract a formal explanation that pinpoints the specific theory constraints responsible for the failure, and feed this explanation back to the LLM to guide its next revision. Our initial evaluation across six planning domains shows that our framework can converge to correct theories.

ABSTRACT. Large language models (LLMs) exhibit strong general capabilities, but their deployment in high-stakes domains is hindered by their opacity and unpredictability. Recent work has taken meaningful steps towards addressing these issues by augmenting LLMs with post-hoc reasoning based on computational argumentation, providing faithful explanations and enabling users to contest incorrect decisions. However, this paradigm is limited to pre-defined binary choices and only supports local contestation for specific instances, leaving the underlying decision logic unchanged and prone to repeated mistakes. In this paper, we introduce ArgEval, a framework that shifts from instance-specific reasoning to structured evaluation of general decision options. Rather than mining arguments solely for individual cases, ArgEval systematically maps task-specific decision spaces, builds corresponding option ontologies, and constructs general argumentation frameworks (AFs) for each option. These frameworks can then be instantiated to provide explainable recommendations for specific cases while still supporting global contestability through modification of the shared AFs. We investigate the effectiveness of ArgEval on treatment recommendation for glioblastoma, an aggressive brain tumour, and show that it can produce explainable guidance aligned with clinical practice.

ABSTRACT. Understanding the internal `thinking' process of Large Language Models (LLMs) and the cause of hallucinations remains a key challenge. To this end, we introduce latent debate, a structured surrogate framework for interpreting model outputs on True/False prediction tasks through the lens of internal latent arguments and interactions amongst them. Unlike human debates, latent debate captures the hidden supporting and attacking signals that arise within a model during a single inference. We first present a model- and task-agnostic conceptual framework, and then instantiate it symbolically to approximate the thinking process of LLMs towards binary decisions. Empirical studies demonstrate that our latent debate is a faithful structured surrogate model that has highly consistent predictions with the original LLM, while providing a form of interpretability. We also demonstrate that our latent debate provides a strong baseline for hallucination detection. Specifically, we identify strong correlations between debate patterns and hallucinations, such as a high degree of disagreement in the middle layers of the latent debate surrogate is linked to a higher risk of hallucinations. Our findings suggest that latent debate shows potential to analyze internal signals in LLMs for binary decision settings.

ABSTRACT. Causal Assumption-based Argumentation (ABA) has been proposed as a causal discovery method with increased guarantees on the correspondence of the discovered causal graphs to a subset of the input constraints that drive the search for the causal relations. Heuristics are currently used to identify the optimal subset of constraints and infer the most likely corresponding graphs. Minimal Unsatisfiable Sets (MUSes) and Minimal Correction Sets (MCSes) have been explored in the Answer Set Programming (ASP) literature to create explanations and repair logic programs (LPs). We leverage the correspondence of stable semantics between ABA and LPs to investigate the benefits and drawbacks of MUSes and MCSes when applied to the causal discovery task carried out by Causal ABA. We define the notion of optimal MCSes and show how they can be computed by leveraging standard optimisation constructs such as weak constraints. We then empirically show that optimal MCSes, integrated into Causal ABA for causal discovery, substantially (i) increase the identification rate of true constraints; (ii) reduce the number of compatible causal graphs in output; (iii) improve graph reconstruction according to standard metrics.

ABSTRACT. We propose a family of local inconsistency measures for graph databases subject to Regular Path Constraints, grounded in an origin-based semantics that scopes constraint evaluation to a designated subset of nodes. We formalize this notion, study the properties of the proposed measures with respect to a set of postulates, and illustrate their behavior on a running example. Our framework enables fine-grained inconsistency assessment, surfacing localized violations that global measures may fail to detect.

ABSTRACT. Reachability is a central question in term rewriting: can a given target term (e.g., an error state) be reached from a start term? It is also an important property in confluence analysis, and corresponding tools compete in the annual confluence competition. An interesting generalization of this problem is handling programs that can make random choices during execution. For such probabilistic programs, reachability becomes a quantitative property instead of a qualitative one: instead of asking whether the target is reachable, one asks with which probability it is reached. We lift reachability analysis from ordinary term rewriting to probabilistic term rewrite systems. To do so, we formalize the maximal probability of reaching a target term and adapt two techniques for analyzing reachability (based on symbol transition graphs and on term orderings) to compute upper bounds on this probability.

ABSTRACT. In an earlier paper we proved that a transformation due to Snyder generates all canonical TRSs equivalent to a given canonical ground TRS. Here we present an explicit recursive procedure to generate these. We prove its correctness and show how the procedure can be used to obtain the exponential upper bound due to Snyder on the number of canonical ground presentations.

ABSTRACT. Generalized Term Rewriting Systems (GTRSs) extend traditional term rewriting systems by providing a highly expressive framework that integrates conditional rules, context-sensitive constraints, and Horn clauses directly into the rewriting formalism. Recently, we have extended the tools infChecker and MU-TERM to support GTRSs. In this work, we exploit our previous extensions of infChecker and MU-TERM for GTRSs to extend CONFident with corresponding capabilities for proving confluence.

ABSTRACT. We formalize strong barbed similarity for the $\pi$-calculus in the Beluga proof assistant, completing a line of work addressing the Concurrent Calculi Formalization Benchmark. By extending previous developments to include replication, we give a coinductive encoding of behavioral equivalence based on barbs and internal actions. Using Beluga’s copattern-based coinduction, we obtain concise and compositional proofs, including compatibility properties and a context lemma characterizing barbed precongruence. The case study demonstrates the effectiveness of combining HOAS and coinductive reasoning for mechanizing concurrent calculi.

ABSTRACT. This paper introduces the strategy language of Pgeon, a meta-prover with a clear separation between inference rules and proof search. We give the semantics of strategies as functions over proof states, and of the operators that are used to combine them, allowing for sequential composition, choice, repetition and interleaving of strategies. This language is designed to handle the challenge of fair proof search in semi-decidable logics, where simple depth-first exploration of the proof space is not guaranteed to achieve completeness. We showcase the expressiveness and effectiveness of the approach through case studies in first-order and modal logics.

ABSTRACT. Kappa is a graph-rewriting language originally developed for modeling molecular interactions in cellular processes. A key feature of Kappa models is that, inspired by organic chemistry, interaction rules operate on patterns i.e., partially specified molecular species, thus allowing compact descriptions of otherwise large or even infinite models. In this paper, we propose and implement a framework for statistical model checking for stochastic Kappa models against properties written in bounded linear temporal logic (BLTL). A key feature of our approach is that temporal properties operate over Kappa patterns, making the specification language native to Kappa and avoiding the expensive—and sometimes theoretically impossible translation of the model into an equivalent chemical reaction network with a finite number of species. Concretely, given a Kappa model and a property, we first instrument the model by introducing additional variables and observables that track the truth value of each atomic proposition. For each simulated trace, the BLTL formula satisfaction is evaluated using an offline monitoring procedure. Finally, the satisfaction probability is statistically estimated from repeated model simulations. The proposed model checking framework enables a systematic exploration of behavioral properties of Kappa models, that is computationally efficient while able to capture stochastic and finite size effects with any predefined desired accuracy/precision. As such, it can serve in applications for e.g. model selection, property-driven parameter exploration, or robustness analysis. The framework is illustrated on representative case studies from systems biology and swarm robotics.

ABSTRACT. Bursty transcription in single cells typically produces over-dispersed, skewed, and sometimes heavy-tailed expression distributions that are explained by two-state Markov models of the promoters. While the gold standard for simulation is exact stochastic sampling with Gillespie's algorithm, obtaining thousands of timed traces is computationally costly. Surrogate models based on stochastic differential equations (SDEs) are widely used to speed up this simulation process. An example is the Chemical Langevin Equation based on Gaussian noise, which, however, does not capture heavy-tailed noise. In this work, we present a unified SDE framework that combines deterministic drift, Gaussian fluctuations, and additive sporadic jumps of arbitrary distributions, and provide an open-source Python implementation, bcrnnoise. The framework subsumes standard surrogate models and allows for vectorized generation of batches of transcription traces. We assess computational speed and accuracy of common surrogate models along with new models, showing that high accuracy can be obtained while reducing computational cost up to two orders of magnitude.

ABSTRACT. Reaction Systems (RSs) provide a successful qualitative modelling framework inspired by biochemical reactions. In a RS a computation starts from a initial state given by a set of entities and each following computation state is determined by the application of all the enabled reactions to the previous state. RSs can also model the interaction with the environment. Each entity can either be present or absent in a computation state, as a crisp boolean condition, and also reactions are (or not) enabled under crisp conditions. This framework has proved to have many applications for modelling biomedical and computer science systems, but it can become restrictive when laboratory measurements exhibit graded concentrations, partial inhibition, and noise. We thus introduce Mamdani-driven Fuzzy Reaction Systems (M-FRS), as a graded conservative extension of RSs. Each reaction in the style of RSs is now interpreted as a Mamdani rule, and we formalise a single four-stage fuzzy inference cycle (fuzzification, rule evaluation, aggregation, optional defuzzification) which defines a deterministic discrete-time graded update operator. Fuzzy inference yields a discrete dynamical system. As a first case study, we develop a compact M-FRS model of the hypothalamic--pituitary--thyroid axis.

ABSTRACT. Kappa offers a modeling environment to describe, simulate, and reason about rule-based models. It has been used to model protein-protein interaction networks, especially models of signaling pathways. Kappa comes with a static analyzer, KaSa, to assist the modeler and assess the consistency of the models. Although efficient, KaSa is sometimes too slow to reason while modifying large models or when editing models within the user interface. Here, we propose an incremental version that updates the result of the current analysis at each model modification. Our approach relies on the use of an abstraction of the relationships between the rules of the model and the properties that they induce. Partial evaluation is used when some rules are removed, to exclude the results that derive from the removed rules. Adding rules is done classically by resuming the iterations of the analysis algorithm. This incremental analysis is available on the command-line or as an electron app, and it is evaluated on examples from the literature.

ABSTRACT. Recent research has established complexity results for the problem of deciding the existence of interpolants in logics lacking the Craig interpolation property (CIP). The proof techniques developed so far are non-constructive, and no meaningful bounds on the size of interpolants are known. Hybrid modal logics (or modal logics with nominals) are a particularly interesting class of logics without CIP: in their case, CIP cannot be restored without sacrificing decidability and, in applications, interpolants in these logics can serve as definite descriptions and separators between positive and negative data examples in description logic knowledge bases. In this contribution we show, using a new hypermosaic elimination technique, that in many standard hybrid modal logics Craig interpolants can be computed in fourfold exponential time, if they exist. On the other hand, we show that the existence of uniform interpolants is undecidable, which is in stark contrast to modal or intuitionistic logic where uniform interpolants always exist.

ABSTRACT. In the past two decades, significant research and development effort went into the development of verification tools for individual languages, such as C, C++, and Java. Many of the used verification approaches are in fact language-agnostic and it would be beneficial for the technology transfer to allow for using the implementations also for other programming and modeling languages. To address the problem, we propose SV-LIB, an exchange format and intermediate language for software-verification tasks, including programs, specifications, and verification witnesses. SV-LIB is based on well-known concepts from imperative programming languages and uses SMT-LIB to represent expressions and sorts used in the program. This makes it easy to parse and to build into existing infrastructure, since many verification tools are based on SMT solvers already. Furthermore, SV-LIB defines a witness format for both correct and incorrect SV-LIB programs, together with means for specifying witness-validation tasks. This makes it possible both to implement independent witness validators and to reuse some verifiers also as validators for witnesses. If possible It would be great if this talk could occur during the first day of the workshop, i.e, July 24th.

ABSTRACT. Imprecise probability generalizes standard probability theory by replacing a single distribution with a convex set of possible distributions. We show that this generalization requires no change to the standard BDD compilation and weighted model counting pipeline used by discrete probabilistic languages. An imprecise coin flip is simply a BDD variable whose weight is left free rather than fixed. We introduce “Imp", a Haskell embedded DSL for imprecise probabilistic programming. A graded monad, indexed by finite sets of named sources of epistemic uncertainty, restores the commutativity that the standard convex powerset monad lacks, and GHC's type system enforces this at compile time. Weighted model counting is parametric in the semiring, so the same compiled BDD supports exact, differentiable, and interval-bounded inference.

ABSTRACT. Anytime MaxSAT solving is indispensable in applications that require finding near-optimal solutions within a flexible, user-controlled time budget. Recent years have seen substantial progress in anytime MaxSAT algorithms, including the introduction of SAT-based local search, the development of efficient approximation techniques, and significant advances in classical local search methods. However, all leading anytime solvers—including the winners of the three most recent MaxSAT Evaluations (MSEs) in the anytime categories—reuse the code base of a single solver, tt-open-wbo-inc. While highly efficient, this code base lacks an in-memory API, is non-incremental and incomplete, and contains a substantial amount of dead and legacy code. We introduce Aperture, a new solver for SAT-based optimization, including MaxSAT, written from scratch in C++ with in-memory APIs for C++ (IPAMIR-compliant) and Python. For MaxSAT, Aperture is anytime, incremental, and complete; algorithmically, it follows a similar high-level approach to tt-open-wbo-inc, but employs a unified flow for both weighted and unweighted MaxSAT. Performance-wise, Aperture is highly competitive as a MaxSAT solver. Under the benchmark sets and evaluation conditions of MSE 2024, it outperforms both the MSE 2024 winner SPB-MaxSAT-c and tt-open-wbo-inc in all four anytime categories, and in 8 out of 12 anytime categories across the three most recent MSEs (2022–2024). Moreover, Aperture outperforms leading non-anytime MaxSAT solvers on 2 out of the 6 incremental benchmark sets from MSE 2022, an evaluation setting in which—unlike the anytime categories—both incrementality and completeness are mandatory. Beyond MaxSAT, Aperture also supports other paradigms for optimizing an objective function under Boolean constraints, including Optimization Modulo Bitvectors (OBV) and black-box optimization. Across all supported paradigms, the solver is incremental and anytime; it is complete for MaxSAT and OBV, but incomplete for black-box optimization.

ABSTRACT. Implicit Hitting Set (IHS) Solving has been a successful solving paradigm in maximum satisfiability (MaxSAT) and has also recently been ported to pseudo-Boolean optimization (PBO). In a nutshell, the IHS algorithm iteratively solves an underconstrained version of the original optimization problem, which we refer to as the hitting set (HS) problem. A solution to the hitting set problem is then attempted to be extended to a solution to the original problem. If the solution cannot be extended, a new constraint is added to the hitting set problem. Traditionally, the hitting set problem has been solved using an integer linear programming solver. We propose instead using the pseudo-Boolean solver RoundingSat, which supports VeriPB proof logging, as well as local search, to solve the HS problem. This allowed us, for the first time, to provide a certifying IHS solver, which participated in the Pseudo-Boolean Competition 2025. However, it is very challenging to create a certifying IHS solver that is competitive with uncertified IHS solving. This is evident in the concurrent work (Ihalainen et al., AAAI 2026), where introducing certification results in a major hit in performance. The hitting set solver is being run on a problem with a growing number of constraints, and a major challenge is how to recycle information between calls rather than solving the HS problem from scratch every time. Our solution is to use additional activation variables to keep track of which constraints remain valid in between calls, but adapting solver heuristics and constraint post-processing techniques to this setting is highly nontrivial. In our presentation, we will explain some of the technical challenges involved and then report on experimental results from our work-in-progress implementation in the solver RoundingSat, which shows that proofs for all solved instances can be verified by VeriPB and the formally verified checker CakePB. Our preliminary experiments show that performance can be made competitive with uncertified IHS solving with SCIP as the hitting set solver.

ABSTRACT. Maximum Satisfiability (MaxSAT) is an optimization extension of the Satisfiability (SAT) problem. In Branch-and-Bound (BnB) MaxSAT solving, the quality of the lower bound estimation is critical for effective search space pruning. State-of-the-art BnB solvers typically estimate this bound by identifying disjoint inconsistent subformulas (cores) via Unit Propagation (UP). However, a limitation of this standard approach is that UP fails to detect cores that exhibit complex dependencies with already identified cores. In this paper, we propose a further lookahead algorithm that leverages pre-detected cores to uncover additional disjoint inconsistencies, thereby tightening the lower bound. Experimental results demonstrate that the proposed algorithm significantly tightens the lower bound, enabling the state of the art BnB solver MaxCDCL to solve more instances.

ABSTRACT. The increasing integration of deep neural networks in critical systems has spawned a theoretical and practical interest in formally guaranteeing safety properties about their behavior. To achieve this, contemporary verification algorithms rely on computing linear relaxations for a network's non-linear activation functions. Existing approaches for linear relaxations typically fall into one of two categories: single-neuron relaxation, in which each activation neuron is bounded in terms of its sources; and multi-neuron relaxation, in which linear bounds involving multiple activation neurons and their sources are calculated. However, existing methods might fail to balance tightness and scalability, as single-neuron bounds might not derive sufficiently tight bounds necessary for verification to complete, whereas generating multi-neuron relaxation for all activation neurons is computationally expensive. In this paper, we present a middle-ground approach featuring partial multi-neuron relaxation, in which we generate multi-neuron bounds for only a small, heuristically selected subset of neurons. To achieve this, we build upon existing branching heuristics for selecting neurons and for optimizing bounding hyper-planes for multi-neuron bounds. We integrated our proposed method within the Marabou verifier, and obtained favorable results in comparison to existing bound tightening methods. Our experiments showcase the potential of our technique for neural network verification.

ABSTRACT. We present our ongoing work on implementing and benchmarking scalable SAT-based procedures for query answering under variants of three well-known inconsistency-tolerant semantics (AR, brave and IAR) based on two notions of optimal repairs (Pareto- and completion-optimal) that exploit a priority relation between conflicting facts. We focus in particular on comparing different SAT encodings that can handle non-binary conflicts.

ABSTRACT. Description logic (DL) knowledge bases (KBs) built by hand or (semi)automatically using machine learning or information retrieval tools may contain errors, often detected when reasoning derives an inconsistency. However, not all errors cause an inconsistency, but such errors may be noticed when reasoning produces a consequence that follows from the KB, but does not hold in the application domain modelled by the KB. In fact, some application-relevant DL KBs such as the large medical ontology SNOMED CT are even written in DL dialects such as E L that cannot even express an inconsistency. Getting rid of an inconsistency or an unwanted consequence by removing a minimal amount of information from the KB is usually called repair in the DL literature. Instead of producing a single new KB as repair, inconsistency-tolerant reasoning takes all repairs of a detected inconsistency into account, e.g., by producing only consequences that follow from all (in a certain way preferred) repairs. This notion can be extended to repairs that remove an unwanted consequence, but this variant has been investigated in less detail. The purpose of this paper is to show that certain results for inconsistency-tolerant reasoning can easily be transferred to error-tolerant reasoning. To this purpose, it concentrates on results that link inconsistency-tolerant reasoning for prioritized KBs to certain notions of extensions in argumentation frameworks (AFs). The paper shows that these results, originally proved for inconsistency-tolerant reasoning in certain DL-Lite dialects, can easily be transferred to error-tolerant reasoning for KBs written in the DL EL.

ABSTRACT. When using datalogMTL over a dense timeline and inconsistent data, there can be several kinds of repairs as recently defined in [BBK-IJCAI25]. One of such kind is pointwise repairs for which no method for deciding existence for DatalogMTL is known. In this paper, we consider datalogMTL^\diamondminus, a fragment of datalogMTL, which has diamond minus as the only temporal operator and a bounded dataset. We develop a computation algorithm that returns pointwise repairs for this setting.

ABSTRACT. In this work, we provide an overview of our recent work on SHACL validation, satisfiability and containment, and specifically relate it to the setting in which SHACL constraints are paired with an ontology. This allows for combining employing database constraints to detect inconsistencies with domain knowledge to reduce gaps in the data: both standard techniques to address current data plagued by quality issues.

ABSTRACT. We present a framework for computing special constant-preserving (scp) generalizations in anti-unification (or generalization) modulo equations. Our approach is motivated by interaction composition in distributed systems, where preserving designated constants is crucial for consistent synchronization between partial behaviors. To address this, we extend a rule-based scp generalization algorithm with a variant-based mechanism, enabling reasoning modulo equational theories while enforcing constant-preservation constraints.

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. Safety-critical deployment of machine learning models requires unambiguous specification and verified implementation of tensor operators. This paper presents a formally verified pipeline based on the Why3 deductive verification platform. The pipeline takes each operator from an abstract WhyML specification over mathematical tensors to extracted C code, via a concrete implementation on flat arrays linked by a machine-checked refinement proof. A reusable library supports the development, providing abstract tensor types, a row-major layout with proven bijectivity, and a refinement mapping to a C-level representation. We illustrate the workflow on several ONNX operators, developed within the SONNX Working Group. Finally, we demonstrate how the abstract specifications compose to enable contract-based verification of functional properties of complete networks. The methodology is applicable beyond ONNX to any framework requiring verified tensor implementations.

ABSTRACT. Graph neural networks (GNNs) have become a prominent approach for developing fast, topology-aware surrogates in electric power systems, supporting tasks such as power flow (PF) analysis, optimal power flow (OPF) estimation, and cascading failure analysis (CFA). Despite this growing use, formally verifying GNN-based models remains challenging, with existing methods limited in scope. We extend the neural network verification (NNV) framework to graph-structured inputs through GraphStar sets, a generalization of Star sets that captures uncertainty over both node and edge features. This extension enables the propagation of linear message-passing operations and the sound approximation of ReLU nonlinearities for GNN architectures, including graph convolutional network (GCN) and graph isomorphism network with edge features (GINE) layers. We evaluate GNNV across three power system tasks, PF, OPF, and CFA, on the IEEE-24, IEEE-39, and IEEE-118 test cases, as well as two standard graph classification benchmarks, ENZYMES and PROTEINS. Our results show that GNNV provides tighter robustness guarantees than CORA on graph classification models with ReLU-based activations and, for the first time, delivers edge-aware robustness guarantees for GINE-based PF and OPF models under joint node and edge perturbations.

ABSTRACT. Vision-Language Models (VLMs) struggle with explainability and tasks requiring step-by-step reasoning. This paper proposes a neuro-symbolic framework that leverages both logic and neural networks for interpretable results; chaining together convolutional neural networks (CNNs), computer vision techniques, and Satisfiability Modulo Theories (SMT). We introduce a challenging benchmark suite of KenKen and Sudoku puzzles, both NP-complete in the general case. Provided with an unsolved board image, these puzzles require image decomposition, constraint evaluation, and error detection/correction, making it a relevant benchmark suite for VLMs. We compare our neuro-symbolic framework against five state-of-the-art VLMs: Gemini-2.5-Pro, GPT-4o, GPT-4o-mini, Claude Sonnet 4.0, and Qwen2.5-VL-7B-Instruct. These VLMs have significant difficulty solving Sudoku or KenKen puzzles beyond 4x4 grids. The neuro-symbolic framework achieves 100% accuracy on computer-generated characters for all classes. For handwritten characters, we demonstrate the neuro-symbolic can correct image decomposition errors, improving solve rate. Overall, the benchmark is used to demonstrate the neuro-symbolic framework outperforms state-of-the-art VLMs while providing explainable reasoning to enable the self-correction of error. The benchmark suite consists of 2200 board images: seven classes of KenKen puzzle and four classes of Sudoku, for both computer-generated and handwritten characters.

ABSTRACT. While neural networks have achieved remarkable success across a wide range of application domains, their predictions remain brittle when confronted with adversarial perturbations. To enable their responsible deployment in safety-critical settings, neural network verification techniques have been developed to formally establish input–output properties of interest. However, even state-of-the-art verification systems such as α,β-CROWN, the winner of the Verification of Neural Networks Competition (VNN-COMP) since 2021, may fail to prove challenging properties within reasonable time budgets. Fully exploiting the capabilities of such systems typically demands careful tuning of numerous parameters, a process that often relies on substantial domain expertise and extensive manual experimentation. In this work, for the first time, we apply automated algorithm configuration to α,β-CROWN using SMAC3, thereby eliminating the need for labour-intensive manual tuning. We show that, given a carefully designed parameter search space, automatically discovered configurations can achieve performance comparable to expert-crafted configurations, even when using relatively modest computational budgets for the optimisation process. We evaluate our approach on the benchmarks from the regular track of VNN-COMP 2025 and demonstrate that the automatically configured version of α,β-CROWN achieves a higher overall score than the author-provided configuration when applying the scoring scheme of the competition.

ABSTRACT. With AI increasingly deployed in safety-critical systems, providing formal robustness guarantees for the underlying models is essential. Existing verification methods either rely on overly conservative approximations or incur prohibitive computational costs. For example, the use of $\ell_p$-norm perturbations in video settings encodes the belief that the adversary can inject noise in every video frame. In practice, adversarial perturbations exhibit structured spatial and temporal correlations, constrained to lower-dimensional, semantically meaningful subspaces. In this work, we study robustness verification of \emph{3D convolutional neural networks} (3D CNNs) processing video and volumetric inputs, targeting applications in action recognition (UCF-101), autonomous driving (Udacity), and medical imaging (MedMNIST) exploiting realistic assumptions on adversarial strength by modelling them as spatio-temporal constraints --- where the attacker can modify either a subset of frames or patches within a set of consecutive frames. We demonstrate that modelling realistic constraints enables tighter approximations, particularly in CNNs. We introduce \emph{Spatio-Temporal Bound Propagation} (STBP), a verification framework that computes an exact closed-form characterization of the first convolutional layer and propagates certified bounds through subsequent layers using scalable approximations. Computing the exact closed-form provides the tightest bounds for the first convolutional layer. Thus, we utilise approximation methods in the remainder of the network. To spur further progress in this field, we propose \texttt{ST-Bench}, a verification benchmark for autonomous driving and activity recognition, to systematically evaluate verifiable robustness. Compared to existing verification and training-based approaches, STBP provides stronger robustness guarantees with significantly improved scalability, achieving up to $1.7\times$ higher certified robust accuracy under identical perturbation budgets.

ABSTRACT. We report on the design and implementation of a verification condition generator (VCG) for fractional separation logic in Isabelle, developed primarily using Eisbach with lightweight Isabelle/ML extensions. Rather than focusing on the underlying logic itself, this paper concentrates on the engineering of the proof automation infrastructure. We present a modular VCG architecture based on explicit normalization, controlled rule applica- tion, frame inference, and configurable verification-condition handling. During the implementation effort, several reusable proof-engineering patterns emerged, including combinator-style Eisbach methods, dispatch based on subgoal shape, configurable failure behaviour for debugging and strict modes, and an orthogonal mechanism for deferring verification conditions. In addition, we describe auxiliary tools developed during the project, such as a focused goal deferral mechanism (SDefer) and a theorem-search tool for named theorem collections. While the implementation targets a specific separation logic, many of the presented techniques are largely independent of the underlying logic and may be useful for Isabelle automation more broadly.

ABSTRACT. Responsibility allocation is a fundamental problem in the analysis of distributed systems: How do we attribute individual contributions to a joint outcome? Petri nets are a model of distributed (concurrent) systems in which actors are represented by transitions. We propose the notion of forward-responsibility of coalitions of such actors as the existence of a winning strategy in a game played against the remaining transitions, with the objective of avoiding bad places. In our formalisation we introduce a novel game model on Petri nets, where a central concept is precedence determining priorities between conflicting transitions. We show how to compute forward-responsibility in Petri nets via a reduction to imperfect information games and demonstrate the expressiveness of our framework by encoding existing models of responsibility allocation. This allows us to adopt a new perspective and attribute responsibility not only to actors, but also directly to actions.

ABSTRACT. Scheduling is a highly relevant aspect of industrial work. From assigning jobs to machines to creating shift plans for employees; schedules must be created to ensure efficiency, cover requirements and adhere to working regulations. As creating schedules while keeping track of all constraints is often a notoriously difficult job, automated methods can be employed. However, sometimes no solution can be found due to conflicting problem specifications. In this case, it is important to explain which constraints contribute to infeasibility and how the problem can be relaxed. We study the Rotating Workforce Scheduling Problem, for which we develop a framework that generates explanations for instances with incompatible constraints. We show how Minimal Correction Sets can be used to provide detailed explanations for infeasible problems, caused by hard constraint violations or by conflicting optimisation goals. We perform a case study and experiments on (real-life) instances that reveal that explanations can be efficiently generated.

ABSTRACT. Formal explainability methods provide logic-based explanations with precise semantic guarantees, yet they often require full access to a model's symbolic encoding. Sample-based approaches relax this requirement by deriving explanations from finite observations of model behavior, but existing methods largely produce static explanations that ignore user context and domain constraints. This paper proposes a framework that integrates sample-based formal explainability with restricted constraint reasoning, where constraints encode user preferences as inclusion and exclusion of features. We show that, under these restrictions, the validation of the existence of both abductive and contrastive explanations can be decided in polynomial time. We further embed this mechanism into a dialogical framework that allows users to interactively refine constraints and obtain adapted explanations without sacrificing formal guarantees. A running example illustrates how the dialogue evolves as constraints are revised.

ABSTRACT. We investigate how the recently proposed framework of answer set programming with quantifiers (ASP(Q)) can be applied to the task of computing step-wise explanation sequences for the classic puzzle game Sudoku.

ABSTRACT. Miller and Tiu’s generic quantification (i.e., the ∇ quantifier) brings a logical treatment of the common concepts of name and freshness. Unlike the related fresh quantifier of nominal logic, generic quantification has been defined proof theoretically. In fact, several generic quantifiers have been considered. In the earlier version, nabla is defined as a self-dual quantifier commuting with all propositional connectives. Later, it has been extended to satisfy two additional properties: ∇x.∇y.F is equivalent to ∇y.∇x.F; ∇x.F is equivalent to F if x does not occur in F. Together, the two properties imply nominal logic’s equivariance principle. While they have not been considered independently so far, it is natural to consider the two properties individually, giving rise to four quantifiers. Taking inspiration from substructural proof theory, we call the first property exchange and the second one weak- ening, and define uniformly four logics through proof systems with substructural generic contexts. We then consider the problem of giving a (sound and complete) truth seman- tics for these logics. We build upon earlier work by Goubault-Larrecq, which proposed a complete semantics for Miller and Tiu’s early nabla quantifier, and show that (enriched) nabla sets can be used to define, in a uniform way, a semantics for the four substructural generic logics. We show that this semantics is sound and complete for three of the logics, defined through their natural (classical) sequent calculi. However, we identify a mismatch for the case where nabla satisfies weakening but not exchange: in that case, the natural proof system is not sound for our semantics.

ABSTRACT. This paper examines the foundational distinctions between proof theory and dependent type theory (DTT) in the design of interactive theorem provers. While several implemented systems are designed using the dependently typed lambda-calculus to represent proofs, no major proof assistant is designed using modern structural proof theory, even though, as I will argue here, the sequent calculus offers a compelling alternative framework. Six specific topics are proposed where the proof-theoretic perspective is arguably superior to the DTT perspective. These topics include the separation of logic from proof structure, the strategic use of non-determinism in proof reconstruction, and the avoidance of complex typing-discipline issues such as universe levels and proof irrelevance. The final topic---the treatment of bindings---is further developed to demonstrate how a natural, intensional approach is achieved through the mobility of binders. This methodology is illustrated via the Abella theorem prover, which leverages lambda-tree syntax and the nabla-quantifier to provide an elegant environment for reasoning about the meta-theory of languages and logics involving complex binding.

ABSTRACT. Recent advances in automated reasoning have led to the development of powerful tools for solving complex problems in domains such as verification, theorem proving, and planning. A key component of many of these tools is tailored SAT solvers. Historically, SAT solvers have relied on a very aggressive backtracking strategy, called non-chronological backtracking. To preserve clean invariants, the addition of new clauses to the solver forces it to backtrack, even when the new clause is already satisfied. This can lead to significant performance degradation. Chronological backtracking is a more conservative approach. With weaker invariants, it is more resilient to the addition of new clauses. This scheme can be further improved to support the addition of arbitrary clauses non-falsified, without requiring any backtracking. While CB addresses inefficiencies at the SAT level, it is still ignorant of the cost of flipping literals. Graph Backtracking is a new technique for SAT solvers that allows the user to provide a cost heuristic to guide the backtracking process. The SAT engine is then dissuaded from undoing expensive literals. In this presentation, we explore how chronological and graph backtracking can be integrated into Vampire, and more specifically into AVATAR. AVATAR combines the strengths of SAT solvers with first-order saturation by splitting the search space into smaller, more manageable parts using a SAT solver. Graph backtracking can be used to guide the splitting process and preserve expensive literals as long as possible. We will discuss the challenges and benefits of integrating these techniques into AVATAR, and present preliminary results on their impact on the performance of the solver. This work is still in progress. As such, we will welcome suggestions and feedback from the community on how to best integrate these techniques.

ABSTRACT. Modern first-order theorem provers are usually presented as logical engines: they transform conjectures into clauses, saturate a search space under inference rules and terminate, when successful, with a proof or countermodel. This talk proposes a complementary view: a prover such as Vampire is also a highly structured combinatorial optimization system. Its central computational difficulty is not merely the validity of a formula, but the disciplined allocation of scarce search resources across an enormous space of possible clauses, inferences, simplifications, splittings, theory calls and strategy schedules. The starting point is the observation that saturation-based theorem proving already contains many objects familiar to combinatorial optimization and operations research. Clause selection resembles online scheduling under uncertainty; literal selection and term ordering resemble priority design in discrete search; redundancy elimination functions as dominance pruning; AVATAR-style splitting introduces a branch-and-cut like interaction between first-order reasoning and propositional control; portfolio modes instantiate algorithm-selection and resource-allocation problems. In this perspective, a successful Vampire run is not only a derivation in logic, but also an efficiently managed search process whose performance depends on implicit operational decisions. The proposed contribution is a research agenda for making these operational decisions explicit. I argue for treating prover strategy design as a mathematically analyzable optimization problem over proof-search policies. Rather than asking only which heuristic performs well on a benchmark class, we can ask which structural features of a problem justify a particular inference budget, splitting policy, simplification frequency or theory reasoning schedule. This reframes heuristic engineering as policy synthesis: a prover becomes a system that continuously solves a meta-level optimization problem while it searches for an object level proof. This viewpoint also suggests new application areas from algorithms and operations research. Many results in combinatorial optimization depend on certificates: infeasibility proofs, dominance arguments, valid inequalities, decomposition cuts, approximation bounds and correctness proofs for reductions. Vampire-like provers could serve as certificate auditors for optimization pipelines, checking whether a preprocessing rule preserves optimality, whether a decomposition cut is logically valid, or whether an algorithmic reduction from one discrete problem to another is sound under stated assumptions. Conversely, OR can contribute sharper evaluation methodology for theorem proving: performance profiles, ablation-aware benchmarking, budgeted portfolio design, robust strategy selection and instance-space analysis. The talk will focus on the implementation consequences of this synthesis. What prover internals must be exposed to support OR-guided strategy control? Which proof-search traces should be logged to make unsuccessful case studies scientifically useful? How should benchmarks be designed when the relevant object is not merely theorem/non-theorem status, but the cost structure of reaching a proof? Finally, I identify missing features in current provers: richer proof-search telemetry, optimization-aware strategy languages, interfaces for external policy learners and certificate formats that connect first-order derivations with optimization models. The broader claim is that substantial progress in theorem proving may require not only stronger calculi, but a more explicit theory of proof search as an optimization problem. Vampire is an especially natural testbed for this agenda because its architecture already sits at the intersection of saturation, SAT/SMT interaction, portfolio reasoning, finite model construction and practical proof engineering.

ABSTRACT. Forward subsumption and subsumption resolution are among the most performance-critical redundancy elimination techniques in saturation-based theorem proving. Vampire implements both using Clause Code Trees, where clauses from the search space are compiled into sequences of matching instructions (CodeOps) arranged in a trie. The trie structure allows common prefixes across different clauses to be merged, reducing the total number of CodeOps. In a standard Clause Code Tree, literals of the same clause form a path inside the trie. That means common prefixes between literals within the same clause cannot be merged. A Wide Clause Code Tree addresses this by flattening all literals into a single shared trie, enabling intra-clausal sharing. While this seems like an obvious optimization, it turns out to be surprisingly hard to implement efficiently. The core problem is that the standard Clause Code Tree structure allows for very efficient pruning techniques based on literal depth and matching compatibility. This structure is lost in Wide Trees. Pruning turns out to be essential, as the savings from exploiting inter-literal overlap are far smaller than those gained from pruning. Attempts to recover pruning via index interval propagation reduced executed CodeOps significantly, even below the original Clause Code Tree implementation, but the per-branch overhead of interval checking outweighed the savings. CodeOp execution is simply too cheap for any non-trivial bookkeeping to be affordable. Wide clause code trees remain an open problem and this talk discusses the above approaches and current directions.

ABSTRACT. In this paper, unification is considered as a simple theorem prover in which variables to be solved are directly represented by free logic variables. This approach is different from other works which consider unification as the application of a set of rewrite rules. The benefit of the approach this paper considers is naturalness, clearness and uniform framework. The theorem prover is not in full setting. Since programming formulas are fixed and simple a few rules, goal formulas are matched with the left hand-side of rewrite rules. The theorem prover acts like a term rewriting system. But when free logic variables are at the top, they are subject to search. This paper considers the solution of this technical problem.

ABSTRACT. We present an E-unification procedure for a set of non-ground (dis)equations, along with a dynamic set of ground (dis)equations, and prove its completeness. The ground part is dynamic in the sense that it continually changes. The algorithm saturates the non-ground equations using Superposition modulo the ground theory. We also have an Instantiation rule that matches the left hand side of non-ground (dis)equations with ground terms, creating new ground (dis)equations, which changes the ground theory. This algorithm can be used in quantified SMT problems, where the dynamic ground theory represents the evolving model. We develop an ordering to compare terms modulo a ground theory, which is used to orient non-ground equations. We prove properties of this ordering, using a weak form of monotonicity and subterm property. We finally present a set of inference rules for our ordering, which allows us to properly orient equations in theories of some finite data structures, such as a theory of finite lists with length and append.

ABSTRACT. It is well-known that Boolean unification is unitary with constants, but only finitary with function terms. However, any discriminator theory may be expanded with function terms without loss of unification type provided that they satisfy a certain compatibility condition. We construct an isomorphism between compatibly expanded and nonexpanded Boolean rings, allowing us to reason about compatibly expanded Boolean rings via correspondence. Additionally, we show that the result generalizes to $p$-rings expanded with compatible unary function terms. This additionally shows that the compatible function terms are not injective, even when restricted to terms generated without ring connectives, which renders them unhelpful for many of the applications of general Boolean unification.

ABSTRACT. Matching and unification have been introduced in Description Logic as non-standard reasoning problems with applications in ontology engineering. For the DL EL, it was shown that both problems are NP-complete, but some special cases of matching are tractable. Surprisingly, it turned out that for unification the complexity increases to PSpace if one disallows the use of the top concept to build concept descriptions. However, the effect of disallowing the top concept has not been investigated for matching. We show that a similar increase in complexity applies to matching when the top concept is not allowed.

ABSTRACT. Given a set of equations E, one is often interested in proving (or disproving) E-*validity* of equations s=t, i.e., whether s and t are *equivalent* with respect to E, written s =_E t. Assume that E can be turned into a Term Rewriting System R which is *confluent* and such that the equational theory of E_R, obtained by replacing `->' by `=' in all rules of R, coincides with that of E. Then, s =_E t and R-*joinability* of s and t, i.e., checking whether s ->*_R u and t ->*_R u holds for some term u, coincide. Termination of R is useful to check such joinability: just rewrite s and t until no further reduction is possible to obtain s' and t'; then compare them for syntactic equality. Using term rewriting for proving E-validity with *non-terminating* systems R, though, is underexplored to date. In this paper we show how to use *Context-Sensitive Rewriting* (where only selected arguments of function symbols can be rewritten) to prove and disprove E-validity, even if R is *not* terminating.

ABSTRACT. Constraint satisfaction problems underlie many resource allocation and scheduling decisions. When feasible solutions affect individual stakeholders, a solver that returns a single high-quality solution may systematically favor some individuals over others, even when many equally valid solutions exist. In this paper we address fair decision making for combinatorial optimization problems of the kind routinely solved with popular frameworks such as SAT solvers, constraint programming, or integer programming. We study (first-level) distributional max-min fairness for constraint satisfaction problems, whereby the solver outputs a probability distribution over feasible solutions that maximizes the expected utility of the least-favored stakeholder. We propose an approximate algorithm based on the multiplicative weights update framework, where each iteration calls an oracle for a weighted version of the original CSP. Preliminary experiments with a variety of solvers show that our approach can be practical on NP-hard benchmark problems for which state-of-the-art solvers are effective.

ABSTRACT. Pseudo-Boolean solving adapts the revolutionary conflict-driven clause learning (CDCL) algorithm from Boolean satisfiability (SAT) to the much more expressive paradigm of 0-1 integer linear programming. Conflict analysis for 0-1 integer linear programming requires applying cuts to constraints, which transform constraints to constraints that are implied over the Booleans but not necessarily over the reals. It also requires weakening constraints, which focuses constraints more on the conflict and can make cuts more effective. In this work-in-progress paper, we systematically study a number of different cut rules and different methods to weaken constraints. Our preliminary experimental evaluation agrees with some theoretical expectations, but also provides some unexpected results and shows that different benchmark families benefit from different cut rules.

ABSTRACT. The Quadratic Assignment Problem (QAP) consists of finding a permutation that minimizes a quadratic objective function. Exact methods generally rely on a branch-and-bound procedure, the efficiency of which depends heavily on the quality of its lower bound. In integer linear programming, several bounds have been investigated, exhibiting different trade-offs between speed and quality. The Gilmore-Lawler bound appears to be the most commonly used in practice. It requires solving a linear assignment problem (LAP) for each variable-value pair. We show how to obtain this bound using Singleton Node Consistency (SNC) and LAP. In Cost Function Networks (CFNs), we propose a reformulation that transforms the result of applying LAP to a given variable-value pair into cost functions of arity 1 and 2, which can be added to the original problem. Combined with existing lower bounds for CFNs, including EDAC and a recent CFN propagator for AllDifferent, this method (SNC-LAP-GLB), used as a preprocessing, significantly increases the initial lower bound and accelerates the search, resulting in competitive results on the QAPLIB benchmark. We then propose an extension of the AllDifferent propagator for the Global Cardinality Constraint. It allows us to exploit variable symmetries on some challenging QAPLIB instances, thus improving the results. Last, we report some preliminary results obtained by an automatic configuration tool for tuning the solver parameters.

ABSTRACT. We present an Isabelle/HOL mechanisation of rely-guarantee reasoning combined with separation logic, developed on the seL4 trace monad: an Aczel-style trace model that makes environment interference first-class. We follow Feng's local rely-guarantee (LRG) because its frame rule fits the seL4 Microkit framework we target: a static-architecture setting in which components, their memory-region mappings, and the communication channels between them are fixed at build time. The development so far has: (i) LRG's frame and hide rules, mechanised over the trace monad's primitives, sequential composition, and while loops; (ii) an n-ary parallel composition rule; and (iii) a three-component Microkit case study (a producer/filter/consumer pipeline over shared memory regions) composed by the n-ary parallel rule.

ABSTRACT. This talk will present two case studies on verification interfaces at both ends of the seL4 operating system kernel's bulk of formal specifications in Isabelle/HOL. Reaching deep into the concrete depths, our efforts to prove that seL4 enforces time protection, the absence of timing leaks through microarchitectural state, rely entirely on a new hardware–software contract. Meanwhile, up where verified user-level programs would need to rely formally on a suitable abstraction of seL4's system call behaviour, there stands a long-unbridged kernel–userland gap: what developers would expect from reading seL4's reference manual is not quite yet what's been proved. We will examine how the urgent need to clarify both interfaces arose and what we are doing about it at UNSW, offered as data points for discussion on what it can take to provide a trustworthy body of software through formal methods and mechanised verification in Isabelle.

ABSTRACT. This is a brief and mostly LLM-written (but human checked/rewritten) report on my recent experience with agentic autoformalizaton using Isabelle. We discuss the problems encountered and solutions developed during an LLM-assisted autoformalization of Munkres’ Topology (§§12– 85) in Isabelle/HOL. The project (200,000+ lines, 4,000+ commits, described in [1,2]) has surfaced a range of issues that we believe are representative of large-scale LLM–ITP interaction. The proposed talk at the workshop will likely discuss some of these issues and perhaps more.

ABSTRACT. We present a stratified normalisation completion procedure for rewriting systems over linear precategories. Our approach relies on a stratification of the set of rewriting rules according to their confluence and termination properties. We introduce stratified termination functions to establish termination for such systems. We illustrate the method on several classes of algebraic structures, including associative and diagrammatic algebras. In these contexts, we show how the stratification of defining rules can be used to compute hom-bases effectively.

ABSTRACT. We describe *completion* procedures to obtain *strongly confluent* TRSs from a set of equations. Strong confluence implies confluence *without requiring termination*. We show the performance of our implementation in TRS.Tool 2 by means of some benchmarks.

ABSTRACT. Propositional formulas frequently contain implicitly defined variables, and extracting their explicit definitions is often useful. Following the standard proof of Beth's definability theorem, these definitions can be obtained as Craig interpolants of formulas expressing implicit definability. In practice, one calls a SAT solver for each defined variable and extracts an interpolant from the resulting resolution proof. We propose an alternative approach where a single resolution refutation serves as a witness of definability for a set of variables. We then present a simple modification of standard interpolation systems that constructs a multi-output circuit representing all definitions in one pass over this proof. The running time and circuit size are $O(nm)$, where $n$ is the number of defined variables and $m$ the proof size. Preliminary experiments on Boolean functional synthesis benchmarks show that the single refutation witnessing definability is produced at least as quickly as the sequence of proofs of a per-variable baseline, but that the multi-output circuits are typically larger, sometimes substantially so on instances with many definitions. Extraction that asymptotically improves upon $O(nm)$ is identified as the main open question.

ABSTRACT. Many real-world systems require balancing several conflicting quantitative objectives simultaneously. For instance, randomized retry protocols must trade off reliability against latency and communication overhead, while autonomous robotic systems must balance safety, energy consumption, and task completion time. Such systems are naturally modeled as probabilistic programs, where quantitative reasoning about multiple objectives becomes essential. We present a predicate transformer approach to multiobjective verification for probabilistic programs. Our work combines ideas from weakest preexpectation calculi and multiobjective model checking to compute Pareto fronts (that is, optimal values for several objectives) directly at the program level.

ABSTRACT. Client server systems are one of the largest programming paradigms. Crypto exchanges with an unbounded number of investors, multiplayer games where the number of players are not known apriori and services with an unbounded customer base are instances of unbounded client server systems. We focus on client server systems with single server and unboundedly many clients, where the number of clients are not known apriori and there can be unbounded concurrent interactions between the clients and server. The major challenges are to identify the suitable model to abstract the behaviour of the systems, to identify suitable logics to specify the properties and to identify formal techniques for verifying the properties on the model. In this talk, we discuss the formal modeling, encoding , verification algorithm to exploit concurrency. We also discuss the suite of formal verification tools for client server systems with unbounded clients using classes of nets and various suitable logics to represent their properties.

ABSTRACT. Weakest pre-expectations are the probabilistic program analogue to weakest preconditions in classical programs. Deductive veri!cation approaches aim to establish bounds on these quantitative expectations. Their automation has been successful in analysing a variety of discrete probabilistic programs. Key routines in that automation require reasoning about (partially unrolled) loops, however, the logical representation of weakest pre-expectations on such unrollings often explodes. In this talk, we will present typed extended decision diagrams (TEDDs), inspired by various extensions to binary decision diagrams in classical planning. We demonstrate computing WPs represented as TEDDs, SMT-based pruning to further shrink their representation, and we lift some proof rules for loops to operate on TEDDs. Experimental results demonstrate that TEDDs boost the scalability of deductive probabilistic program veri!cation by orders of magnitudes over the state of the art.

ABSTRACT. Incorrect or incomplete specifications often give rise to critical AI safety risks, such as reward hacking and unpredictable edge-case behaviors. To prevent AI agents from exploiting these vulnerabilities, verification methods should perform checks under a variety of different and unexpected conditions, and this demands incorporating causal counterfactual reasoning. This is a preliminary work on sabotage logic which leverages different types of deletions and allows one to reason about the causal and counterfactual dependencies.

ABSTRACT. Propensity scores (PS) are an effective strategy for controlling for bias when estimating causal effects from observational data. Nevertheless, traditional methods often struggle with complex treatment structures beyond binary or discrete treatments. In this context, this work introduces a methodology for propensity score estimation that accommodates generalized treatment structures without imposing restrictive parametric assumptions. We use a probabilistic classification model to estimate stabilized weights and propensity scores via density-ratio estimation, making our method adaptable to various treatment forms. Experimental results show notable performance improvements in accuracy and stability across different synthetic and semi-synthetic datasets, even as the number of covariates increases. This suggests that our approach is flexible enough to be considered for challenging real-world applications in causal effect estimation, such as healthcare, policy analysis, and personalized marketing.

ABSTRACT. We address the problem of computing actual causality, as defined by Halpern and Pearl for the explanation of predictions made by Neural Networks. Most existing explanation methods assume feature independence, which can yield misleading explanations when inputs exhibit structured dependencies. We formalize explanations via Halpern and Pearl actual causality with SCMs, reducing cause search to a verification problem solved via differentiable relaxations and branch-and-bound. We perform preliminary experiments and show that our method outperforms state-of-the-art approaches in scalability and completeness.

ABSTRACT. Counterfactuals -- statements about what *might* have happened under different circumstances -- offer a natural way to phrase causal questions and have gained increasing prominence in machine learning, with applications ranging from medical decisions to discrimination. We argue that, while counterfactuals are powerful philosophical constructs, the computation of *individual* counterfactual trajectories is riddled with dangers. Individualized counterfactuals are often not useful or even harmful, because the required assumptions cannot be adequately justified or because counterfactuals are conceptually misaligned with what would be informative for the task at hand.

ABSTRACT. A prominent claim in the foundations of causal reasoning in artificial intelligence—most influentially associated with Judea Pearl—is that contemporary machine learning systems remain confined to associative reasoning and therefore lack genuine causal competence. According to this view, explicit structural causal models are a necessary prerequisite for answering interventional or counterfactual questions. We argue that current practice already challenges the strongest interpretation of this claim. Modern machine-learning-based systems, particularly when embedded in interactive or agentic settings, exhibit forms of behavior that cannot be cleanly classified as purely associative, including intervention-like reasoning, explanation-seeking dialogue, and responsibility attribution. The contribution is not to reject formal causal frameworks, but to expose a growing mismatch between formal definitions of causation and the descriptive reality of deployed computational systems. This mismatch raises foundational questions directly relevant to formal reasoning about causation, responsibility, and explanation.

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. Explainable Reinforcement Learning (XRL) seeks to make Reinforcement Learning (RL) policies more transparent and interpretable, a key requirement in safety-critical and human-centric scenarios. However, it is mostly based on user studies, thus targeting the needs of a specific audience and lacking shared evaluation metrics. On the other hand, logic-based approaches within eXplainable Artificial Intelligence (XAI) provide compact, human-readable abstractions of decision-making. However, the systematic quantification of the explainability degree of logical representations remains an open problem. This work aims to advance the state of the art in XRL by introducing objective and planning-oriented metrics for policy explainability in single-and multi-agent RL settings. At the same time, it contributes to the field of logics for XAI by providing a principled way to quantify the explainability of logical rules, moving beyond common-sense assessments and simple propositional fragments. We employ Inductive Logic Programming (ILP) to extract symbolic representations of RL policies and define a novel set of explainability metrics, including \textit{activation rate}, \textit{feature coverage}, \textit{syntactic distance} and \textit{semantic distance}. These metrics quantify alignment between symbolic rules and agent behavior, the role of features in decision-making, and the evolution of policies during training and across agents in single and Multi-Agent RL (MARL). Experiments across different RL domains show that the proposed metrics highlight action-specific learning dynamics beyond global return, provide fine-grained insights into domain features beyond classical approaches for global feature importance estimation, and uncover coordination, specialization, and adaptation patterns in MARL. Moreover, they provide crucial insights for the transfer and generalization of action-specific policies. Our framework advances XRL by offering rigorous, objective, and interpretable metrics to evaluate symbolic policy representations. This contributes to understanding, debugging, and refining RL agents, paving the way for more robust and trustworthy applications in dynamic, safety-critical, and multi-agent environments.

ABSTRACT. Neural networks (NNs) are the core of AI-based technologies. However, the degree of reliability in performing the task is an open problem. The explainability of a central task of NNs, classification, is of immense importance. While at the rise of AI-based reasoning, explainability of the NN classification has mostly been done using statistical methods, nowadays, a more reliable trend of formal logic-based methods is gaining popularity. The advantage of the formal approach is that it gives strict and provable guarantees of the classification. Formal methods is a mature field that has delivered a number of efficient computational solutions already applied in the analysis of software and hardware systems. Formal explainability methods naturally have the ability to reuse existing techniques and tools for a newly emerging field of formal explainability of NN classification. This paper surveys existing efforts to compute explanations of neural network classification based on logical abductive reasoning. The abduc- tion approach is crucial for generalizing the results, capturing the underlying behavior of the classifier. We present the existing techniques as instances of a general formalization that allows contrasting them against each other. In addition, we discuss the issue of the quality of explanations, focusing on their key metrics and factors. As an illustrative example, the paper also presents a practical framework, SpEXplAIn, which automatically computes Space Explanations, the most general abduction-based explanations for classifying NNs with provable guarantees of the behavior of the network in continuous areas of the input feature space. The tool leverages an SMT solver compatible with a range of flexible Craig interpolation algorithms and unsatisfiable core generation, and is applicable to a wide range of applications.

ABSTRACT. In knowledge distillation, a student model learns from the outputs produced by a teacher model. Recent studies have shown that, beyond explicit task knowledge, student models may also acquire hidden behavioural traits from teacher models, a phenomenon known as subliminal learning. Yet, its underlying mechanism remains unclear. In this paper, we use argumentative explanations to investigate this phenomenon. Specifically, we represent Multi-layer Perceptron (MLP)-based teacher and student models as quantitative bipolar argumentation frameworks (QBAFs), and apply argument attribution explanations (AAEs) to measure the contribution of each argument to the final output argument. Our experimental results show that student models exhibiting subliminal learning are more closely aligned with their teacher models in AAE patterns than non-subliminal student models.

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.