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 standard trick for proving hypersafety properties is to build a product program and reason about the multiple behaviours of multiple copies in the context of a single program. But there are many choices for the product program, and any choice is only as good as the runs you choose to include in it. Verification (especially the automated variety) may succeed or fail depending on this choice. This talk tells that story as a sequence of escalating challenges—from sequential to concurrent to recursive programs—on how an effective state space of product programs can be defined and algorithmically used for effective hypersafety verification.

ABSTRACT. Learning-based methods, such as reinforcement learning, are receiving increasing attention for solving challenging control tasks. However, the lack of safety assurances about learned controllers poses a significant barrier to their practical deployment. In this talk, we will present a framework for learning and formally verifying neural controllers for tasks specified via temporal logic specifications. The framework is applicable to stochastic dynamical systems, thus also taking into account environment uncertainty. Given a specification and a probability bound, the framework jointly learns and formally verifies a controller together with a formal certificate of the specification being satisfied with at least the desired probability, both parametrized as neural networks. Certificates are supermartingale-like objects that can be effectively used to formally reason about stochastic systems in a fully automated fashion. The talk will touch upon several aspects of the neural control problem, including learning of neural controllers from temporal logic specifications, formal verification via neural certificates, and safety assurances upon runtime deployment.

ABSTRACT. Causal representation learning (CRL) is a new and exciting research direction in causality and representation learning that aims at learning meaningful high-level causal variables from low-level representations (e.g. images or videos) in an unsupervised way, while providing theoretical guarantees on their identifiability/correctness or the disentanglement of their representations. For example, given a video of agent performing actions in a simulated environment, temporal CRL methods are able to learn in a low-dimensional latent space a representation of the causal variables, e.g., the individual objects and their attributes, up to permutations and element-wise transformations with respect to the ground truth ones. This enables us to have a disentangled or "steerable" latent space, which allows us to imagine the effect of new combinations of actions and thus create new counterfactual trajectories. By reverse engineering the underlying causal system directly from visual inputs and actions, we can then provide a potential first step towards AI systems that reason about the world causally without supervision. In this talk I will give a high-level overview of a few recent CRL methods in this exciting setting, and I will try to discuss a few high-level ideas of why I think this is also interesting for the (AI) verification crowd, e.g., by providing a principled and theoretically grounded way to extract meaningful concepts from unstructured data that could be then used for safety specifications.

ABSTRACT. The integration of constraint programming (CP) together with machine learning (ML) has emerged as a promising direction for tackling complex decision-making and combinatorial optimization problems. While CP offers expressive modeling capabilities and formal guarantees, ML provides adaptive methods for learning from data and generalizing across instances. This survey presents a comprehensive overview of recent advances in combining CP and ML. We first show how ML has been used to improve the CP toolbox, both in modeling and in the efficiency of solving. Then, we examine how CP can support ML, particularly in providing structure, guarantees, and symbolic reasoning capabilities. Finally, we identify key open challenges inherent to such hybrid approaches and outline promising directions for future research. This survey provides a first conceptual and structured review of recent advancements in this emerging field, aiming to serve as a resource for practitioners and researchers in both the CP and ML communities. To keep the progress up to date, a curated list of references is hosted on an accompanying repository (https://github.com/corail-research/CPML-paper-list) and is open to community contributions. https://doi.org/10.1613/jair.1.19533

ABSTRACT. Formal verification of arithmetic circuits remains a challenging problem at the intersection of SAT solving, SMT, and computer algebra. While SAT-based techniques have achieved remarkable success across many verification domains, arithmetic hardware continues to pose significant challenges. One of the most effective approaches in this setting relies on algebraic reasoning: a circuit, represented as an and-inverter graph, is encoded as a system of polynomials that induces a Gröbner basis, and correctness is established by reducing a polynomial specification with respect to this basis. In the first part of this talk, I will provide an overview of arithmetic circuit verification and discuss how SAT solving and computer algebra can be combined to discover structural information and enabling simplifications that are difficult to obtain through purely algebraic methods. In the second part, I will present a recent approach that addresses one of the main bottlenecks of algebraic verification: the monomial blow-up that occurs during specification rewriting. Rather than focusing computational effort on rewriting the specification, we rewrite the Gröbner basis itself to expose useful linear relations using algebraic guesses and SAT-based proofs. The resulting approach significantly simplifies the reduction process and improves the scalability of arithmetic circuit verification.

ABSTRACT. We introduce a theory of nested datatypes. The theory is obtained by restricting the naive combination of datatypes and arrays, so as to prevent non-standard models from emerging. A reduction-based decision procedure for the theory is given. Finally, we describe an implementation of the procedure, as well as an evaluation over both real-world and crafted benchmarks.

ABSTRACT. The Functional Machine Calculus (FMC) is a new foundational model of computation that seamlessly integrates higher-order functions (the lambda-calculus) with effectful imperative computation. Previous approaches to this problem have made use of heavy mathematical machinery, such as monads, monad transformers, Lawvere theories, and premonoidal categories. However, even in the monadic approach, standard effects such as store, input/output, and exceptions are all constructed from simple primitives: products, coproducts, and function spaces; or in other words, standard intuitionistic logic. This opens up a fundamental question: are effects inherently complex, or is there a simple underlying model waiting to be exposed? The FMC is an attempt at the latter, via the approach of structural proof theory, essentially asking the question: what is a good syntax for the phenomena we observe? The answer is a minimal extension of the lambda-calculus, preserving confluent reduction and a type system within intuitionistic logic, that nevertheless allows the embedding of various calculi, effects, and other constructions: the call-by-value lambda-calculus and call-by-push-value; higher-order store, input/output, and probabilistic choice; and sequencing, constants, conditionals, exceptions, and loops. In this tutorial, after a brief overview of the problem and some past solutions, I will introduce the FMC in stages, along with its main features: a small-step operational semantics in a simple stack machine; a natural big-step operational semantics; a confluent reduction relation; and a system of simple types.

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. Missing Values (MVs) in databases (DBs) are problematic for at least two data quality dimensions: completeness and consistency. Starting from an “observed” DB D* that exhibits MVs on which we would like to do query answering (QA), and assuming we have additional stochastic knowledge about the Missingness Mechanisms at play (that is, how and when MVs occur, as introduced by Donald Rubin), we represent D* as Probabilistic DB. We show how we can (and if we can easily) obtain from the latter a “best” MV-free possible DB D on top of which one can do QA. This is joint research with Farouk Toumani.

ABSTRACT. This is a tale in two parts. The first offers a reappraisal of the history and accomplishments of mechanized metatheory, from the first LFM workshop to the age of AI. We will examine the influence, if any, of benchmarks on our research area (remember POPLmark?), and ask whether there is still work left to do before, as the old Gauls used to fear, the sky falls on mechanized metatheory. The second part proceeds from the old Gaulish premise that tomorrow never comes. We turn to recent developments in the encoding of substructural systems: from the rediscovery of the unusual effectiveness of Crary’s “linear” predicate, to work in progress on a general Rocq library inspired by adjoint logic.

ABSTRACT. We introduce a new type of proof formalism for multiagent modal epistemic logics with S5-type modalities, viewed here as a logic of multiagent epistemic reasoning in distributed systems. We use this formalism to give a constructive proof that multiagent epistemic logic S5 enjoys a strong form of Craig interpolation property with respect to both propositional variables and agents, the latter in the form of agent-indexed knowledge modalities, a fact that has previously been proven using semantic methods. Our new proof formalism uses cross-word sequents that combine the features of hypersequents to represent individual S5 modalities—equivalence classes of individual agents—with nested sequents to represent the tree structure for alternating agent modalities—intersecting equivalence classes of distinct individual agents. The resulting calculus is sound and cut-free complete, allowing for strongly terminating proof search, and yields decidability and the finite model property for multiagent epistemic logic S5. No strongly terminating nested sequent calculus for S5 has been provided so far, and combining the structural features of hypersequents and nested sequents seems to be necessary to obtain computationally effective interpolation for agents rather than merely propositional variables. We further obtain Lyndon interpolation for propositional variables, which goes beyond existing semantic proofs of agent interpolation for multi agent epistemic logic S5. The talk is based on joint work with Wesley Fussner and Roman Kuznets.

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. Striking advances in machine learning are transforming how we build sequential decision-making systems---from conversational agents and logistics planners to robots, and more generally to computer programs that automate a myriad of everyday tasks. The synthesis of decision-making systems from data presents fundamental challenges to how we effectively integrate and leverage human know-how, reflect human norms and preferences, adhere to safety and regulatory constraints, and how we build systems that are taskable by and understandable to the humans they interact with. In this talk, I’ll discuss how language---both formal and natural language—provides a signal-symbol nexus for building human-compatible AI sequential decision-making systems. Not only does language provide an expressive and concise vehicle for communication, but I’ll show that exploiting the compositional syntax and semantics of language can greatly improve the efficiency of learning.

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. Rewriting induction is a form of inductive theorem proving to show that two terms in a term rewriting system compute the same value. This is a basic, easily understandable proof system -- for term rewriting systems. But what if we want to use it on functional programs? We can deal with in-built data structures like integers, but once we encounter higher-order variables -- a staple in any functional language -- new questions arise. Questions such as "what does equivalence even mean?" and "can I analyse these two tiny functions without knowing the entire program around it?" and "okay, but does this ever work for actually practical questions?". In this talk, I will discuss some possible answers to these questions, and show how we can use rewriting induction in general to analyse simple functional programs.

ABSTRACT. Contextual equivalence is the standard notion of program equivalence. A key theorem is that contextual equivalence is an equational theory. Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does not induce an equational theory, for an apparently essential reason: cost is not invariant under reduction. In the paradigmatic case of the untyped 𝝺-calculus, the talk will introduce _interaction equivalence_ (recent work published in POPL 2025). Inspired by game semantics, we observe the number of interaction steps between terms and contexts but---crucially---ignore their internal steps. We prove that interaction equivalence is an equational theory and characterize it as ℬ, the well-known theory induced by Böhm tree equality. It is the first observational characterization of ℬ obtained without enriching the discriminating power of contexts with extra features such as non-determinism.

ABSTRACT. Constructive mathematics is often guided by the slogan that proofs are programs. But this immediately raises a question: what kind of programs? While constructive foundations are traditionally interpreted through pure computation, many mathematical principles become more natural, more informative, or even newly valid when the underlying programs are allowed to use computational effects such as state, non-deterministic or probabalistic computation, etc. In this talk, I will explain how modalities provide a principled way to control such effects inside type theory. Rather than treating effects as external impurities, modalities act as an observation policy: they determine which computational capabilities are exposed to the logic and which remain hidden. Changing the modalities therefore changes the constructive world we obtain. Through examples involving Continuity, Choice, and variants of Markov’s principle, I will show how this perspective gives a systematic way to study how the landscape of constructive mathematics shifts when programs are allowed to compute with effects.

ABSTRACT. We will showcase how fixed point theory enables reasoning about probabilistic programs with loops. We will first give a recap on weakest preexpectations and thereafter see fixed point techniques that enable reasoning about loops. We will also showcase a new fixed point theorem and discuss possible applications in (probabilistic) program reasoning.

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. Constraint satisfaction problems (CSPs) provide a common modelling language for many application domains. In a CSP, the input is a collection of constraints imposed on a common set of variables, and the goal is to assign values to the variables so that all constraints are satisfied. For example, in reasoning applications, checking the consistency of available data can often be formulated as a CSP. In practice, however, constraint systems are often inconsistent because of noisy data, modelling errors, faulty measurements, conflicting requirements, or other imperfections. This motivates the MinCSP problem: given a CSP instance and a budget k, can we make the instance consistent by deleting at most k constraints? In this talk, I will discuss the complexity of solving almost-satisfiable CSPs, focusing on the parameterized complexity of MinCSPs with respect to the deletion budget k. I will survey dichotomy results, algorithmic techniques, and lower bounds, with applications to problems in spatial and temporal reasoning.

ABSTRACT. I generalize acyclic deterministic structural causal models to the nondeterministic case and argue that this offers an improved semantics for counterfactuals. The standard, deterministic, semantics developed by Halpern (and based on the initial proposal of Galles & Pearl) assumes that for each assignment of values to parent variables there is a unique assignment to their child variable, and it assumes that the actual world (an assignment of values to all variables of a model) specifies a unique counterfactual world for each intervention. Both assumptions are unrealistic, and therefore I drop both of them in my proposal. I do so by allowing multi-valued functions in the structural equations. In addition, I adjust the semantics so that the solutions to the equations that obtained in the actual world are preserved in any counterfactual world. I provide a sound and complete axiomatization of the resulting logic and compare it to the standard one by Halpern and to more recent proposals that are closer to mine. Finally, I extend these models to the probabilistic case and show that they open up the way to identifying counterfactuals even in Causal Bayesian Networks.

ABSTRACT. Many important functional and security properties—including non-interference, determinism, and generalized non-interference (GNI)—are hyperproperties, i.e., properties relating multiple executions of a program. Existing separation logics allow one to reason about specific classes of hyperproperties, e.g., ∀∀-hyperproperties such as non-interference and ∃∃-properties such as non-determinism. However, they do not support quantifier alternation, which is for instance needed to express GNI. The only existing logic that can reason about such properties is Hyper Hoare Logic, but it does not support heap-manipulating programs and, thus, is not applicable to common imperative programs. This paper introduces Hyper Separation Logic (HSL), the first program logic that supports modular reasoning about hyperproperties with arbitrary quantifier alternation over programs that manipulate the heap. HSL generalizes Hyper Hoare Logic with a novel hyper separating conjunction that lifts the standard separating conjunction to sets of states, enabling a generalized frame rule for hyperproperties. We prove HSL sound in Isabelle/HOL and demonstrate its expressiveness for hyperproperties that lie beyond the reach of existing separation logics.

ABSTRACT. Heisenbugs—a pun on the name of Werner Heisenberg—are bugs that alter their behavior or disappear when attempts are made to find and analyze them. Such bugs occur in a range of contexts including elusive concurrency bugs as well as unintended system alterations during debugging, and can be caused by various sources of nondeterminism on different system levels. We frame Heisenbugs and their causes as two- safety hyperproperties, thus providing formal foundations for rigorously reasoning about causes of Heisenbugs, and making this challenging class of bugs amenable to an arsenal of existing tools and techniques.

ABSTRACT. Generalized planning aims to find policies that solve large classes of symbolic planning problems. State abstraction plays a crucial role for generalization---mapping numerous states to a single abstract representation allows for omitting unnecessary details and finding policies that generalize to arbitrary instances within the same problem class. In this paper, we describe a state abstraction technique based on classical methods from first-order reasoning: Skolemization, unification, and regression. We use Skolemization to characterize groups of similar objects through common properties, including relational interdependencies. Unification specializes terms as much as necessary, where the most general unifier provides the most general action that achieves a subgoal, and regression determines under which condition this action leads to the goal. Together, these techniques enable a form of dynamic abstraction and refinement, allowing for the synthesis of general policies that are provably correct on all instances, while outperforming comparable methods both in terms of expressivity and efficiency.

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. 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. 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. 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. 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. 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. 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. 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. Abstraction is widely used in reasoning about action, for instance to facilitate planning or to provide explanations of agent behavior. In this paper, we present an incremental method to synthesize an abstract basic action theory (BAT) in the situation calculus that suppresses uninteresting details from a concrete BAT based on specifications provided by a knowledge engineer. The engineer can introduce abstract actions that are implemented by/mapped into Golog programs over the low-level theory and drop some low-level actions from the abstract BAT. She can also perform state abstraction by introducing high-level fluents that are mapped to low-level state formulas and drop some low-level fluents from the abstract BAT. The method allows the engineer to synthesize the abstract BAT step-by-step, providing the mapping along the way. The abstraction steps are validated to ensure that the resulting high-level BAT is guaranteed to be a sound and/or complete abstraction of the original low-level BAT. Abstraction steps that would fail to yield a sound/complete abstraction are rejected with an explanation for the failure, which guides the engineer towards a solution. Regression and SMT reasoning are used to automatically generate the axiomatization of the new abstract actions and fluents.

ABSTRACT. We present planned work on using abstraction to support the presentation of argumentative reasoning in computational argumentation. Building on our previous symbolic methods for abstracting potentially complex argumentation frameworks, we aim to extend the approach with a machine learning component. In this setting, the latter component determines the parts of the framework that are relevant based on user-input, while symbolic AI ensures that the reasoning presented remains sound at every level of abstraction.

ABSTRACT. Abstraction is a key problem-solving technique in knowledge representation and a common representational operation allowing complex parts to be treated as simpler wholes. In combination with association (co-activation or linking via a typed relationship, as in a subject-verb-object triple), abstraction is one of the central operations cognitive agents use to build complex concepts and statements. We refer to the compositional operation which supports abstraction as "containment", arguing that it can be underprioritised in knowledge representation systems. We propose the association-containment approach: that the operations of containment and association, by which nodes may contain other knowledge graphs and may be employed as a triple's subject, object, or link, give significant representational power. We show that diverse information formats, including sentences, can be effectively represented as association-containment graphs. We apply this approach to converting dependency parse trees into association-containment form. We describe simple transformation rules which can be repeatedly applied to progressively convert dependency parse trees. These results demonstrate the flexibility of the association-containment approach and suggest its utility for knowledge representation.

ABSTRACT. Knowledge base embeddings are widely applied, used for instance to improve link prediction tasks on knowledge graphs by exploiting the geometric regularities occurring during learning.. Techniques where ontological concepts are interpreted as boxes have shown to be particularly useful in this context, as they are both suitably expressive and of low computational cost allowing practical implementations. However, in order to use those regularities for learning reliably, it is necessary to determine and understand the possible biases in the approach: how do we distinguish what is learned due to regularities in the data from what is simply based on the representational limitations of the embedding? In this paper, we establish that there are some severe limitations in expressivity when modeling description logic ontologies with box embeddings in intended target languages such as ELO. We illustrate that, under some weak assumptions, box semantics always satisfy Helly's Property, and is thus too weak to semantically capture ELO in an adequate way. We then characterize how so-called Helly-satisfiable ELO ontologies can be determined and discuss other restrictions of representability arising from Helly's Property, namely the restricted faithfulness of the embeddings.

ABSTRACT. In a Curry-Howard-Lambek correspondence perspective, proofs are considered up to computational equivalence: βη-equivalence, cut-elimination and axiom-expansion, categorical equality, etc. In intuitionistic logic, η-long β-normal forms of the λ-calculus provide canonical representatives of the equivalence classes. In constructive classical logic, normal forms of the λµ-calculus are not canonical anymore but proof nets provide canonical representatives. By navigating through various (non-polarized) fragments of linear logic, we show that proof nets often reach their limits with respect to canonicity. This forces us to reconsider the equivalence of proofs up to rule permutations as a more robust and more versatile tool for the study of the computational identity of proofs in large fragments.

ABSTRACT. We introduce an illfounded sequent calculus for the constructive µ-calculus, the logic constructed by adding least and greatest fixed points to constructive modal logic. In addition to providing the Kripke-style and game semantics from the literature, we adapt a recent cut elimination argument by Curzi and Leigh, and based on Tait's and Girard's reducibility candidates for this logic. With this, we contribute to a general cut elimination procedure for illfounded proof systems by showcasing this proof method on a logic with modalities and without interdefinability between its connectives.

ABSTRACT. The modal μ-calculus μML is the logic obtained by adding least and greatest fixed point quantifiers to modal logic. It subsumes many temporal and dynamic logics such as PDL, LTL, CTL and CTL*. It is a classical logic, but intuitionistic variants have recently been proposed. In this talk, we present an ongoing project on formalising a variant of the modal μ-calculus inside Agda, a proof assistant based on dependent type theory. We use the machinery of indexed containers to handle the fixed points. The result is a proof-relevant, constructive Kripke semantics, where the semantics of a formula P assigns to a world w a "type of witnesses" that P holds at w. Currently, we have a semantics for the strictly positive fragment of μML (i.e., the fragment without negation and implication); adding implication is still a work in progress, but we believe this can be accomplished using the Cartesian closed structure of the category of containers. The next step is to develop a proof theory for this semantics.

ABSTRACT. Hyperproperties, properties that relate sets of execution traces rather than a single one, are needed to express information-flow security policies like noninterference, consistency criteria like linearizability, robustness in cyber-physical systems, and diagnosability, none of which can be captured by standard trace logics. Since HyperLTL and HyperCTL* equipped LTL and CTL* with explicit, simultaneous quantification over traces, the area has grown into a small zoo of logics, semantics, and verification techniques. In this talk I will take a chronological tour of that landscape, starting from the original synchronous hyperlogics and their automata-based and reduction-based model-checking algorithms, then follow two threads: time, including discrete and pointwise timed semantics (HyperMTL) and finite-trace semantics with past operators; and asynchrony, including traces that stutter or advance along independent contexts or trajectories (HyperLTL_S, HyperLTL_C, A-HLTL), undecidability in general but with decidable fragments, and recent attempts to unify these extensions into a single framework. I will also look at non-standard semantics, from multimodels to what these logics express when evaluated for a single trace model, where some asynchronous fragments turn out to characterize non-regular properties. From the algorithmic side, we move from automata constructions and self-composition reductions to bounded model checking via QBF and SAT, with an eye on the elusive loop conditions; and from static verification to gray-box runtime verification. I will close the talk by looking past finite-state systems, e.g. population protocols, with some thoughts on open problems.

ABSTRACT. Program equivalence is a notoriously undecidable problem, consequently, all approaches to determining whether two programs are equivalent are either imprecise or labor-intensive. In practical applications, developers often rely on proxy measures, such as the syntactic similarity of programs. In this paper, we formalize what it means for a similarity measure to be semantically descriptive and provide a framework for ranking measures based on their ability to differentiate between equivalent and non-equivalent program pairs. We refer to this metric as the average semantic loss of the similarity measure. We evaluate 17 established similarity measures, including those based on edit distance, compression, and vector embeddings. Using a subset of 0.45 million program pairs from the IBM ProjectCodeNet benchmark, we show that our semantic loss score replicates previous findings based on classifier performance. Finally, using this score, we demonstrate that compression-based measures outperform state-of-the-art vector-embedding-based approaches, such as CodeBERT and GraphCodeBERT, on unformatted code, but lag behind when the code is formatted or compiled and then decompiled. This indicates that these approaches are sensitive to the varying formatting of code.

ABSTRACT. Software development is a process of gradually modifying program behavior; thus, most programs are revisions of other programs. Developers informally reason about a revision in terms of which behaviors are removed, added, or preserved. We formalize these notions by providing a collecting semantics for program revisions, parameterized by a user-specified state correspondence, which classifies reachable states as ``removed'', ``added'', or ``related''. Intuitively, reasoning about added and removed states requires showing that some reachable state in one program has no corresponding state in the other. Therefore, proving safety properties over removed and added states requires an underapproximation of one program and an overapproximation of the other. Existing relational Hoare-style program logics provide limited support for reasoning about this class of properties. To address this gap, we present a system for proving safety properties of ``added'', ``removed'', and ``related'' states that combines over- and underapproximating program logics.

ABSTRACT. We flesh out that *equivalence checking* constitutes a form of backward-complete *abstract interpretation* on pairs of programs. The first part of the paper illustrates this framing for trace semantics on finite-state systems. We then extend the approach to uniformly handle simulation, failure equivalence, and ready simulation in a single abstract interpretation.

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 Model Constructing Satisfiability (MCSat) approach has shown strong performance in solving complex SMT problems, in particular in algebraic SMT theories such as non-linear integer and real arithmetic. In this paper we revisit the theory-independent MCSat framework as a proof system to provide a modern perspective that refines the original formulation of MCSat. By closely formalizing the implementation of MCSat within the Yices2 SMT solver, we incorporate design decisions that diverge from those in the seminal MCSat paper and thereby capture the current state-of-the-art in MCSat-based SMT reasoning. We present a general, theory-agnostic rule scheme for MCSat and instantiate it for several theories, including propositional logic, non-linear real arithmetic, and uninterpreted functions. We provide several detailed examples to illustrate the applicability of the presented calculus.

ABSTRACT. We propose a framework for solving quantifier-free formulas from (undecidable) extensions of non-linear real arithmetic (NRA) with transcendental functions, such as exponential and trigonometric ones. The framework extends the Model Constructive Satisfiability calculus (MCSAT), and leverages procedures for NRA and methods from real analysis. At its core, our procedure abstracts the input formula to NRA, and lets MCSAT and an NRA plugin incrementally builds a partial model of the abstracted formula. A Transcendental Real Arithmetic plugin, acting as an intermediary between MCSAT and the NRA plugin, ensures the consistency of the partial model and is responsible for refining the abstracted formula. We implemented our procedure in the Yices2 SMT solver for the sine and exponential functions, and conducted an extensive empirical evaluation that shows that our implementation outperforms state-of-the-art solvers on both SAT and UNSAT instances.

ABSTRACT. Satisfiability modulo non-linear real arithmetic is about checking Boolean combinations of polynomial constraints. The non-uniform CAD (NuCAD) and cylindrical algebraic covering (CAlC) algorithms are variants of the complete cylindrical algebraic decomposition (CAD) algorithm which reduce effort by transferring the exploration-guided technique from SAT solving, so that the trace of these algorithms can be described as a search tree. The modification in this paper alters the order in which the search tree is explored, deferring the exploration of branches with expensive computations to potentially find an easier-to-compute solution. We adapt both the NuCAD and CAlC algorithms. In the experimental evaluation, NuCAD solves a significant number of previously unsolved instances, whereas CAlC does not benefit from the modification.

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. 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. 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. 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 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 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. 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. 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. PDL is a modal logic where modalities are indexed by programs which come equipped with operations, namely the * operation, which iterates a program an infinite number of times. We explore an intuitionistic variant of PDL and propose a cut-free proof system making use of non-wellfounded proofs.

ABSTRACT. We introduce the semantically-defined constructive logics with master modality CK* and WK*, extending the basic constructive modal logic CK and the Wijesekera-style logic WK obtained by imposing infallibility. Using translations between our logics and fragments of PDL, we show that both CK* and WK* are EXPTIME-complete and admit an exponential-size finite model property. In particular, for their diamond-free fragment, also studied by Afshari et al. and Celani, we establish EXPTIME-completeness, thereby settling the conjecture of Afshari et al. As an application, we embed CS4 and WS4 into the master-modality logics, showing that their validity problems are in EXPTIME.

ABSTRACT. Constructing reasonable proof systems in the presence of generalized quantifiers is challenging, in part due to the general lack of sound introduction/elimination rules for such quantifiers. We propose an alternative approach to the proof theory of generalized quantifiers, using deep inference methods to circumvent this problem. We show that the quantifiers suitable for a deep inference treatment are specifically the class of monotone quantifiers, and subsequently present a generic methodology for designing deep inference proof systems for logics with monotone quantifiers.

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. MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Contextual Modal MetaML, \textit{the first metaprogramming language that supports storing and running open code under a strong type safety guarantee}. The type system utilises contextual modal types to track and reason about free variables in code explicitly. A crucial concern in metaprogramming-based program optimisations is whether the optimised program preserves the meaning of the original program. Addressing this question requires a notion of program equivalence and techniques to reason about it. In this paper, we provide a semantic model that captures contextual equivalence for Contextual MetaML, establishing \textit{the first full abstraction result for an imperative MetaML-style language}. Our model is based on traces derived via operational game semantics, where the meaning of a program is modelled by its possible interactions with the environment. Modal types can be introduced as box names and queried by running.

ABSTRACT. \section*{Background on Effectful Contextual Modal Type Theory} In 2021, N. Zyuzin and A. Nanevski proposed a calculus for the theory of algebraic effects, where effectful signature is treated as a \emph{variable context}, and effects are tracked via \emph{indexed modalities} inherited from Contextual Modal Type Theory (CMTT). In the resulting calculus, named ECMTT (Effectful Contextual Modal Type Theory), effect information is encoded in the \emph{modal type} $\boxt{\Psi}{A}$, classifying computations of type $A$ that may invoke exactly the operations declared in the algebraic theory $\Psi$. \paragraph{On Contextual Modal Type Theory.} CMTT is a contextual variant of constructive modal S4. Its typing judgments are of the form $\Delta;\Gamma \vdash e : A$, where $\Gamma$ holds ordinary \emph{value variables} $x:A$ (intuitively, making the assumption that $A$ is \emph{contingently} true at the given world) and $\Delta$ holds \emph{modal variables} $u \mathrel{::} A[\Psi]$, annotated with a context $\Psi$ of variables saying that $A$ is \emph{valid relative to} $\Psi$ (i.e.,~true in every world in which every $B$ in $\Psi$ is true). Two of the main rules of CMTT are the following. \begin{center} \AXC{$\Delta; \Psi \vdash e: A$} \LL{$\Box I$} \UIC{$\Delta;\Gamma \vdash \mathrm{box }\ \Psi.e: [\Psi]A$} \DP \quad \AXC{$\Delta;\Gamma \vdash e_1: [\Psi] A$} \AXC{$\Delta, u::A[\Psi]; \Gamma \vdash e_2: B$} \RL{$\Box E$} \BIC{$\Delta; \Gamma \vdash \mathrm{let\ box} \ u = e_1\ \mathrm{in}\ e_2: B$} \DP \end{center} The \emph{introduction form} $\boxe{\Psi}{e}$ binds all variables of $\Psi$ in the scope of $e$, simultaneously removing the outside context $\Gamma$ from $e$'s premise (reading the rule $\square I$ from the bottom up). The \emph{elimination form} $\mathbf{let}\;\mathbf{box}\;u = e_1\;\mathbf{in}\;e_2$ (rule $\square E$) binds the unboxed body of $e_1$ to the modal variable $u$; occurrences of $u$ in $e_2$ must be guarded by \emph{explicit substitutions} $u\langle\sigma\rangle$ that supply definitions for the variables in $\Psi$. ECMTT adopts and readapts the aforementioned concepts: contexts $\Psi$ become algebraic theories and explicit substitutions become effect handlers. \paragraph{Accomodating algebraic effects.} Consider, as an example, the operation $get$ that reads the current state and the operation $set$ that updates it. An algebraic theory, e.g.\ the state theory \[St \triangleq \mathit{get} \div \mathit{unit} \Rightarrow \mathit{int},\; \mathit{set} \div \mathit{int} \Rightarrow \mathit{unit},\] is treated as a variable context locally bound by the $\mathbf{box}$ constructor. The term \[\mathit{incr} \triangleq \boxe{St}{x \leftarrow \mathit{get}();\; \_ \leftarrow \mathit{set}(x+1);\; \mathbf{ret}\;x}\] has type $\boxt{St}{\mathit{int}}$, and the boxed term is a pure (i.e.~not effectful) expression. As mentioned above, context reachability in CMTT is witnessed by \emph{explicit substitutions}; in ECMTT it is witnessed by \emph{effect handlers}. Consider the following \[handlerSt \triangleq (get(x,k,z) \rightarrow \mathrm{cont}\ k\ z\ z,\ set(x,k,z) \rightarrow \mathrm{cont}\ k\ ()\ x,\ return(x,z) \rightarrow \textbf{ret}(x,y)).\] A handler such as $\mathit{handlerSt}$ specifies how each operation of $St$ is interpreted, thereby transforming a computation in theory $St$ into one in the empty theory. %The handler is used through the elimination form %$\mathbf{let}\;\mathbf{box}\;u = \mathit{incr}\;\mathbf{in}\;\mathbf{handle}\;u\;\mathit{handlerSt}\;0$, %which binds $u$ to the unboxed body of $\mathit{incr}$ and runs it under the handler with initial %state~$0$. \iffalse The operational semantics of ECMTT is determined solely by $\beta$-reduction (plus $\eta$-expansion for local completeness), in direct analogy with other logic-based calculi. This is in sharp contrast to monad-based designs, where the bound computation executes eagerly. The paper also situates ECMTT as a first step towards a Curry--Howard correspondence for algebraic effects and modal logic, anticipating transfers of results (Kripke semantics, normalisation by evaluation, dependent types, etc.) between the two fields. \fi ECMTT uses four variable judgments ($x:A$, $u::A[\Psi]$, operations $\mathrm{op}\div A\Rightarrow B$, continuation variables $k\sim\!\!\!:\,A\stackrel{S}{\Rightarrow}B$) and five term judgments (expressions, computations, statements, handlers, handling sequences). By design, the operational semantics of ECMTT is determined solely by $\beta$-reduction, as customary in other logic-based calculi (but not in other systems for algebraic effects). The new syntactic category of (effectful) \emph{computations} sequences bindings of algebraic operations and continuation calls in monadic-style notation $x \leftarrow s;\;c$, and terminates with $\mathbf{ret}\;e$. The category of \emph{expressions} remains purely functional. In contrast with the CMTT setting, the modal type $\boxt{\Psi}{A}$ now classifies computations, not expressions. The context $\Gamma$ (formerly holding value variables) now holds \emph{algebraic operations} $\mathit{op} \div A \Rightarrow B$ and \emph{continuation variables} $k \sim\!\!\!:\, A \stackrel{S}{\Rightarrow} B$. The context $\Psi$ (used in $\boxt{\Psi}{A}$) ranges only over operation-only subsets (algebraic theories). Value variables $x:A$ migrate to $\Delta$, reflecting the fact that values are computations in the empty theory. This allows values to survive boxing, enabling parametric computations such as $\mathit{incr}_n \triangleq \lambda n:\mathit{int}.\;\boxe{St}{x \leftarrow \mathit{get}();\;y \leftarrow \mathit{set}(x+n);\;\mathbf{ret}\;x}$. \section*{In search for a logical interpretation of Algebraic Effects} In the case of the constructive modal logic S4, we already have a relational Kripke-style, algebraic, and categorical semantics; all of these are well-known and have been successfully used to study the metaproperties of the logic for which they are complete. At present, however, there is no known semantic characterization of the logic defined by the ECMTT calculus, nor is there a known Hilbert-style axiomatization of it. Our task is to find such a characterization to identify for the first time a correspondence, in the style of Curry-Howard, targeting algebraic effects.\footnote{As far as the authors are aware, this would count as the first instance of a Curry-Howard-style correspondence where the computational system is developed before its logical interpretation.} The following is a list of relevant, non-interderivable theorems of ECMTT, which currently constitute an initial attempt at axiomatization within a Hilbert-style proof system. \begin{enumerate} \item \label{item1} $\vdash [\Psi]A \wedge [\Psi]B \rightarrow [\Psi](A \wedge B)$, for every $\Psi$; \item \label{item2} $\vdash A \rightarrow [\Psi]A$, for every $\Psi$; \item \label{item3} $\vdash [\Psi][\Psi]A \rightarrow [\Psi]A$, for every $\Psi$; \item \label{item4} $\vdash [\Psi]A \rightarrow [\Psi']A$, given $\Psi \subseteq \Psi'$; \item \label{item5} $\vdash A \rightarrow [\Psi]B$, whenever $\mathrm{op}\div A\Rightarrow B$ is in $\Psi$; \item \label{item6} $\vdash [\Psi]C \rightarrow((A_1\rightarrow B_1) \rightarrow\cdots\rightarrow(A_n \rightarrow B_n) \rightarrow \Box C)$, where $\Psi = \{\mathrm{op}_i\div A_i \Rightarrow B_i\}_{i=1}^{n}$. \end{enumerate} The first three theorems listed above correspond exactly to a multimodal version of propositional Lax logic. It is known that multimodal propositional Lax logic is sound and complete with respect to multirelational CL-Kripke models. The latter are defined as a tuple $(W, \leq, V, \{R_\Psi \mid \Psi \text{ is an algebraic signature}\}, \models)$, where $W$ is a non-empty set of possible worlds partially ordered by $\leq$; $V$ is a map which assigns to every propositional variable $p$ an upset $V(p) \subseteq W$; each $R_\Psi$ is a partial order on $W$; finally $\models$ is a relation between worlds and formulae recursively defined as in the intuitionistic case, where \[w \models [\Psi]A \text{ iff forall } w' \geq w \text{ there exists } w'' \text{ such that } w'R_\Psi w'' \text{ and } w'' \models A.\] We also require every $R_\Psi$ to be hereditary, namely if $w \models A$ and $wR_\Psi v$, then $v \models A$. It can be shown that the validity of Theorems \ref{item4}, \ref{item5}, and \ref{item6}, in the context of the multirelational CL-Kripke models defined above, is equivalent to the following conditions imposed on the accessibility relations $R_\Psi$ and the valuation function $V$. \begin{enumerate} \addtocounter{enumi}{3} \item $\vdash R_\Psi \subseteq R_{\Psi'}$, whenever $\Psi \subseteq \Psi'$; \item whenever $\mathrm{op} \div A \Rightarrow B \in \Psi$ and $w \models A$, there exists $v \in W$ such that $wR_\Psi v$ and $v \models B$; \item whenever $w \models [\Psi]C$ and $w \models A_i \rightarrow B_i$ for every $\mathrm{op} \div A_i \Rightarrow B_i \in \Psi$, there exists $v \in W$ such that $wR_\emptyset v$ and $v \models C$. \end{enumerate} Intuitively, Theorem \ref{item4} states that whenever an algebraic signature is contained within another, it is possible to use every operation present in the first one within the second. Theorem \ref{item5}, on the other hand, states that it is possible to perform $\mathrm{op}\div A \Rightarrow B$ (in the context of an appropriate algebraic signature $\Psi$ containing the aforementioned operation) whenever an input of type $A$ is available. Finally, Theorem \ref{item6} captures the concept of operation handling: every $\mathrm{op}\div A \Rightarrow B$ in $\Psi$ is handled via the corresponding function of type $A \rightarrow B$.

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. 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. 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. As modern software systems control more and more aspects of our everyday lives, they grow increasingly complex. Therefore, the goal of modern IT science does not only lie in the development of powerful and versatile systems, but also in providing comprehensive techniques to understand these systems. This motivates research on formal notion of cause-effect relations in operational models that enhance the understanding why properties hold or not, and which system components are mostly responsible for the satisfaction or violation of properties. The talk will present recent work on formal concepts of cause-effect reasoning in Markov chains and Markov decision processes. It will present formalizations of causality based on the probability-raising principle, essentially stating that causes raise the probabilities of their effects, and methods to solve related algorithmic questions such as checking cause-effect relationship for a given effect and a cause candidate and finding "good" causes for a given effect with respect to some quality criterion for causes.

ABSTRACT. Constraint satisfaction problems with few variables but large domains arise naturally in parameterized algorithms for graph-separation problems and, more broadly, in the study of MinCSPs over finite and temporal domains. As suggested by George Osipov’s morning talk, flow augmentation plays a central role in the tractability classifications for Boolean MinCSPs and for certain temporal MinCSPs, such as MinCSP(<, ≤) and MinCSP(=, ≠). At a high level, flow augmentation reduces these problems to CSP instances with a parameter-bounded number of variables but potentially unbounded domains. Tractability is then obtained by exploiting the particular structure of the resulting constraints. A natural graph-separation problem that remained elusive even after the application of flow augmentation is Directed Multicut with three terminal pairs. Given a digraph D, three ordered pairs of vertices (s_1,t_1), (s_2,t_2), (s_3,t_3), called terminal pairs, and a positive integer k, the task is to determine whether one can delete at most k arcs of D so that, in the resulting digraph, there is no directed path from s_i to t_i for any i in {1, 2, 3}. Directed Multicut has been known, for more than a decade, to be W[1]-hard when the input contains four terminal pairs. However, the parameterized complexity of the three-pair case remained open for a long time; we resolve it affirmatively by giving an FPT algorithm. In this talk, we will walk through the main ideas behind this algorithm. We will see how flow augmentation allows Directed Multicut to be modelled as a CSP with few variables and large domains, and how the resulting CSP can then be solved using a \emph{twin-width}-based win-win argument. More broadly, the talk illustrates how twin-width---a graph parameter introduced in 2020---can capture the structural complexity of constraints arising in bounded-variable CSPs over unbounded domains.

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. We address the satisfiability problem for quantified nonlinear integer arithmetic (NIA), which is undecidable even in the quantifier-free case. Our approach reduces NIA formulas to linear integer arithmetic (LIA) by replacing nonlinear terms with fresh existential variables---a process we call purification. The resulting LIA abstraction over-approximates the original problem and is iteratively refined by adding axioms that constrain the abstracted terms to respect their nonlinear semantics. Experimental evaluation on SMT-LIB benchmarks and randomly generated polynomial representation problems outperforms state-of-the-art solvers. In the case of representation problems, our prototype solves more than twice as many instances as the next-best solver (yicesQS).

ABSTRACT. Formal verification of cryptographic protocols in the computational model provides strong security guarantees but remains challenging to automate. The Computationally Complete Symbolic Attacker (CCSA) logic, implemented in the Squirrel proof assistant, provides computationally sound reasoning in a polymorphic higher-order logic whose validity is defined as overwhelming truth. Recently, we introduced an SMT-based tactic to automate a first-order fragment of that logic, but higher-order constructs and polymorphism were left unsupported. In this paper, we extend our approach to automate the full local logic of Squirrel. We implement this translation in Squirrel's SMT tactic and demonstrate its effectiveness on generic benchmarks and several case studies.

ABSTRACT. We introduce a dependently typed theory of floating-point arithmetic for SMT-LIB 3 in which exponent and significand widths are symbolic parameters. This enables reasoning about format-parametric properties that cannot be expressed in SMT-LIB 2. We implement MC-Hammer, an extension of Isabelle/HOL's Sledgehammer, which translates polymorphic floating-point terms into SMT-LIB 3 with dependent types. Using this infrastructure, we generate over 600 benchmark problems covering both fixed and symbolic sizes. Our work provides the first practical bridge between interactive theorem provers and SMT-LIB 3 for floating-point reasoning.

ABSTRACT. Proving non-trivial lower bounds on proof size in the classical sequent calculus remains a longstanding open problem in proof complexity. In this work, we revisit this problem through the lens of substructural and linear logics. By considering calculi that restrict contraction or weakening, we obtain systems in which derivations are subject to resource-sensitive constraints. Within these frameworks, we exhibit formulas that, while admitting short classical proofs, require substantially larger derivations. These results provide a proof-theoretic explanation of why classical systems are difficult to analyze: their efficiency stems from the interaction of structural rules, a feature that becomes visible only when examined against substructural baselines.

ABSTRACT. Once upon a time, there was a user who heard of an ontology that perfectly suited their needs. They found a way to open it and... Depending on what happens next, what follows may become either a fairy tale or a nightmare. In this talk, we will not only revisit some approaches to building abstractions over conceptual models and ontologies, but also explore the philosophical side of the story. What does it mean, from a logical point of view, to construct an abstraction? What role does abstraction play in the explanation process? Does it have explanatory power? What role does the user play, and why should we care about their goals? There is no promise of a happily ever after, but there may be a few clues to help you navigate your own journey.

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. Labelled Markov chains are commonly used to model systems with random behaviour. To mitigate the state-space explosion problem, behavioural equivalences such as probabilistic bisimilarity can be used to minimise the state space. In this talk, I will begin with an introduction to probabilistic bisimilarity and its associated behavioural pseudometric. I will then discuss a key limitation: probabilistic bisimilarity suffers from a lack of robustness under small perturbations of the transition probabilities. This can lead to unexpected changes in behaviour in practical applications where transition probabilities are often approximations derived from experimental data. There exist different approaches in the literature to address the sensitivity of probabilistic bisimilarity. I will also present our notion of robust probabilistic bisimilarity, which is designed to be stable under small changes in the model by ensuring the continuity of the associated probabilistic bisimilarity distance function. Finally, I will give an overview of our partition-refinement algorithm for computing robust probabilistic bisimilarity.

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. Motivated by applications of Craig interpolation in computer science, I will discuss some recent work pertaining to the Craig interpolation property (CIP) for various important decidable fragment of first-order logic, including guarded fragments, finite-variable fragments, and ordered fragments. Most of these fragments lack the CIP. We will discuss strategies that have been proposed to deal with this lack of CIP, as well as results that shed light on where, within the landscape of decidable fragment of first-order logic, one may find logics that enjoy CIP.

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. There are two main contenders for a grand unified theory of computer security: hyperproperties in the formal methods community, and the Real–Ideal paradigm (e.g., Universal Composability) in the cryptography community. I describe how they meet in the Viaduct compiler, which transforms high-level sequential programs to distributed, concurrent cryptographic realizations. Even though the source and target systems have very different properties, the Viaduct compiler transformation preserves the security promises of the original source program, because it robustly preserves all hyperproperties. The proof of Robust Hyperproperty Preservation is achieved by building a series of Real–Ideal simulations that transitively connect the source to the final target. This work points to a deep connection between these two contending perspectives, and suggests that Real–Ideal simulations are a powerful tool for security specification and provable enforcement.

ABSTRACT. Hyperproperties relate multiple executions of a program and capture essential correctness and security properties such as determinism, monotonicity, transitivity, reachability, and (generalized) non-interference. Existing program logics for hyperproperties typically reason about a fixed number of states, which limits the kinds of hyperproperties they can express and prove, and hinders the reuse of proofs across different formalisms. In this talk, I will present Hyper Hoare Logic (HHL), a generalization of Hoare logic whose assertions range over sets of states rather than individual states. This generalization enables uniform reasoning for a wide range of hyperproperties, including those beyond the reach of existing logics. Despite its expressiveness, HHL admits simple and intuitive inference rules that support key reasoning principles, such as composing different kinds of hyperproperties in the same proof or reasoning about loops where different executions perform different numbers of iterations. I will then show that HHL lends itself to automation through Hypra, an automated verifier that translates a program and its HHL specification into a Viper program, with each Viper execution representing a set of executions of the original program. Our evaluation on new and existing benchmarks shows that Hypra can automatically prove diverse hyperproperties efficiently and with minimal annotation overhead. Finally, I will turn to Hyper Separation Logic, a recent extension of HHL that brings modular reasoning about hyperproperties to heap-manipulating programs. Its key ingredient is a hyper separating conjunction that lifts the standard separating conjunction to sets of states, yielding a generalized frame rule for hyperproperties.

ABSTRACT. In this project, we explored Dafny's capabilities in proving program equivalence. We built EquiDafny, an equivalence checker on top of Dafny to generate equivalence proofs automatically, with no user assistance. Finally, we evaluated EquiDafny against program verifiers Dafny and Stainless.

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. By temporal resources we mean resources manipulated by programs whose usage is time-sensitive or time-critical, and which, while perhaps already physically available to a program, can be used or acted upon only after a certain amount of time has passed or some prescribed events have taken place (perhaps in some order). In this talk, I will discuss some ongoing work on using and combining graded effect systems, temporally aware algebraic effects and effect handlers, and graded modal types for specifying, controlling, and verifying how and when programs use their resources. In particular, I will discuss how our past work, which only tracked (the lower bounds on) the duration of program execution, naturally generalises to a setting where effect grades and resource grades can come from general, and not necessarily the same, ordered monoids. For instance, in this way the effect system part of the calculus can track fully detailed information using sets of traces of events or algebraic operation calls, while the modal resource-typing part can specify properties of resources in terms of durations of computations or in terms of (sequences of) only certain events.

ABSTRACT. So far, the verification of reactive systems against temporal hyperproperties has been mostly studied from the perspective of model-checking for finite-state systems (e.g., hardware). However, there is still a lack of interactive and deductive techniques to prove temporal hyperproperties of infinite-state systems (e.g., software). This presentation aims to give an introduction to recent works based on \emph{cyclic deductive proof system} for verifying temporal hyperproperties with the help of an interactive proof assistant. In particular, we will present HyCo, a framework for the interactive verification of $\forall^*\exists^*$-safety properties embedded in the Rocq proof assistant.

ABSTRACT. Information flow security ensures that the secret data manipulated by a program does not influence its observable output. In concurrent programs, operations on secret data may influence the execution time of a thread and, thereby, the interleaving between threads; such internal timing channels may affect the observable outcome of a program even if an attacker does not observe execution times. Existing verification techniques attempt to prove that secret data does not influence the relative timing of threads. However, these techniques are often restrictive (forbidding branching on secrets) and make strong assumptions about the execution platform (ignoring caching and other common features that affect execution time). In this talk, we will give an overview of CommCSL, a verification technique for secure information flow in concurrent programs that lifts these restrictions and does not make any assumptions about timing behavior. We will explain its key idea, which is to prove that all mutating operations performed on shared data commute, such that different thread interleavings do not influence its final value. Subsequently, we will describe some limitations of CommCSL in its current form and outline ideas on how they can be addressed.

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. This talk aims to explore the role of arbitrary objects in foundational projects based on abstractionist theories. The driving hypothesis of the talk is that mathematical objects implicitly defined by abstraction principles can be understood as arbitrary objects, as defined by Horsten’s Arbitrary Object Theory (AOT, cf. [9], [10]). To support this claim, we will develop a theory of arbitrary abstract objects (AAOT) by extending Horsten’s AOT ([10]) with a schematic abstraction principle (@𝜑= @𝜓↔𝐸𝑞.(𝜑,𝜓)). We will then prove that abstract terms denote arbitrary objects.

ABSTRACT. This paper aims to provide a framework that allows a systematic analysis of some open issues related to the notion of 'concept'. It has two main goals. The first is to offer a unified framework that can account for different conceptual representations (prototype theory, exemplar theory, knowledge view) - in other words for the multifaceted nature of concepts. Here the focus is on the structure conceptual representation have. The second is to develop a framework capable of capturing the continuity and evolution of concepts over time. To this end, the paper proposes treating concepts as forms of embodiment à la Kit Fine.

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. 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. Algorithmic meta-theorems establish broad tractability results of the form that every problem expressible in a given logic can be solved efficiently on graph classes with suitable structural properties. A central objective in this area is to identify the exact tractability boundaries for increasingly expressive logics and increasingly general graph classes. For first-order logic, we established that on graph classes closed under taking subgraphs, model checking is fixed-parameter tractable if and only if the class is nowhere dense [Grohe, Kreutzer, Siebertz, 2014]. More recently, attention has shifted to the substantially more challenging setting of graph classes closed under taking induced subgraphs, where the precise tractability frontier is still far from understood. At the same time, first-order logic has important expressive limitations, most notably its inability to capture connectivity. To overcome this, we introduced separator logic as a natural extension with significantly greater expressive power and many algorithmic applications [Schirrmacher, Vigny, Siebertz, 2022]. For classes closed under taking subgraphs, we proved that model checking for separator logic is fixed-parameter tractable precisely on classes excluding a fixed topological minor [Pilipczuk et al., 2022]. In this talk, I will survey these developments and present recent progress on algorithmic meta-theorems for expressive logics on structurally restricted graph classes [Mählmann et al., 2026+]. I will then discuss an application to the recently introduced framework of solution discovery [Fellows et al. 2023],  where the goal is not to compute a solution from scratch, but to transform a given initial configuration into a valid solution using as few modification steps as possible.

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. This work investigates proof-theoretic methods for handling Henkin quantifiers within first-order logic. While such quantifiers extend expressiveness beyond standard first-order logic and are naturally representable in second-order logic, their direct treatment poses challenges for analytic proof systems and unification-based reasoning. Building on sequent calculi that incorporate Henkin quantifiers while preserving desirable properties such as cut-elimination and completeness relative to corresponding second-order systems, we introduce tableau systems with unification, enabling effective proof search while maintaining soundness and completeness.

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. 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. Some security properties of cryptographic protocols cannot be expressed as trace properties. This is typically the case for privacy-related properties such as anonymity, or unlinkability. They are generally expressed in terms of an adversary's inability to distinguish two distinct scenarios, while actively interacting with the protocol. In symbolic models (following the initial work of Dolev and Yao) such indistinguishability properties can be naturally modeled using process equivalences in extensions of the pi calculus such as the applied pi calculus. We will illustrate how process equivalences can be used to model privacy properties. We provide complexity results for the underlying verification problem (when the number of sessions is bounded) and we will describe the decision procedure underlying the DeepSec verification tool.

ABSTRACT. We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs. Equivalence and similarity are two fundamental relational properties of probabilistic programs that are essential for their correctness both in implementation and in compilation. In this work, we present a new method for static equivalence and similarity refutation. Our method refutes equivalence and similarity by computing a function over program outputs whose expected value with respect to the output distributions of two programs is different. The function is computed simultaneously with an upper expectation supermartingale and a lower expectation submartingale for the two programs, which we show to together provide a sound and complete certificate for refuting equivalence and similarity. To the best of our knowledge, our method is the first approach to relational program analysis to offer the combination of the following desirable features: (1)~it is fully automated, (2)~it is applicable to infinite-state probabilistic programs, and (3)~it provides formal guarantees on the correctness of its results. We implement a prototype of our method and our experiments demonstrate the effectiveness of our method to refute equivalence and similarity for a number of examples collected from the literature.

ABSTRACT. Although techniques for the verification of neural networks (NNs) have seen significant progress in recent years, specifying meaningful properties remains non-trivial. One promising approach to the specification of neural networks are relational properties which do not specify the behavior of an NN in absolute terms, but impose constraints on related execution traces. We provide an overview of our recent advances in using differential verification in NN verification by leveraging the abstract domain of Zonotopes. This approach enables us to reason about changes in behavior locally, at the level of individual neurons of an NN. We discuss the fundamental ideas of our abstract domain and discuss current and future applications of the differential verification paradigm.

ABSTRACT. Modal type systems are a powerful tool for tracking properties in programming languages. They have long been used to track properties of computations, such as mobility, co-effects or erasability. In recent years, several authors have used them to track properties of values, such as stack location, linearity, purity or acyclicity. However, to support the latter applications, one needs to restrict modal type systems appropriately. In this abstract, we identify the value trick as a unifying principle connecting several approaches from the literature.

ABSTRACT. Fitch-style natural deduction for intuitionistic modal logics have found a variety of applications in computer science, notably in the design of modal type systems in programming languages. In this work, we propose a Beth-Kripke-Joyal-style cover semantics à la Goldblatt for Fitch-style modal natural deduction with the overarching motivation of 1) explaining the seemingly ad hoc proof rules in the Fitch-style approach and 2) implementing Normalisation by Evaluation for corresponding modal lambda calculi.

ABSTRACT. What the appropriate intuitionistic analogue of the normal modal logics should be, is question without a simple answer. In the intuitionistic setting, $\Box$ and $\Diamond$ are no longer defined as dual to each other and as a result, it is not so immediate as to what the correct rules for intuitionistic $\Box$ and $\Diamond$ should be. Most commonly, as in~\cite{degroot2025semanticalanalysisintuitionisticmodal,StrassbergerDasArisakaNestedSequentsForConstructiveModalLogics,simpson1994Thesis}, one finds Intuitionisic Modal Logics (IMLs) defined as taking any axiomatisation of IPL and adding the following five axioms and rule of inference: \vspace{-1.2cm} \begin{center} \[ \begin{array}{ccccc} k_1: & \Box(\varphi\to\psi) \to \Box\varphi \to \Box\psi & \qquad & k_3: & \Diamond\bot\to\bot \\ k_2: & \Box(\varphi\to\psi) \to \Diamond\varphi \to \Diamond\psi & \qquad & k_4: & \Diamond(\varphi\lor\psi)\to (\Diamond\varphi\lor\Diamond\psi) \end{array} \] \vspace{-0.5cm} \[ \begin{array}{cc} k_5: & (\Diamond\varphi\to\Box\psi)\to\Box(\varphi\to\psi) \end{array} \] \vspace{-0.5cm} \[ \infer[\text{Nec}]{\Gamma\vdash\Box\varphi}{\vdash\varphi} \] \end{center} possibly with additional axioms (such as intuitionistic variants of the T or 4 axioms). We call the logic with just the axiomatisation above, IK, as, in analogy with K, it forms the base of the IMLs. Simpson, in his thesis~\cite{simpson1994Thesis}, argues that the IMLs should be considered the real intuitionistic analogue to the normal modal logics and, as part of his argument for this position, shows he can obtain a normalising natural deduction system for the IMLs, using labelled formulae. However, from the perspective of constructive reasoning, axioms $k_3$ to $k_5$ are troublesome. This begs the question, if we remove axioms $k_3$ to $k_5$, can we obtain a constructively reasonable logic with a normalising natural deduction system with introduction and elimination rules for the modalities, as in the case of IK? The logic obtained by removing axioms $k_3$ to $k_5$, called ``Constructive K'' (CK), in fact, admits a non-labelled, normalising, natural deduction system, as discussed in~\cite{BellinDePaivaRitterCurryHowardForCK}. However, this system has an unfortunate and somewhat undesirable property\footnote{Undesirable, from the definitional point of view of the inference rules.} that the modalities each have only one inference rule that acts as both an introduction and an elimination rule. Not satisfied with this system, we instead propose a labelled, normalising, natural deduction system for CK, that can be considered a modification of Simpson's for IK, where $\Box$ and $\Diamond$ both have introduction and elimination rules. We do this by starting from Simpson's system for IK and, by combining the techniques of Strassberger, Das and Arisaka~\cite{StrassbergerDasArisakaNestedSequentsForConstructiveModalLogics} and Masini~\cite{Masini2NatDed}, surgically removing features of the natural deduction system to make it sound and complete for CK. The methodology used is completely proof-theoretically motivated but certain interesting properties, obvious in the semantics, such as the upward closure condition for $\bot$ (c.f.~\cite{BellinDePaivaRitterCurryHowardForCK,degroot2025semanticalanalysisintuitionisticmodal}) come to the forefront in this calculus. We use Strassberger, Das and Arisaka~\cite{StrassbergerDasArisakaNestedSequentsForConstructiveModalLogics} as a starting point, as they have a nested sequent calculus for CK that retains cut elimination. Nested calculi~\cite{Bruennler2009,StrassbergerDasArisakaNestedSequentsForConstructiveModalLogics} allow for strict tree-like reasoning where formulae can be considered as residing in ``branches'' of a tree. This tree-like reasoning is a core aspect of the proof system we develop. When eschewing ourselves of the explicitly nested structure of nested sequents, instead appealing to a labelling system, we have two choices of how to assign labels to formulae such that we preserve the tree-like reasoning structure: Firstly, one can label formulae by the sequence of nodes required to reach the ``position'' it is at, as used by Martini, Masini and Zorzi~\cite{MartiniMasiniMargheritaFrom2SequentsAndLinearToNatDed}. Whilst perfectly reasonable, doing so seems somewhat syntactically heavy. Furthermore, extending this approach to the rest of the cube seems somewhat unwieldy. Alternatively, one can use a simple labelling scheme, akin to that of Simpson's calculus for IK, instead demanding globally that the underlying graph of the consequence relation always remains a tree. This is the approach we take, though this restriction alone is not enough. To fully capture the ``nested-like'' reasoning, we also need to introduce the concept of context restrictions to rules. The restriction says that the derivation of hypothesis cannot occur using open assumptions holding at certain worlds. We observe that context restrictions are not completely novel, for they are present in Massini's 2-Natural Deduction~\cite{Masini2NatDed} for Deontic logic, albeit in a slightly different form. It turns out, these two modifications suffice to develop a normalising natural deduction system for CK and in fact, extending this calculus to the rest of the constructive modal cube is as trivial as in the case of IK, except in the case of logics with the ``B'' axiom, where the approach presented seems to break down.

ABSTRACT. Property directed reachability (PDR, also known as IC3) is a model checking algorithm for proving or refuting safety properties of transition systems. Although many variants and extensions have been studied, presentations and implementations of PDR algorithms often rely on concrete representations and solver-based mechanisms. This sometimes makes it difficult to identify the underlying algorithmic principles and to develop natural extensions. In this talk, I will present a lattice-theoretic abstraction of PDR, in which PDR can be understood as an interaction between searches for invariants and counterexamples. This abstraction reveals that the interaction is mediated by an adjunction representing forward and backward computations along transitions. I will then explain how to handle cases where such an adjunction is not available. The required adjunction can be recovered by the lower-set construction, which is categorically understood as a free cocompletion via Kan extensions. Finally, I will discuss how this framework yields a PDR algorithm solving max reachability problems for Markov decision processes, together with experimental results.

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. Feasible interpolation is a property of a proof system, a complexity-sensitive variant of Craig interpolation, which has become a powerful tool in proof complexity. It can be used to establish the existence of hard theorems, that is, short formulas that require exponentially long proofs in a given system. In this talk, we provide a gentle introduction to feasible interpolation and its applications. We show that it holds for weak proof systems such as resolution and the cut-free sequent calculus, yielding exponential lower bounds on proof length. We then turn to strong proof systems, such as the sequent calculus LK, and show that feasible interpolation fails for them, assuming widely believed cryptographic hardness assumptions, including the security of RSA and the Diffie–Hellman key-exchange protocol against polynomial-size circuits. Finally, we explain how this failure implies that these strong proof systems are not automatable in a precise formal sense.

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. Whether LLMs can reason or write software is widely debated, but whether they can write software that itself reasons is largely unexplored. We present a case study in which an LLM coding agent builds a complete DPLL(T)-style SMT solver for QF_UF with zero human-written code. The solver implements the Nieuwenhuis-Oliveras congruence closure algorithm, includes preprocessing, and emits Lean proofs for unsatisfiable instances. We describe the development process and key challenges, and show that the resulting solver is competitive on SMT-LIB benchmarks. While full proof emission for unsatisfiable instances appears to be beyond the capabilities of the LLM, the solver achieves competitive performance and passes correctness tests.

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, 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. Satisfiability Modulo Theory (SMT) has recently emerged as a powerful tool for solving various automated reasoning problems across diverse domains. Unlike traditional satisfiability methods confined to Boolean variables, SMT can reason on real-life variables like bitvectors, integers, and reals. A natural extension in this context is to ask quantitative questions. One such query in the SMT theory of Linear Real Arithmetic (LRA) is computing the volume of the entire satisfiable region defined by SMT formulas. This problem is important in solving different quantitative verification queries in software verification, cyber-physical systems, and neural networks, to mention a few. We introduce ttc, an efficient algorithm that extends the capabilities of SMT solvers to volume computation. Our method decomposes the solution space of SMT Linear Real Arithmetic formulas into a union of overlapping convex polytopes, then computes their volumes and calculates their union. Our algorithm builds on recent developments in streaming-mode set unions, volume computation algorithms, and AllSAT techniques. Experimental evaluations demonstrate significant performance improvements over existing state-of-the-art approaches.

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. The falsifier calculus [1] has recently been introduced as a new deep-inference proof system for first-order predicate logic in the language of Hilbert’s epsilon-calculus. It uses a new inference rule, the falsifier rule, to introduce epsilon-terms into proofs that is distinct from the critical axioms of the traditional epsilon-calculus. The falsifier rule is a generalisation of one of the quantifier-shifts, inference rules for shifting quantifiers inside and outside of formulae. Like the epsilon-calculus and proof systems which include quantifier-shifts, the falsifier calculus admits non-elementarily smaller cut-free proofs of certain first-order theorems than Gentzen’s sequent calculus. Analogous to the way in which Herbrand’s Theorem decomposes a proof into a first-order and a propositional part, connected by a Herbrand disjunction as an intermediate formula, the falsifier calculus provides a new decomposition theorem for first-order proofs which gives rise to a new notion of intermediate formula in the epsilon-calculus, falsifier disjunctions. Certain first-order theorems admit non-elementarily smaller falsifier disjunctions than Herbrand disjunctions, providing a new perspective on the structure and complexity of Herbrand disjunctions. This talk will overview the established work on the falsifier calculus and explore the ongoing research into using the falsifier calculus as a means of extracting Herbrand disjunctions from first-order proofs. [1] Cameron Allett, Non-Elementary Compression of First-Order Proofs in Deep Inference Using Epsilon-Terms, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024), Tallinn, Estonia, Association for Computing Machinery, 2024.

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 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. Mathematicians and computer scientists are increasingly using proof assistants to formalize and check correctness of complex proofs. This is a non-trivial task in itself, however, with high demands on human expertise. Can we lower the bar by introducing automation for conjecturing helpful, interesting and novel lemmas? We present the first neuro-symbolic lemma conjecturing tool, LEMMANAID, designed to discover conjectures by drawing analogies between mathematical theories. LEMMANAID uses a fine-tuned LLM to generate lemma templates that describe the shape of a lemma, and symbolic methods to fill in the details. We compare LEMMANAID against the same LLM fine-tuned to generate complete lemma statements (a purely neural method), as well as a fully symbolic conjecturing method. LEMMANAID consistently outperforms both neural and symbolic methods on test sets from Isabelle's HOL library and from its Archive of Formal Proofs (AFP). Using DeepSeek-coder-6.7B as a backend, LEMMANAID discovers 50% (HOL) and 28% (AFP) of the gold standard reference lemmas, 8-13% more than the corresponding neural-only method. Ensembling two LEMMANAID versions with different prompting strategies further increases performance to 55% and 34% respectively. In a case study on the formalization of Octonions, LEMMANAID discovers 79% of the gold standard lemmas, compared to 62% for neural-only and 23% for the state of the art symbolic tool. Our result show that LEMMANAID is able to conjecture a significant number of interesting lemmas across a wide range of domains covering formalizations over complex concepts in both mathematics and computer science, going far beyond the basic concepts of standard benchmarks such as miniF2F, PutnamBench and ProofNet.

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. Handling inconsistency is an ubiquitous issue in data and knowledge processing, which has been raised early on and has continuously been receiving a lot of attention. Various methods and approaches have been developed, resulting in a rich landscape for tackling this problem. In this talk, we consider the history and evolution of the topic, as well as possible future directions from a KR perspective and personal experience.

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. In this talk, I will consider model counting, which asks to output the number of solutions to a given input instance. I will present recent complexity results and a solving approach that employs structural parameters (treewidth) for faster solving. While the algorithm provides a theoretical bound, a direct implementation is, unsurprisingly, practically infeasible. Therefore, we turn our attention to a more practical exploitable direction. Finally, I will illustrate practical applications of counting to analyze and navigate solution spaces, including directions that focus on counting for decision spaces rather than entire solution spaces, significantly improving complexity.

ABSTRACT. We introduce Disintegration Temporal Logic (DTL), a new probabilistic temporal logic that can express a wide range of probabilistic hyperproperties, including probabilistic non-interference and perfect indistinguishability. DTL is based on the notion of measure disintegration from probability theory, which allows for conditioning probabilities on a finite or infinite sequence of events occurring during a program execution. We relate the new logic to existing concepts, such as distributional transformers for Markov decision processes, probabilistic au- tomata on infinite words, and existing probabilistic logics. While model checking Markov chains against full DTL is undecidable, we identify two decidable fragments that capture many hyperproperties of interest. The qualitative fragment is handled by an automata-theoretic procedure that extends the standard algorithm for HyperCTL∗ with reasoning about the bottom strongly connected components. The linear fragment admits a polynomial-time model-checking procedure based on linear algebraic techniques.

ABSTRACT. This work investigates the affine segment decomposition algorithm used in the Rocq-NN-Roll prover for neural network hyperproperties through the lens of monoidal categories. This perspective is designated for future integration into Rocq-NN-Roll to facilitate reasoning.

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.

ABSTRACT. Theory and Applications of Craig Interpolation. Edited by Balder ten Cate, Jean Christoph Jung, Patrick Koopmann, Christoph Wernhard and Frank Wolter. Ubiquity Press, DOI 10.5334/bdg, open access. To appear in July 2026. Preprints accessible from https://cibd.bitbucket.io/taci/. Uniting experts from logic, computer science, and philosophy, this volume surveys classical and modern work on Craig Interpolation and Beth Definability. It highlights foundational results, new techniques, and applications in verification, automated reasoning, and databases, offering an indispensable reference for researchers and graduate students.