ABSTRACT. Modern AI systems have achieved remarkable capabilities, yet they continue to struggle with reasoning, robustness under uncertainty, semantic controllability, and reliable generalisation across diverse tasks and environments. Addressing these challenges requires methods that meaningfully integrate data-driven learning with explicit representations of structure, knowledge, and inference. In this talk, I present a neuro-symbolic perspective on these challenges, grounded in work on learning from answer sets and extended to reward learning, task representations, foundation models, and controlled generation. I explore how symbolic representations and logical semantics can be learned from raw and noisy data, integrated with neural architectures, and used to support interpretable inference and reasoning across a range of settings. The research challenges I address include learning symbolic abstractions from perception, learning robust task representations for reinforcement learning, integrating symbolic reasoning with foundation models, and controlling the semantic behaviour of generative models. The central question unifying this work is how to build AI systems that are not only accurate, but semantically grounded, robust, and capable of reasoning that generalises well beyond the tasks they were trained on.

ABSTRACT. The differential λ-calculus studies how the quantitative aspects of programs correspond to differentiation and to Taylor expansion inside models of linear logic. Recent work has generalized the axioms of Taylor expansion so they apply to many models that only feature partial sums. However, that work does not cover the classic web based models of Köthe spaces and finiteness spaces. First, we provide a generic construction of web based models with partial sums. It captures models, ranging from coherence spaces to probabilistic coherence spaces, finiteness spaces and Köthe spaces. Second, we generalize the theory of Taylor expansion to models in which coefficients can be non-positive. We then use our generic web model construction to provide a unified proof that all the aforementioned web based models feature such Taylor expansion.

ABSTRACT. Quantum causal models extend classical causal models to quantum systems. In particular, Quantum Bayesian networks, first introduced in foundational work by Henson, Lal, and Pusey (2014) provide a mathematical formalism to describe causal relations, to analyse correlations, and to predict the probabilities of measurement outcomes, in systems involving both classical and quantum data. Such a framework generalizes Pearl's Bayesian networks—prominent graphical models for classical probabilistic reasoning and inference. Our paper brings compositional principles and a typing discipline into the setting of Quantum Bayesian Networks, with two main contributions. - First, a compositional semantics with a key feature: when all causes are classical, it coincides with the standard semantics of Bayesian networks (which is key to inference algorithms), while in the purely quantum case it reduces to tensor networks. - Second, a typed graphical formalism based on linear logic proof nets, where types ensure well-behaved composition of systems.

ABSTRACT. The purpose of this paper is to invite structural proof theorists to a challenging problem in substructural and fuzzy logics: the consistency of Cantor-Lukasiewicz naive set theory. To this end, we consider two logics: FLew (Full Lambek calculus with exchange and weakening) and its extension \L (Lukasiewicz' infinite-valued logic). The former is equivalently specified as the !-free intuitionistic linear logic with weakening, while the latter is the most important system of mathematical fuzzy logic. For each of them, we consider two extensions: one with simultaneous fixed points of formulas and the other with naive set theory with unrestricted comprehension, so that we end up with four systems: FLew-fix, FLew-set, \L-fix and \L-set. The first two admit an easy proof of consistency by cut elimination, while the third admits a proof by Brouwer's fixed point theorem. The last system \L-set (Cantor-Lukasiewicz set theory) is our main target. Although its consistency is still open, we prove the consistency of a restricted fragment.

ABSTRACT. Metric temporal equilibrium logic (MEL) extends temporal equilibrium logic (TEL) by incorporating quantitative timing constraints, enabling the specification and analysis of deadlines and durations. MEL is particularly suited for domains where time-bound properties are crucial, such as embedded systems, cyber-physical systems, and real-time software. It facilitates the precise expression of timing behaviors, such as the requirement that an event must occur within 5 milliseconds of a trigger, which often elude traditional qualitative temporal logics. In this paper, we present a Tseitin-like translation that maps any metric temporal formula into a logic programming fragment restricted to past operators. This translation provides a formal bridge to leverage existing Answer Set Programming (ASP) solvers for reasoning about metric temporal constraints. By restricting the target fragment to past operators, we enable more effective evaluation and integration with current ASP-based toolchains for multi-shot solving.

ABSTRACT. The development of temporal extensions to Answer Set Programming (ASP) has led to the emergence of linear-time (TEL), dynamic (DEL), and metric (MEL) temporal logics. However, the inherent rigidity of highly optimized ASP systems often hinders the rapid exploration and implementation of alternative logical designs. In this work, we propose a flexible meta-programming framework that operationalizes the semantics of varied temporal logics through a unified, declarative framework. Our approach extends standard ASP meta-programming by augmenting clingo’s theory grammar with formal type specifications and nesting capabilities. To ensure semantic correctness, we introduce a transformation pipeline that protects nested modalities from stable- model-based simplifications during grounding. We demonstrate the extensibility of our framework by implementing meta-encodings for TEL, MEL, and DEL. We provide a comprehensive account of TEL and highlight the key features for for managing the interval constraints of MEL and the Fischer-Ladner closure in DEL. Finally, we introduce the metasp system, a versatile tool that encapsulates workflow.

ABSTRACT. The Power grid is a critical infrastructure underpinning all aspects of modern society and its services. Maintaining its effectiveness requires continuous adaptations. In particular, addressing sustainability targets, demand patterns, and urbanisation trends requires implementing changes to the network. Actual developments can potentially span over a decade, with supply continuity and service quality that must be preserved throughout by ensuring conformance to several topological and combinatorial invariants. Long-term power grid planning deals with the above process, and although planning languages could be a natural choice, the kind of properties and invariants needed are cumbersome to express in such languages; on the contrary, they can be elegantly and succinctly encoded in Answer Set Programming (ASP). In this paper, we propose the first approach to automate and optimise the long-term power grid planning process using ASP. Experimental evaluations conducted on synthetic and real‑world grid data confirm the expressive power of the proposed ASP‑based approach and demonstrate its effectiveness.

ABSTRACT. We consider a fragment of Higher-Order Datalog with negation and argue that it generalizes the familiar and important fragment of Linear Datalog. We investigate the expressive power of this fragment, establishing a tight connection with the hierarchy of space complexity classes. In particular, we demonstrate that for all k >= 1, the (k+1)-order fragment of Stratified Linear Higher-Order Datalog$^\neg$ captures (k-1)-EXPSPACE. This result suggests that restricting programs to linear recursion shifts the expressive power of the corresponding fragments from time to space, generalizing the classical result that (Stratified) Linear Datalog captures NL. Unlike the first-order setting where an ordering assumption is required to capture NL, our results hold without any such assumption on the input database. The proof relies on simulating space-bounded Turing machines using Stratified Linear Higher-Order Datalog$^\neg$ programs and providing a space-efficient evaluation of the query program. We argue that identifying such computationally well-behaved fragments is a crucial step towards paving the way for practical implementations of Higher-Order Datalog.

ABSTRACT. Treewidth is a well-studied decompositional parameter to measure the tree-likeness of a graph. While the propositional satisfiability problem (SAT) is known to be tractable when parameterized by the treewidth of the underlying primal graph, the evaluation of quantified Boolean formulas (QBFs) remains PSPACE-complete even on formulas of constant treewidth. Intuitively, this is because ordinary treewidth does not take into account the prefix of the QBF: it neither distinguishes between existential and universal variables, nor accounts for the order in which they are quantified. In the past, several weaker variants of treewidth have been devised to incorporate prefix-sensitive information. To establish tractability for QBFs under these notions, prior work has employed either strategy- or resolution-based techniques, thereby dividing the parameterized complexity landscape of QBF into two regimes that are incomparable in strength. We establish fixed-parameter tractability with respect to bilateral treewidth, a novel and strictly more powerful decompositional parameter that combines these rivaling approaches by simultaneously allowing for branching on strategies and performing Q-resolution.

ABSTRACT. CAQE (Clausal Abstraction for Quantifier Elimination) is currently the most successful algorithmic paradigm for solving Quantified Boolean Formulas (QBF) practice-wise, clearly dominating recent QBF competitions. While apparently being a very strong solver, not much is known about CAQE theory-wise. We propose a framework for formalising CAQE runs which we use to analyse the algorithm proof-theoretically. We show that one can perform strategy extraction on that CAQE proof system in such a way that strategy size serves as a lower bound for CAQE runs. Furthermore, we introduce a measure, which we call CAQE width, which not only acts as a lower bound on CAQE proofs, but — with the quantifier depth as exponent — as an upper bound as well. Using this analysis, we prove that on QBFs of bounded quantifier complexity, both QCDCL (Quantified Conflict Driven Clause Learning, formalised as a proof system) and Q-resolution p-simulate CAQE and are indeed strictly stronger. Hence, as proof systems, QCDCL is provably better than CAQE, contrary to their relative performance in practice.

ABSTRACT. Quantified Boolean Formula (QBF) is a notoriously hard generalization of \textsc{SAT}, especially from the point of view of parameterized complexity, where the problem remains intractable for most standard parameters. A recent work by Eriksson et al.~[IJCAI 24] addressed this by considering the case where the propositional part of the formula is in CNF and we parameterize by the number $k$ of existentially quantified variables. One of their main results was that this natural (but so far overlooked) parameter does lead to fixed-parameter tractability, if we also bound the maximum arity $d$ of the clauses of the given CNF. Unfortunately, their algorithm has a \emph{double-exponential} dependence on $k$ ($2^{2^k}$), even when $d$ is an absolute constant. Since the work of Eriksson et al.\ only complemented this with a SETH-based lower bound implying that a $2^{O(k)}$ dependence is impossible, this left a large gap as an open question. Our main result in this paper is to close this gap by showing that the double-exponential dependence is optimal, assuming the ETH: even for CNFs of arity $4$, QBF with $k$ existential variables cannot be solved in time $2^{2^{o(k)}}|\phi|^{O(1)}$. Complementing this, we also consider the further restricted case of QBF with only two quantifier blocks ($\forall\exists$-QBF). We show that in this case the situation improves dramatically: for each $d\ge 3$ we show an algorithm with running time $k^{O_d(k ^{d-1})}|\phi|^{O(1)}$ and a lower bound under the ETH showing our algorithm is almost optimal.

ABSTRACT. The so-called algebraic approach to the constraint satisfaction problem (CSP) has been a prevalent method of the study of complexity of these problems since early 2000's. The core of this approach is the notion of polymorphisms which determine the complexity of the problem (up to log-space reductions). In the past few years, a new, more general version of the CSP emerged, the promise constraint satisfaction problem (PCSP), and the notion of polymorphisms and most of the core theses of the algebraic approach were generalised to the promise setting. Nevertheless, recent work also suggests that insights from other fields are immensely useful in the study of PCSPs including algebraic topology. In this paper, we provide an entry point for category-theorists into the study of complexity of CSPs and PCSPs. We show that many standard CSP notions have clear and well-known categorical counterparts. For example, the algebraic structure of polymorphisms can be described as a set-functor defined as a right Kan extension. We provide purely categorical proofs of core results of the algebraic approach including a proof that the complexity only depends on the polymorphisms. Our new proofs are substantially shorter and, from the categorical perspective, cleaner than previous proofs of the same results. Moreover, as expected, are applicable more widely. We believe that, in particular in the case of PCSPs, category theory brings insights that can help solve some of the current challenges of the field.

ABSTRACT. Higher-dimensional automata (HDAs) provide a geometric model of true concurrency, yet their standard formulation encodes an artificial total order on events. This representational artifact causes a fundamental mismatch between the combinatorial structure of HDAs and their observable behavior, leading to logical asymmetries and complicating the application of categorical tools. In this paper, we resolve this tension by developing a semantics for HDAs that is independent of event order, based on interval ipomsets (partially ordered multisets with interfaces) that preserve only precedence and concurrency. We prove that for any HDA, the traditional ST–trace of an execution path corresponds precisely to its associated interval ipomset. On the structural side, we show that the presheaf-theoretic presentation with an unordered base and the combinatorial presentation of symmetric HDAs are categorically isomorphic. Finally, by characterizing ST- and hereditary history-preserving (hhp) bisimulation via ipomset isomorphism, we provide a unified, order-free foundation for HDA semantics. Our results resolve several critical ambiguities in the literature: they provide the necessary path-category structure to canonically apply the Open Maps framework, eliminate representational artifacts in temporal and modal logics, and bridge systematic mismatches between HDAs and other models of concurrency such as Petri nets.

ABSTRACT. We explain how to construct a cartesian closed fibration of higher-order regular languages using glueing techniques combined with a fibered refinement of the usual Frobenius reciprocity formula.

ABSTRACT. We present a unified, categorical theory of monads and distributive laws \emph{in substructural contexts}. In the study of distributive laws, the roles of (the absence of) structural rules for variable contexts have been recognized; our theory formalizes these substructural situations using Tronin's \emph{verbal categories} $\W$, in a uniform and presentation-independent manner. We define the notion of \emph{$\W$-operadic monad} (those ``defined'' in the context $\W$) and that of \emph{$\W$-commutative monad} (those ``preserved'' in the context $\W$). We present a canonical construction of a distributive law $ST\to TS$; it is applicable when $S$ is $\W$-operadic and $T$ is $\W$-commutative (under mild conditions). This accounts for many known and new distributive laws. When the condition fails, we can \emph{refine} $S$ and force $\W$-operadicity; this generalizes Varacca and Winskel's construction of indexed valuations.

ABSTRACT. A monadic decomposition of a formula over a first-order theory is an equivalent Boolean combination of atomic formulas, each containing only one variable. Monadic decomposition is a generic simplification technique that has found applications in various settings such as quantifier elimination, string solving, and constraint databases. Previous work has mostly focused on the decision problem of whether a formula admits a monadic decomposition. However, much less is known on how to actually efficiently produce a small monadic decomposition, which is required for any application. We study this question for the quantifier-free fragment of Presburger arithmetic. Here, monadic decomposability is known to be coNP-complete, and monadic decompositions can be computed in exponential time. An exponential size lower bound was only known for monadic decompositions in DNF or CNF. In this work, we extend this an exponential lower bound to general monadic decompositions. Guided by this lower bound, we present fragments that admit polynomially-sized monadic decompositions which, in many cases, can be constructed efficiently. A surprising key ingredient in our proof are small-depth circuits for arithmetic operations in Chinese remainder representation, due to Beame, Cook, Hoover (1986).

ABSTRACT. We consider expansions of Presburger arithmetic with families of monadic polynomial predicates. (Examples of such predicates are the set of perfect squares, or the set of integers of the form 2n^3-5n+3, etc.) Although the full attendant first-order theories are well known to be undecidable, very little is known when one restricts the number of variables. For single-variable theories, we obtain positive results for the following families of predicates: (i) for perfect powers, decidability of the corresponding theory follows from the solvability of hyperelliptic Diophantine equations; (ii) for polynomials of degree at most three, we establish decidability by relying on the low genus of the resulting algebraic curves; (iii) for arbitrary polynomials, conditional decidability is entailed by an effective version of Faltings's theorem, which itself was recently proved subject to certain classical number-theoretic conjectures. In turn, we present various hardness results for theories with unresolved decidability status by using them to encode certain longstanding open Diophantine problems.

ABSTRACT. Recently, symbolic structures were proposed as finite representations of potentially infinite first-order structures, where Linear Integer Arithmetic terms and formulas define the domain and interpretations of a structure. We generalize symbolic structures to use any base theory that admits a standard model, and prove decidability of the model-checking problem, which determines whether a given symbolic structure satisfies a given first-order formula, for decidable base theories. This enables proving decidability for fragments of first-order logic by establishing a symbolic model property, which states that every satisfiable formula has a symbolic model. We use this approach to prove decidability for several fragments that extend the fragment of stratified formulas, relaxing the quantifier-alternation constraints by allowing one sort to have self-looping functions, under certain restrictions. To establish the symbolic model property for these fragments we construct a symbolic model for a formula from an arbitrary model. The construction and its correctness are proved in a generic fashion, which may be instantiated to other similarly restricted fragments.

ABSTRACT. The Orbit Problem asks whether the orbit of a point under a matrix reaches a given target set. When the target is a single point, the problem was shown to be decidable in polynomial time by Kannan and Lipton. This decidability result was later extended by Chonev et al. to targets of dimension 3 (in arbitrary ambient dimension), but decidability remains open for subspaces of dimension 4. At the other extreme, the special case of the Orbit Problem in which the target set is a hyperplane of codimension 1 is equivalent to the Skolem Problem for linear recurrence sequences, whose decidability has been open for many decades. In this paper, we show that the Orbit Problem is decidable if the target subspace has dimension logarithmic in the dimension of the orbit. Over rationals, we moreover obtain a complexity bound NP^RP in this case. On the other hand, we show that the version of the Orbit Problem where the dimension of the target subspace is linear in the dimension of the orbit is as hard as the Skolem Problem.

ABSTRACT. The starting point of this paper is work by Lakemeyer and Levesque, who proposed an epistemic logic where the beliefs of aknowledge-based agent are characterized in terms of increasing levels of complexity. At the lowest level, the agent is only able to draw simple conclusions from its knowledge base. Higher levels lead to more and more inferences and computing the beliefs at any particular level turns out to be tractable. What makes this logic particularly appealing is the fact that the underlying semantics is based on possible worlds. However, the work is still limited in that only beliefs about what is true in the world are considered, that is, an agent's beliefs about its own beliefs are ignored. In this paper we will close this gap and generalize the earlier work by proposing a model of limited belief where anagent is able to fully introspect on its own beliefs without sacrificing tractability.

ABSTRACT. The cops and robber game is a well-studied model for investigating pursuit-evasion phenomena among many others. While many variants of this game have been studied in the literature, the epistemic assumptions underlying their game designs are often left implicit. In this work, we focus on the imperfect information version of the game and re-examine it from an epistemic perspective to explore the levels of player knowledge that are essential for playing the game. To facilitate our investigations, we discuss two kinds of strategies for the players, history-based and positional, and show what matters in this context. Our study eventually sheds light on the implicit assumptions prevalent in the existing literature in terms of player knowledge while playing the game.

ABSTRACT. We present SRIP, a SAT-based system for solving the Independent Set Reconfiguration Problem (ISRP) under the Token Jumping (TJ) rule. SRIP formulates ISRP with SAT problems employing a clique-partition-based constraint model and a set of pruning constraints that strengthen propagation and reduce the search space for reconfiguration. The resulting model is compiled into a sequence of SAT problems and solved using incremental SAT within a bounded model checking framework, enabling SRIP to compute shortest reconfiguration sequences efficiently. We evaluate SRIP on benchmark instances from the CoRe Challenge, a competition series dedicated to ISRP under TJ. SRIP finds optimal (shortest) reconfiguration sequences for 477 out of 693 instances, achieving the best results among state-of-the-art solvers on this benchmark suite.

ABSTRACT. Answer set programming (ASP) in the NP fragment can be solved by translating into propositional satisfiability (SAT). However, for non-tight programs, this requires additional encodings to enforce acyclicity of the underlying dependency graph, making acyclicity handling a key challenge in translating ASP encodings of decision and optimization problems into SAT and maximum satisfiability (MaxSAT). Various SAT encodings of acyclicity exploiting structural graph properties have recently been proposed for various settings. Focusing on ASP, we show that such encodings are captured by a generalized transitive closure framework. The framework can be instantiated for obtaining various types of refined transitive closure encodings. We consider four concrete instantiations framework, analyzing their correctness and size. Putting the framework into practice, we show through extensive empirical evaluation that current state-of-the-art SAT and MaxSAT solvers are competitive with, and can often outperform, state-of-the-art native ASP solvers on both decision and optimization problems.

ABSTRACT. The acceptance of AI agents in daily life hinges on their alignment with social, moral, and legal norms, and in recent years, attempts to build norm-sensitive AI agents --- including reinforcement learning (RL) agents --- have gained traction. However, while there are many promising approaches, they tend to be geared toward environments with modest state spaces, and adaptations to the \textit{deep RL} context are lacking. In this paper we present a deep learning adaptation of \textit{normative restraining bolts} (NRBs). Our contributions are twofold; we combine NRBs with deep Q-networks (DQNs) and proximal policy optimization (PPO) to learn optimal behaviour compliant with challenging norms in a complex environment, demonstrating our agent's ability to learn difficult normative behaviours in the game Pac-Man, which has been used to benchmark normative RL techniques in the past. Secondly, while past work has assumed a lexicographic ordering over conflicting norms when finding appropriate weights for norms, we discuss the shortcomings of this approach, and provide an alternative which is both far more scalable, and allows for the selection of policies deemed ideal by more complex metrics.

ABSTRACT. A normative supervisor is an external module that uses a for- mal reasoning engine to impose normative constraints on re- inforcement learning agents, by either dynamic action mask- ing or feeding the agent additional punishments when vio- lations of norms occur (or both). In this paper, we use a normative supervisor implemented with a solver for deontic answer set programming (ASP) — deolingo — as a ba- sis for the construction of a normative narrator, which uses deolingo’s ability to interface with the explainable solver xclingo to construct a module capable of both regulat- ing behaviour through action masking and additional punish- ments, and providing contrastive explanations of why a given action was allowed while others were not, relative to the nor- mative system being enforced. The explanations are mod- elled after the two tiers – internal and external – of expla- nation. We demonstrate this approach’s ability to provide un- derstandable and descriptive explanations in a scenario where a taxi driver agent must act in accordance to a normative sys- tem governing its normal duties and provisions that must be made in case of an emergency.

ABSTRACT. A variable in a quantified Boolean formula (QBFs) is defined, if its value is uniquely determined by some other variables. Such definitions are widely exploited in various techniques for QBF solving. In this work, we formalize the concept of using definitions for reducing variable dependencies by introducing a novel dependency scheme and investigate its proof-theoretic impact. Our analysis shows that a definition-based dependency scheme is able to detect independencies other established dependency schemes cannot and that this can lead to exponentially shorter refutations. We further demonstrate that our scheme can be combined with any other scheme and that such a combined use can exponentially outperform using either scheme alone. Moreover, we study the dynamic application of our definition-based dependency scheme, which leads to another exponential speedup compared to the static application. Finally, we analyze the computational complexity of our dependency scheme and introduce a family of efficiently computable variants.

ABSTRACT. Certification for Quantified Boolean Formulas (QBF) and Dependency Quantified Boolean Formulas (DQBF) is an ongoing challenge. Recent proof complexity work has shown that the majority of QBF and DQBF techniques can be p-simulated by using the independent extension rule. In propositional logic, extension rules are supported by proof checkers using a more general RAT (Resolution Asymmetric Tautology) rule. The obvious next step in (D)QBF certification would be to update these modern RAT formats to match the strength of this independent extension rule. In this paper we first introduce a new dependency scheme called Dpure, this rule is the missing ingredient that when added to Blinkhorn's proof system DQRAT allows it to be p-equivalent to the Independent Extended QU-Res, the most powerful of the known QBF and DQBF proof systems. Up until now, DQRAT has only existed in theory, so we implement a prototype checker DQRAT-check which includes our extra rule. In addition to its inclusion in our proof checker we show Dpure has two other properties that have been found for previous dependency schemes, and each of these observations has potential in solving/checking. We demonstrate a strategy extraction theorem for long distance Q-resolution equipped with Dpure, meaning it can be incorporated soundly into the dependency learning solver Qute.

ABSTRACT. Strategy extraction in QBF proof systems usually attempts to extract winning strategies from valid proofs. However, an alternative (and arguably more powerful) view is to extract Skolem/Herbrand functions, or equivalently synthesis of the game values at all intermediate points. In this paper, we investigate the existence and properties of such proof systems from which one can extract Skolem and Herbrand functions. We propose such a proof system for QBF, which we show is sound and complete, and from which extraction of Skolem/Herbrand functions can be performed, and game values computed, in polynomial time. We also show that this system is optimal among all proof systems that allow efficient extraction of Skolem/Herbrand functions. We provide conditional lower bound results for our new proof system and compare it to several existing/standard proof systems for QBF that have been studied in the literature, showing interesting orthogonality results. Finally, we provide a compilation algorithm that takes an arbitrary QBF and synthesizes a proof in our system, from which Skolem and Herbrand functions can be easily computed.

ABSTRACT. For a quantified Boolean formula (QBF), the problem of computing the number of winning strategies is known as the #QBF problem. This problem is considered harder than the analogous #SAT problem. Recently, important proof systems for QBFs and #SAT have been studied. By extending the ideas from both fields, we show that it is possible to design proof systems for #QBF. Such proof systems are important not only for advancing the theory of #QBF but also for certifying and designing better #QBF solvers, an area that is still in its early stages. In this paper, we explore #QBF proof systems to count the number of Skolem functions. Apart from a naive system, we study #QBF systems based on the expansion rule of universal variables in QBFs. We observe that these systems have inherent structural weaknesses that lead to lower bounds. As an alternative, we propose a #QBF proof system that we call Q-MICE, which consists of sound inference rules for computing and certifying the #QBF solution, similar to the line-based #SAT proof system MICE. To demonstrate the strength of Q-MICE, we present various upper bounds, such as the quantified version of the propositional XOR-PAIRS formula, which are known to be hard for MICE. Consequently, we also separate Q-MICE from the expansion-based #QBF proof systems.

ABSTRACT. We describe a procedure that extracts existential strategies from verification proofs in the Long-Distance Consensus (i.e.\ Term-Resolution) proof system when augmented with dependency schemes. We prove that when the standard dependency scheme D^{std} is used, the extracted strategies are winning strategies, thus establishing soundness of the proof system LDQ(D^{std})Consensus. We show through a counterexample that this approach fails to show soundness for LDQ(D^{rrs})Consensus.

ABSTRACT. Discrete probabilistic programs (DPPs) provide a highly expressive formalism for compactly defining arbitrary finite probabilistic models. This expressivity comes at a price: DPP inference is PSPACE-hard. In this work, we show that DPP inference only takes polynomial time for programs that are `structurally simple'. More precisely, inference can be performed in polynomial time when the primal graph of each function appearing in the probabilistic program has bounded treewidth, and the inverse acceptance probability is at most exponential in the size of the probabilistic program. Existing algorithms do not achieve this performance guarantee. Our method relies on finding suitable decompositions, algebraisations, of the string diagrams underlying DPPs, employing existing algorithms for tree decompositions. This is independent of the probabilistic setting of DPPs and has direct applications to many problems, such as evaluating queries on relational databases and cybersecurity risk assessment via attack trees.

ABSTRACT. The Metropolis--Hastings (MH) algorithm is a foundational Markov chain Monte Carlo algorithm. In this paper, we ask whether it is possible to formulate and analyse MH with existing tools from categorical probability theory, using a recent involutive framework proposed for MH-type algorithms as a concrete case study. We first show how basic concepts such as invariance and reversibility can be formulated in Markov categories, and how aspects of the involutive framework can be captured using CD categories. We then study enrichments of CD categories over commutative monoids. These provide a rich setting for reasoning synthetically about a range of important probabilistic concepts, including substochastic kernels, finite and $\sigma$-finite measures, absolute continuity, singular measures, and Lebesgue decompositions. This structure allows us to give very general necessary and sufficient conditions for an MH-type sampler to be reversible with respect to a given target distribution.

ABSTRACT. We establish a connection between two results in the literature on probabilistic semantics: a formulation of De Finetti's theorem in the language of category theory due to Jacobs and Staton, and the generic construction of the free exponential of Linear Logic by Melliès et al, that has been instantiated in the model of probabilistic coherence spaces by Crubillé et al. The structural proximity of these two construction is manifest, but making this connection formal requires technical developments on the relationship between the category of stochastic kernels and the category of integrable cones, two well-known categories in probabilistic semantics. We then use this connection to give a characterization of the total elements of the probabilistic coherence space $!\Bool$.

ABSTRACT. We describe semantic structures relevant for interpreting dependent types for statistical and probabilistic modelling. Our development extends the theory of quasi-Borel spaces (qbses) of Staton et. al, which support simply-typed, higher-order probability theory with continuous distributions. It is well-known that qbses can interpret a dependent-type theory supporting dependent function-spaces through the codomain fibration. We define an equivalent split fibration based on the family fibration, which we call quasi-Borel families (qbfs), characterise its structure, equip it with fibred monads of measures and probability, and use them to develop dependently-typed probability theory. We characterise the structure of the qbf fibration that is relevant for dependently-typed probability theory in elementary form. Our characterisations include: context extension, dependent pairs, dependent functions, extensional identity types, fibred products and coproducts, subspaces, a universe of propositions, and straightforward internalisation and externalisation principles for discrete spaces. We use these concepts to define fibred distribution and probability monads, the semantic structure needed to interpret probability distributions under a dependent context. We show that this structure satisfies a fibred version of Kock's synthetic measure theory. We also use these concepts to develop a qbs counterpart to Kolmogorov's conditional expectation. Our main result is a version of the conditional expectation that, under standard regularity assumptions, is measurable in both the random variables we are conditioning, and the observation map we are conditioning by.

ABSTRACT. Stable graphs, or equivalently Littlestone classes, were characterized by existence of linear-sized 'good' sets, a kind of strongly homogeneous set, in work of Malliaris-Shelah and Malliaris-Moran. We prove a parallel result for VC classes, showing these are characterized by existence of linear-sized symmetric or asymmetric good pairs (which we define). We give several proofs, each requiring drawing from methods and results from different areas, and resulting in different kinds of bounds. We finish with a few words on our learning theory motivation for these investigations and state some further research directions.

ABSTRACT. Consider two planar graphs which are subject to edge insertions and deletions. We show that whether the two graphs are isomorphic can be maintained with first-order logic formulas and auxiliary data of polynomial size. This places the dynamic planar graph isomorphism problem into the dynamic descriptive complexity class DynFO. As a consequence, there is a dynamic constant-time parallel algorithm with polynomial-size auxiliary data which maintains whether two dynamic planar graphs are isomorphic.

ABSTRACT. An infinite structure has the finite length property (over a given field) if, for each of its finite powers, strict chains of equivariant subspaces in the corresponding free vector space are bounded in length. Prior work showed that the countable pure set and the dense linear order without endpoints have this property.We generalise these results to (a) structures approximated by finite substructures with few orbits, provided the field is of characteristic zero, and (b) generically ordered expansions of Fraïssé limits with free amalgamation, in vocabularies consisting of unary and binary relations. As a special case, we deduce the finite length property of the Rado graph using both methods. We also describe some connections with function spaces, weighted register automata, and solving orbit-finite systems of linear equations.

ABSTRACT. Lovász (1967) showed that two graphs $G$ and $H$ are isomorphic if, and only if, they are homomorphism indistinguishable over all graphs, i.e., $G$ and $H$ admit the same number of number of homomorphisms from every graph $F$. Subsequently, a substantial line of work studied homomorphism indistinguishability over restricted graph classes. For example, homomorphism indistinguishability over minor-closed graph classes $\mathcal{F}$ such as the class of planar graphs, the class of graphs of treewidth $\leq k$, pathwidth $\leq k$, or treedepth $\leq k$, was shown to be equivalent to quantum isomorphism and equivalences with respect to counting logic fragments, respectively. Via such characterizations, the distinguishing power of e.g. logical or quantum graph isomorphism relaxations can be studied with graph-theoretic means. In this vein, Roberson (2022) conjectured that homomorphism indistinguishability over every graph class excluding some minor is not the same as isomorphism. We prove this conjecture for all vortex-free graph classes. In particular, homomorphism indistinguishability over graphs of bounded Euler genus is not the same as isomorphism. As a negative result, we show that Roberson's conjecture fails when generalized to graph classes excluding a topological minor. Furthermore, we show homomorphism distinguishing closedness for several graph classes including all topological-minor-closed and union-closed classes of forests, and show that homomorphism indistinguishability over graphs of genus $\leq g$ (and other parameters) forms a strict hierarchy.

ABSTRACT. The paper identifies a relational semantics for theory revision for various notions of bases in arbitrary Tarskian logics. We extend the general work by Delgrande, Woltran and Peppas to the case of logics with infinitely many interpretations, as is the case, e.g., in many predicate logics. First, we identify a property of relations, min-retractivity, that allows for capturing AGM revision semantically in this general setting fully. Part of the characterisation presented is a method for encoding change operators and capture the notion of a base elegant. Moreover, we characterise those logics in which belief revision operators can be represented by a total preorder.

ABSTRACT. Recently, epistemic spaces have been introduced to formalize instantiations of iterated belief change operators and their translations from one concrete representation (epistemic space) to another. In this work, we build on these notions to deepen the understanding of iterated belief change and propose a general method for comparing the expressiveness of existing representations. We introduce the notion of canonicity for epistemic spaces as a tool for identifying those that are sufficiently or necessarily expressive to realize some properties of iterated change operators. In particular, we give the canonical epistemic space (up to equivalence) that allows us to instantiate any iterated change operator.

ABSTRACT. We investigate the truth-tracking performance of iterated belief-change operators. In particular, we show that a class of improvement operators is guaranteed to converge to the truth when the input sequence contains sufficiently many correct inputs, and we establish a corresponding convergence theorem. We also report experimental results indicating that this convergence typically occurs with relatively short input sequences.

ABSTRACT. Rational belief revision is commonly viewed as being based on a preference order between possible worlds, with the resulting new belief set being those sentences true in all the most preferred models of the incoming new information. Usually, such a preference order is taken to be a total preorder. Nevertheless, there are other, more general classes of ordering that can also be employed. In this paper, we explore two such classes that have been studied within the theory of rational choice but have seen limited or no application in belief revision. We begin with interval orders, introduced by Fishburn in the ’80s, which associate to each possible world a nonnegative ‘interval’ of plausibility. We then move on to biorders, studied by Aleskerov, Bouyssou, and Monjardet, which generalise interval orders by allowing the intervals to have negative lengths, a feature that can be used to capture a notion of dissonance or instability. We provide axiomatic characterisations of these two resulting families of belief revision operators, as well as of two further families of interest that lie between interval orders and biorders. We show that while biorder-based revisions satisfy the Success postulate, they do not always yield consistent outputs. By modifying their definition to discard inputs that lead to inconsistency as ‘incredible’, we derive new families of so-called nonprioritised revision that satisfy the Consistency postulate, but not the Success one. These families are linked to credibility-limited revision operators of Hansson et al., but for which the set of credible sentences does not satisfy the single-sentence closure condition. We argue that the biorder-based approach is well-suited for scenarios where an agent might initially reject new information, but may accept it when presented with additional explanation.

ABSTRACT. Domain-independent planning algorithms require as input an action model that specifies the preconditions and effects of each action. Constructing such models is often challenging for domain experts, particularly in domains where actions involve both Boolean and numeric state variables. We address the problem of learning such hybrid action models from observations of successful action executions. A central challenge is that observing only successful executions provides no explicit evidence about which conditions are necessary for an action to be applicable. This difficulty is especially pronounced for learning numeric preconditions, for which there exist negative theoretical results concerning efficient learnability. To mitigate this limitation, we propose SAM-SVM, a novel numeric action model learning algorithm that learns numeric preconditions by heuristically simulating negative observations, i.e., possible states where actions are inapplicable. We also implemented NSAM+SVM, a hybrid algorithm that integrates SAM-SVM and NSAM, an existing conservative action model learning algorithm. Empirical evaluation demonstrates that SAM-SVM can learn more accurate action models and achieves improved planning performance compared to existing methods on standard numeric planning benchmarks, and NSAM+SVM provides the most robust behavior across most domains.

ABSTRACT. We study whether next-token prediction can yield world models that truly support planning, in a controlled symbolic setting where propositional STRIPS action models are learned from action traces alone and correctness can be evaluated exactly. We introduce two architectures. The first is the STRIPS Transformer, a symbolically aligned model grounded in theoretical results linking transformers and the formal language structure of STRIPS domains. The second is a standard transformer architecture without explicit symbolic structure built in, for which we study different positional encoding schemes and attention aggregation mechanisms. We evaluate both architectures on five classical planning domains, measuring training accuracy, generalization, and planning performance across domains and problem sizes. Interestingly, both approaches can be used to produce models that support planning with off-the-shelf STRIPS planners over exponentially many unseen initial states and goals. Although the STRIPS Transformer incorporates a strong symbolic inductive bias, it is harder to optimize and requires larger datasets to generalize reliably. In contrast, a standard transformer with stick-breaking attention achieves near-perfect training accuracy and strong generalization. Finally, standard transformers without stick-breaking attention do not generalize to long traces, whereas a symbolic STRIPS model extracted from a transformer trained on shorter traces does.

ABSTRACT. It has been recently shown that lifted STRIPS models can be learned correctly and efficiently from action traces alone; i.e., applicable action sequences from a hidden STRIPS model. The result is remarkable because the states are not assumed to be observable at all, and yet it is not practical enough as STRIPS actions include arguments that are not needed for selecting the actions. This shortcoming has been addressed by assuming that the action traces come instead from a hidden STRIPS+ model where some action arguments are implicit in the hidden action preconditions. A limitation of this approach, however, is that it assumes that the states are fully observable. In this work, we relax these restrictions and consider the problem of learning a STRIPS+ action domains from traces in a more general context, where the traces carry partial information about both actions and states. In particular, we formulate algorithms and completeness results for three general cases, all of which assume full observability of some action arguments. In the first case, no observability of the state is assumed, in the second case, full observability of some state predicates is assumed, and in the third case, local observability of some state predicates is assumed instead. Given a STRIPS+ domain one can then determine the conditions under which an equivalent domain will be learned from traces. Experimental results are also reported.

ABSTRACT. Parameterized distributed systems induce an infinite family of concurrent systems indexed by the number of processes, and their learnability cannot be reduced to learning a language in isolation. We address the problem of semantic reconstruction for fine broadcast protocols (fine BPs) from a finite labeled sample and provide an inference procedure that returns a minimal semantically equivalent fine BP when the sample subsumes a suitable characteristic set. Furthermore, we establish hardness boundaries on the learnability of fine BPs, including (i) characteristic sets of exponential size are unavoidable, (ii) consistency is NP-hard, and (iii) predictability is non-polynomial.

ABSTRACT. We study the problem of checking consistency of qualitative preferences expressed in CP-theory languages, which is PSPACE-complete in general. Building on Wilson’s seminal work on sufficient conditions for consistency based on Complete Search (CS) trees, we characterize a necessary and sufficient condition for the existence of a cs-tree, yielding the weakest sufficient condition for cs-tree–based consistency. We show that consistency testing under this condition is coNP-complete. We also present a polynomial-time computable upper approximation of the dominance relation for cs-tree–consistent CP-theory preferences, and prove that it subsumes all previously proposed approximations. Finally, we introduce set-labeled cs-trees, a generalization of cs-trees, which provides a unifying framework for progressively weakening sufficient conditions and ultimately characterizes necessary and sufficient conditions for consistency checking in CP-theory preferences.

ABSTRACT. Compiling a collection of votes (a profile) consists in compressing the information it contains in a minimal way, while still allowing to compute the winner after more votes are received. These additional votes can be understood temporally (when votes come in an asynchronous way) or spatially (when votes are gathered locally in polling stations, and their results published locally before being aggregated on a global level). Given a voting rule, two profiles are equivalent for this rule if for whichever profile we add to each of them, the winner in the two expanded profiles will be the same. An equivalence relation between profiles corresponds to a set of information structures (called compilation structures) encoding equivalence classes. It is well-known that some information structures, such as pairwise majority matrices are the compilation structure for some voting rules, while some others (such as the majority graph) are not. We fully characterise the equivalence relations (or equivalently the information structures) that correspond to some voting rules, and we review a number of interesting information structures and give known voting rules that correspond to them.

ABSTRACT. We extend the languages of Coalition Logic (CL) and Alternating-time Temporal Logic (ATL) with new modalities for welfare-affecting capabilities, capturing the benefit and harm that a coalition can bring to another coalition through its strategic choices. These languages are interpreted over concurrent games enriched with agents’ preferences. On the conceptual side, we use these languages to formalize the notions of potential benefactor and danger. A potential benefactor corresponds to a coalition having the capability to confer a benefit on another coalition. Danger corresponds to a coalition having the capability to inflict harm on another coalition. On the technical side, we present several results concerning their axiomatization, their relationships with standard CL and ATL, and their computational complexity.

ABSTRACT. Asynchronous effects of Ahman and Pretnar complement the conventional synchronous treatment of algebraic computational effects with asynchrony based on decoupling the execution of algebraic operation calls into signalling that an operation's implementation needs to be executed, and into interrupting a running computation with the operation's result, to which the computation can react by installing matching interrupt handlers. Beyond providing asynchrony for algebraic effects, the resulting core calculus also naturally models examples such as pre-emptive multi-threading, (cancellable) remote function calls, multi-party applications, and even a parallel variant of runners of algebraic effects. In this paper, we study the normalisation properties of this calculus. We prove that if one removes general recursion from the original calculus, then the remaining calculus is strongly normalising, including both its sequential and parallel parts. However, this only guarantees termination for very simple asynchronous examples. To improve on this result, we also prove that the sequential fragment of the calculus remains strongly normalising when a controlled amount of interrupt-driven recursive behaviour is reintroduced. Our strong normalisation proofs are structured compositionally as a natural extension of Lindley and Stark's $\top\top$-lifting based approach for proving strong normalisation of effectful languages. All our results are also formalised in Agda.

ABSTRACT. An all-path reachability (APR, for short) predicate is a pair of a source set and a target set, which are subsets of an object set. APR predicates have been defined for abstract reduction systems (ARSs, for short) and then extended to logically constrained term rewrite systems (LCTRSs, for short) as pairs of constrained terms that represent sets of terms modeling configurations, states, etc. An APR predicate is said to be partially (or demonically) valid w.r.t. a rewrite system if every finite maximal reduction sequence of the system starting from any element in the source set includes an element in the target set. Partial validity of APR predicates w.r.t. ARSs is defined by means of two inference rules, which can be considered a proof system to construct (possibly infinite) derivation trees for partial validity. On the other hand, a proof system for LCTRSs consists of four inference rules, and thus there is a gap between the inference rules for ARSs and LCTRSs. In this paper, we revisit the framework for APR analysis and adapt it to verification of not only safety but also liveness properties. To this end, we first reformulate an abstract framework for partial validity w.r.t. ARSs so that there is a one-to-one correspondence between the inference rules for partial validity w.r.t. ARSs and LCTRSs. Secondly, we show how to apply APR analysis to safety verification. Thirdly, to apply APR analysis to liveness verification, we introduce a novel stronger validity of APR predicates, called total validity, which requires not only finite but also infinite execution paths to reach target sets. Finally, for a partially valid APR predicate with a cyclic-proof tree, we show a necessary and sufficient condition for the tree to ensure total validity.

ABSTRACT. We are interested in proving input-output properties of functions that handle infinite data such as streams or non-wellfounded trees. We provide a finitary refinement type system which is (sound and) complete for Scott-open properties defined in a fixpoint-like logic. Working on top of Abramsky's Domain Theory in Logical Form, we build from the well-known fact that the Scott domains interpreting recursive types are spectral spaces. The usual symmetry between Scott-open and compact-saturated sets is reflected in logical polarities: positive formulae allow for least fixpoints and define Scott-open sets, while negative formulae allow for greatest fixpoints and define compact-saturated sets. A realizability implication with the expected (contra)variance on polarities allows for non-trivial input-output properties to be formulated as positive formulae on function types.

ABSTRACT. In the field of static analysis of logic programs, the optimality of abstract operators is a valuable theoretical property, as it provides insight into the structure of abstract domains and the maximum precision that can be achieved. However, implementing optimal operators is often complex and may significantly impact performance, giving rise to a trade-off between precision and efficiency. We experimentally investigate this trade-off in the context of sharing and linearity analysis of logic programs. Our experiments build on previous work that proposed several optimal operators for unification and matching. We have implemented these abstract operators and the corresponding abstract domains within the PLAI analyzer, part of the CiaoPP preprocessor, and we report the impact of increasing operator precision on the accuracy and performance of the overall analysis.

ABSTRACT. In strongly-typed languages, types are verified at compile time, while dynamically typed languages, such as Prolog, perform type consistency checks entirely at run-time. Extending dynamic languages with assertions allows expressing both classical types and more general properties, providing high expressiveness, but at the cost of run-time overhead. Abstract interpretation allows safely approximating such program properties at compile time, which has been used to reduce the number of properties that require run-time checks, while still reporting unverified properties that can guide further static analyses, testing, or domain refinement. In this work, we first study how to selectively integrate the run-time semantics of assertion properties into a multivariant, top-down, goal-directed abstract interpretation algorithm. We then show how multiple inferred calling patterns can be exploited to reduce the number of properties that must be checked at run-time, thus minimizing the overhead. Finally, we report on an implementation of our approach in the Ciao system and provide performance results supporting that better results can be obtained than with the previously reported techniques.

ABSTRACT. Constraint-based causal discovery is notoriously brittle under finite samples: a small number of erroneous conditional-independence (CI) decisions can cascade into substantial structural errors. We argue that causal discovery under noisy CI evidence is fundamentally a problem of defeasible reasoning rather than pure constraint satisfaction. We introduce Quantitative Argumentation for Causal Discovery, a semantics-driven framework that evaluates edge hypotheses by dialectically aggregating uncertain CI evidence. Instead of treating CI test outcomes as hard constraints, Our method models them as defeasible independence arguments whose strengths are derived from statistical tests. Conflicts are resolved through connectivity-mediated structural undercuts, in which short-range graph structure modulates the impact of local CI claims, yielding a fixed-point acceptability labelling over candidate adjacencies. Across standard benchmark Bayesian networks, our method improves skeleton fidelity and interventional reliability compared with classical constraint-based, hybrid and argumentation-based methods. These results illustrate how quantitative argumentation semantics can serve as a computational mechanism for statistical causal discovery under inconsistent CI evidence.

ABSTRACT. Gradual semantics for weighted bipolar argumentation provide a principled framework for modelling argumentative reasoning, yet existing approaches remain mostly scalar, fixed, and weakly grounded in empirical data. We introduce learnable multi-attribute gradual semantics for persuasion prediction in argumentative debates. Our approach builds a dataset of 600 textual debates converted into multi-attribute argumentation graphs enriched with multi-dimensional features on nodes and relations. Building on this representation, we propose learnable aggregation operators that distinguish intrinsic quality from persuasive strategy dimensions. Experiments show that the learned semantics achieve competitive performance with neural and LLM-based baselines while preserving interpretability.

ABSTRACT. Understanding how policy is debated and justified in parliament is a fundamental aspect of the democratic process. However, the volume and complexity of such debates mean that outside audiences struggle to engage. Meanwhile, Large Language Models (LLMs) have been shown to enable automated summarisation at scale. While summaries of debates can make parliamentary procedures more accessible, evaluating whether these summaries faithfully communicate argumentative content remains challenging. Existing automated summarisation metrics have been shown to correlate poorly with human judgements of consistency (i.e., faithfulness or alignment between summary and source). In this work, we propose a formal framework for evaluating parliamentary debate summaries that grounds argument structures in the contested proposals up for debate. Our novel approach, driven by computational argumentation, focuses the evaluation on formal properties concerning the faithful preservation of the reasoning presented to justify or oppose policy outcomes. We demonstrate our methods using a case-study of debates from the European Parliament and associated LLM-driven summaries.

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. ABA Learning is a recent approach for obtaining Assumption-based Argumentation (ABA) frameworks by reasoning with transformation rules from background knowledge and positive/negative examples of concepts of interest. ABA Learning relies on credulous reasoning under a specific semantic notion of extensions for ABA, namely that of stable extensions. In this paper, we newly frame the problem in terms of credulous reasoning under any semantic notion of extensions for ABA. Focusing on admissible, com- plete, grounded, preferred as well as stable extensions, we present X-ABALearn, a novel parametric algorithm (with X any ABA semantics) based on variants of the transformation rules of ABA Learning and an implementation thereof in Answer Set Programming. Finally, we explore the use of (our implementation of) X-ABALearn on several learning problems, including tabular data and beyond.

ABSTRACT. As reinforcement learning (RL) agents are deployed in increasingly complex environments, ensuring that their behavior complies with the user's needs has become a central challenge in eXplainable RL (XRL). An agent's policy may solve a given problem, but some of its choices can seem counter-intuitive or surprising to the user, who may have wished to see the agent accomplish its goal in a different way, and may wonder: what if the agent acted with a different intent in mind? Scenarios that answer this question are called counterfactual policies. In this work, we propose a framework that allows the user to request these alternative policies by formulating preferences about the behavior of the agent. These preferences are expressed in Linear Temporal Logic on finite traces (LTL_f), a formal yet intuitive language that allows reasoning about deterministic sequences of actions. We synthesize the corresponding counterfactual policies using a multi-objective reinforcement learning algorithm, which produces a diverse set of alternative strategies balancing the agent's original policy with the one envisioned by the user. By comparing these strategies and highlighting their key differences, our framework sheds light on the rationale behind the agent's decisions. Experimental trials show that such a set of policies can be synthesized in reasonable time.

ABSTRACT. Time-critical systems must meet stringent real-time constraints, where correctness depends not only on the order of events but also on their timing. Temporal logics provide a well-established formalism for expressing such requirements, ranging from simple deadlines to interval-bounded obligations. Metric Interval Temporal Logic (MITL) has been used successfully, particularly under the signal-based interpretation, where executions are modeled as Boolean signals. In this context, both Boolean and quantitative semantics have been explored. Specifically, time robustness quantifies tolerance to temporal shifts of signals, either synchronously (all signals shifted together) or asynchronously (each shifted independently). These notions have proven valuable for monitoring, verification, and control synthesis of continuous and hybrid systems. In contrast, in the point-based interpretation, where executions are described as timestamped event sequences, the quantitative semantics of MITL have only been marginally investigated, and the notion of time robustness has not been systematically studied. This paper addresses this gap by introducing a new concept of time robustness for MITL over point-based semantics and demonstrating how this measure can serve as a resilience index against timing perturbations. The proposed robustness is implemented and validated through two case studies.

ABSTRACT. Multi-agent systems involve complex, multilevel interactions between autonomous agents. To contain the complexity, but also help a human modeler, hierarchical models can be used to describe the possible courses of action. In that case, the top-level transition system specifies the behavior of the system at a certain level of abstraction, while some nodes are refined via lower-level models. Hierarchical system specifications were originally studied for reactive processes and their temporal properties. In this short paper, we extend the framework to game-like interaction between proactive agents. To this end, we propose \emph{hierarchical concurrent game models} and define their execution semantic by their unfolding to ordinary, flat concurrent game models. We also make the first steps towards verification of strategic abilities, expressed in alternating-time temporal logic ATL, for hierarchical concurrent games.

ABSTRACT. The simple temporal problem (STP) and its generalization allowing disjunctive constraints (DTP) are some of the most influential reasoning formalisms for representing temporal information in AI. We study the problem of resolving inconsistency of data encoded in the DTP, i.e. given a DTP instance, find the minimum number of constraints to remove to make it satisfiable. While this problem is NP-hard in general, it is reasonable to assume that the amount of erroneous data will be small in practical instances. We therefore study the parameterized complexity of this problem parameterized by the number of constraints to be removed to achieve satisfiability. The expressive power of the formalism and the computational complexity of the problem varies depending on the constraint language, i.e. the types of allowed constraints. Dabrowski et al. (AAAI-2022) achieved full P/NP-hard and FPT/W[1]-hard dichotomies for all STP constraint languages. Our main result is an extension of this result to the more expressive binary DTP languages. The starting point is a classification result for discrete temporal CSPs by Bodirsky et al. (JACM, 2018). Using polymorphisms and other tools from logic and algebra, we provide a fine-grained understanding of the complexity of binary DTP languages. Among the tractable cases, we design an FPT algorithm for the language allowing successor constraints and their negations; this generalizes prominent parameterized separation and transversal problems on graphs, such as Edge Multicut and Group Feedback Edge Set (for the additive group of integers) which have previously been solved by disparate tools.

ABSTRACT. Automated logic circuit design enhances chip performance, energy efficiency, and reliability, with applications in model-checking, reactive synthesis, and hyperproperty verification. AIGER circuits are a standard format for these domains, used in hardware model-checking, synthesis competitions such as Syntcomp, symbolic synthesis algorithms, and the verification of security properties in neural networks and safety-critical systems. Traditionally, AIGER circuits are generated from Linear Temporal Logic (LTL) specifications through complex pipelines, such as translating LTL to SMV or to automata and then to AIGER. These pipelines guarantee functional equivalence but produce large circuits with auto-generated labels that obscure the specification’s meaning. In applications like symbolic reactive synthesis, model-checking, and neural network verification, understanding latches and outputs is critical for debugging and tool improvement. In this tool paper, we introduce AIGLE, a novel tool that generates compact AIGER circuits directly from LTL[X] or Past-LTL specifications. Our approach uses linear-size translation from LTL[X] to Past-LTL, which produces highly legible circuits. Compared to tools like py-aiger, our tool reduces gate counts-—often by thousands-— improving readability and synthesis speed. Our empirical evaluation demonstrates smaller, more understandable circuits and faster synthesis, offering a scalable, engineer-friendly solution for formal methods applications.

ABSTRACT. The expressive power of Graph Neural Networks (GNNs) is often analysed via correspondence to the Weisfeiler-Leman (WL) algorithm and fragments of first-order logic. Standard GNNs are limited to performing aggregation over immediate neighbourhoods or over global read-outs. To increase their expressivity, recent attempts have been made to incorporate substructural information (e.g. cycle counts and subgraph properties). In this paper, we formalize this architectural trend by introducing Template GNNs (T -GNNs), a generalized framework where node features are updated by aggregating over valid template embeddings from a specified set of graph templates. We propose a corresponding logic, Graded template-modal logic (GML(T )), and generalized notions of template-based bisimulation and WL algorithm. We establish an equivalence between the expressive power of T -GNNs and GML(T ), and provide a unifying approach for analysing GNN expressivity: we show how standard AC-GNNs and its recent variants such as AC+-GNNs can be interpreted as instantiations of T -GNNs.

ABSTRACT. We characterize the computational power of recurrent graph neural networks (GNNs) in terms of arithmetic circuits over the real numbers. Our networks are not restricted to aggregate-combine GNNs or other particular types. Generalizing similar notions from the literature, we introduce the model of recurrent arithmetic circuits, which can be seen as arithmetic analogues of sequential or logical circuits. These circuits utilize so-called memory gates which are used to store data between iterations of the recurrent circuit. While (recurrent) GNNs work on labeled graphs, we construct arithmetic circuits that obtain encoded labeled graphs as real valued tuples and then compute the same function. For the other direction we construct recurrent GNNs which are able to simulate the computations of recurrent circuits. These GNNs are given the circuit-input as initial feature vectors and then, after the GNN-computation, have the circuit-output among the feature vectors of its nodes. In this way we establish an exact correspondence between the expressivity of recurrent GNNs and recurrent arithmetic circuits operating over real numbers.

ABSTRACT. The counting power of Message Passing Neural Networks (MPNN) has been the subject of many recent papers, showing that they express logic that can count up to a threshold or more generally satisfy a linear arithmetic constraint. In this paper, we study the counting capability of MPNN beyond linear arithmetic, primarily utilising local and global mean aggregations. In particular, our goal is to tease out conditions required to express the extensions of graded modal logic with polynomial counting constraints. We show that global polynomial counting constraints in node-labelled graphs can be checked using mean MPNN. Allowing local constraints is also possible, if we consider formulas with no nested modalities and additionally either (i) permit either sum/max aggregations, or (ii) only restrict to regular graphs. We also show how formulas with nested modalities can be captured by mean MPNN over graphs with tree-like structures.

ABSTRACT. In recent years, there has been a growing interest in study- ing the expressive power of graph neural networks (GNNs) by linking them to logical languages. This line of study was started by a key finding by Barceló et al. (2020), who proved that graded modal logic (or the guarded part of the logic C2) characterises the logical expressiveness of aggregate-combine GNNs. They left a “challenging open problem” asking if C2 characterises the logical expressive- ness of aggregate-combine-readout GNNs. This question has stayed open for five years. In this paper, we solve this open problem by showing that aggregate-combine-readout GNNs can express logical classifiers beyond C2.

ABSTRACT. We analyse how the choice of the aggregation function in graph neural networks (GNNs) affects their uniform expressiveness. Allowing arbitrary aggregation yields expressiveness of infinitary graded modal logic. Expressiveness strictly decreases when moving from arbitrary aggregation to sum, from sum to mean, and from mean to max. When GNNs are equipped with global readout and arbitrary aggregation, they have the expressiveness of infinitary C2 and, surprisingly, restricting aggregation to sum does not decrease their expressiveness. In the presence of readout GNNs with mean aggregation are strictly less expressive than with sum and those with sum are strictly less expressive than with max. In the case of simple GNNs, where combination functions are linear transformations followed by a non-linearity and the classification function is a threshold function, the landscape differs. In particular GNNs with sum aggregation and readout no longer have the expressiveness of full infinitary C2. These results provide us with new insights on the expressiveness of GNNs, showing that even subtle architectural modifications can significantly influence their expressive power.

ABSTRACT. Knowledge compilation transforms logical theories into circuit representations that support efficient reasoning. We study this problem for propositional groundings of FO2, the two-variable fragment of first-order logic over finite domains. Given an FO2 sentence and a domain of size n, its grounding yields a propositional theory over ground atoms. We ask whether such theories admit compact DNNF-based representations and whether these can be constructed efficiently, both with respect to the domain size n for a fixed sentence. We show first that compact compilation is impossible in general: there exists a FO2 sentence whose grounding over a domain of size n requires DNNF size $2^{\Omega(n)}$. On the positive side, we develop a two-stage d-DNNF compiler that exploits the symmetries inherent in the propositional groundings of FO2 sentences. It branches on unary and binary types rather than individual ground atoms, in a similar spirit to lifted inferences for probabilistic relational models. Moreover, it optimizes the compilation process by caching and reusing compiled subcircuits by identifying residual subproblems that are equivalent with respect to future extensions. Experiments on several benchmark families show that our approach generally yields substantially smaller circuits than straightforward grounding-and-then-compiling baselines.

ABSTRACT. The well-founded semantics (WFS) for logic programs results in a unique three-valued interpretation and serves as an efficient basis for skeptical reasoning, but lacks built-in mechanisms for objective choice and case-based reasoning, limiting its expressiveness for decision problems. Propositional SAT solvers excel at the latter but, unlike WFS, do not naturally admit reasoning under uncertainty or encoding transitive closure properties. We present an integration of an objective choice operator into WFS that preserves the semantics' suitability for scalable, partial-information reasoning and show that this choice operator can be materialized by a SAT solver while propagating the consequences of choices through an extension of the well-established alternating fixed-point algorithm for WFS with conflicts being propagated back to the SAT solver. We illustrate the approach in a setting for reasoning about actions under uncertainty, and we extend the framework to support theory constraints, such as difference logic constraints for modeling actions with duration. From a propositional perspective, our semantics gracefully captures semantically unassigned atoms and constraints. We study syntactic decomposition techniques for logic programs with choices, benefiting both grounding and solving. Finally, we relate our semantics to answer sets, and demonstrate that classical propositional satisfiability can not only be embedded in our framework, but can now also be extended with reasoning over transitive closures.

ABSTRACT. Discrete variables are common in many applications, such as probabilistic reasoning, planning and explainable AI. When symbolic reasoning techniques are brought in to bear on these applications, a standard technique for handling discrete variables is to binarize them into Boolean variables to allow the use of Boolean computational machinery such as SAT solvers. This technique can face both computational and semantical challenges though. In this work, we develop a native SAT solver for discrete logic, which is a direct extension of Boolean logic in which variables can take arbitrary values. Our proposed solver has a similar design to Boolean SAT solvers, with ingredients such as unit resolution and clause learning but ones that operate natively on discrete variables. We illustrate the merits of the developed SAT solver by comparing it empirically to CSP solvers applied to discrete CNFs, to Boolean SAT solver applied to binarized CNFs, and to some hybrid solvers.

ABSTRACT. Because CDCL produces proofs in the Resolution proof system, problems provably hard for Resolution are also provably hard for CDCL. Exponentially shorter proofs can sometimes be found using stronger proof systems such as $\text{Res}(\oplus)$, a generalization of Resolution to XNF formulas, whose constraints are disjunctions of parity equations (``linear clauses'') such as $(x \oplus y) \lor \lnot (y \oplus z)$. While some modern solvers like CryptoMiniSAT reason on Boolean clauses with separate parity equations, reasoning about more general linear clauses is less explored. We present $\text{CDCL}(\oplus)$, a generalization of CDCL to XNF formulas, and prove a bidirectional connection with $\text{Res}(\oplus)$: $\text{CDCL}(\oplus)$ not only produces $\text{Res}(\oplus)$ proofs, but also polynomially simulates $\text{Res}(\oplus)$ given nondeterministic decisions and restarts, mirroring the classical relationship between CDCL and Resolution. Our key technical tool is a new set of inference rules for $\text{Res}(\oplus)$ that helps us translate Resolution-based subroutines such as 1-UIP clause learning. Altogether, $\text{CDCL}(\oplus)$'s parity reasoning includes branching on arbitrary parity equations, linear-algebraic reasoning during unit propagation, and learning linear clauses through conflict analysis. We provide a proof-of-concept implementation of $\text{CDCL}(\oplus)$ called \textsf{Xorcle}, which includes adaptations of existing CDCL heuristics to XNF formulas and an extension of LRUP proof logging that we call $\text{LRUP}(\oplus)$. On a selected suite of benchmarks focusing on native XNF formulas, \textsf{Xorcle} outperforms existing solvers such as Kissat and CryptoMiniSAT. Additionally, on Tseitin formulas written in CNF, even without preprocessing, \textsf{Xorcle}'s running time appears to scale nearly polynomially.

ABSTRACT. Streamliner constraints reduce the search space of combinatorial problems by ruling out portions of the solution space. We adapt the StreamLLM approach, which uses Large Language Models to generate streamliners for Constraint Programming, to Answer Set Programming (ASP). Given an ASP encoding and a few small training instances, we prompt multiple LLMs to propose candidate constraints. Candidates that cause syntax errors render satisfiable instances unsatisfiable, or degrade performance on all training instances are discarded. The surviving streamliners are deployed in a parallel portfolio alongside the original encoding, ensuring correctness even if a streamliner is unsound. On three ASP Competition benchmarks (Partner Units Problem, Sokoban, Towers of Hanoi), the portfolio achieves speedups of up to 4-5x over the original encoding. Different LLMs produce semantically diverse constraints, not mere syntactic variations, indicating that the approach captures genuine problem structure.

ABSTRACT. The growing demand for Urban Air Mobility (UAM) introduces significant challenges in airspace management, particularly within densely populated metropolitan regions. As the number of aerial vehicles---such as drones, air taxis, and helicopters---continues to rise, so does the risk of mid-air collisions and conflicts with existing air traffic and obstacles. Ensuring safe and efficient UAM operations requires robust strategic deconfliction mechanisms. We propose an Answer Set Programming (ASP) based approach for strategic deconfliction, focusing on time synchronization and route optimization for conflict-free flight plans. The solution is benchmarked against Constraint Programming (CP), emphasizing scalability and resource use. Results show ASP offers faster execution and better scalability for small to medium cases, while CP maintains stable memory but degrades with complexity.

ABSTRACT. This article presents ASPIC, a new proof-of-concept library that converts extended syntax ASP-Core-2 programs to Picat predicates that can be solved right away with the integrated Picat SAT solver, or embedded in larger Picat programs (``ASP in Picat''), and that can in turn make use of various Picat predicates and functions (``Picat in ASP''). The first tests prove good compatibility with clingo (when the special Picat features are not used). With the embedded Picat, it touches the application field of clingcon as well, by being able to efficiently model with both ASP atoms and with finite domain variables, but goes beyond that by being able to model also non-linear constraints.

ABSTRACT. Answer Set Programming (ASP) is a declarative programming language used for modeling and solving complex combinatorial problems. It has been successfully applied to a number of different real-world problems. However, learning its usage can prove challenging as the declarative language, from a conceptual perspective, differs substantially from imperative programming, and programs are not required to adhere to any particular structure, offering arguably almost too much freedom for a beginner. Recently, a new methodology called Easy Answer Set Programming (Easy ASP) has been introduced that aims to aid in this learning process by focussing on a well-defined fragment of the ASP language and introducing additional structure to the programs. However, while this methodology can indeed be employed, to the best of our knowledge, no tool integrates its features currently. In this paper, we present EZASP, a Visual Studio Code extension designed to support the development of ASP programs following the Easy ASP methodology. It covers and extends the language fragment of Easy ASP and provides the user with warnings in the case of deviations from the methodology as well as the possibility to automatically reorder the program. Complementarily, it also adds syntax error highlighting, including detection of non-safe variables directly while editing, and configurability, as all features can be optionally disabled. A small user study in the context of university teaching suggests that these features are benefitial for both new and experienced users.

ABSTRACT. An effective examination and test schedule for patients plays a crucial role in hospital resource management. In this work, we formulate a new reactive patient-flow scheduling problem in multi-department hospitals where walk-in patients arrive over time and each patient requires multiple examinations per visit. Upon each arrival, the scheduler computes a feasible examination pathway---both the sequence of examinations and the room assignment---for the incoming patient only, while previously scheduled assignments remain fixed. This process is subject to medical precedence constraints and room capacity limitations. We model the problem declaratively in Answer Set Programming (ASP) with clingo, and optimize a two-part cost: travel time between consecutive examination locations and queue-induced waiting time, weighted by the duration of the upcoming examination. To assess robustness under stochastic service times, we propose a Discrete-Event Simulation (DES) evaluation layer and a baseline greedy policy for comparison. On large-scale synthetic datasets across various capacity regimes and patient loads, the ASP approach reduces median stay time and increases the proportion of zero-wait patients compared to DES-based baselines. These improvements are most pronounced under heavy load, while the approach still outperforms baselines across all capacity settings, with smaller gains at higher capacities.

ABSTRACT. Grounding, the translation of high-level models into equivalent quantifier-free formulas, is a crucial step in declarative solving, yet it has so far escaped the proof-logging revolution. When this grounding step is not certified, there is no way of knowing that the obtained solutions actually correspond to the original problem specification, resulting in a trust gap. In this paper, we close the trust gap between the user's high-level specification and the solver's low-level input by introducing a novel certifying grounding framework for first-order logic model expansion (FOX) over finite domains. We present CertiFOX, a certified grounding framework consisting of: (1) a proof format for grounding derivations, (2) GroundFOX, a certifying grounder operating on theories in Grounding Normal Form (GNF)—a new normal form designed for compact, domain-aware grounding—and (3) CheckFOX, an independent proof checker. Our approach guarantees that the grounder's output is equivalent to the input specification, setting the stage for trustworthy end-to-end certified solving pipelines for declarative languages. Experimental evaluation confirms that CertiFOX is a feasible approach. The GroundFOX grounder is competitive with other grounders, and proof checking with CheckFOX remains within a constant factor of grounding time.

ABSTRACT. We consider the problem of implementing deontic modal logic. We show how (deontic) modal operators can be elegantly and directly expressed using default negation (negation-as-failure) and strong negation present in answer set programming (ASP). We propose using global constraints of ASP to represent obligations, prohibitions, and permissions in deontic modal logic. We show that our proposed representation results in the various decades-old paradoxes of deontic modal logic being simply and elegantly resolved. Our method also serves as a means for modeling conditional obligations and conditional prohibitions in knowledge representation.

ABSTRACT. Abstract Interpretation infers and verifies program properties by over-approximating program semantics. It has been highly successful for (Constraint) Logic Programming, enabling the analysis of determinism, types, aliasing, costs, and its application in verification and program optimization. However, Abstract Interpretation has not yet been studied in the context of Goal Directed Answer Set Programming (ASP). In this work we take a first step in this direction. We present a top-down algorithm based in the PLAI fixpoint, implemented in the abstract interpreter of the Ciao Prolog Preprocessor, to perform abstract interpretation of goal-directed ASP. We also introduce the Shared-Constraints abstract domain, designed to capture potential relations among variables induced by constraints. Finally, we study the practicality of the approach in s(CASP) through three applications: detection of false odd loops over negation, efficient forall evaluation enabled by the Shared-Constraints domain, and abstract specialization (including the simplification of required global constraints). Our results show that compile-time static analysis can improve the evaluation of goal-directed ASP programs.

ABSTRACT. A lazy program interpreter postpones computation until the result is actually needed. This is typically more efficient than an eager (or call-by-value) interpreter, but a concern is that the semantics is not generally preserved. We propose a new semantic analysis of lazy evaluation that relies on a subtle combination of name generation and read-only state. For a language with arbitrary algebraic effects and data types, we derive conditions under which lazy evaluation computes the same result as the eager semantics. The semantic model suggests better intermediate representations of sum and product types in a lazy interpreter, along with equations that justify further optimizations. To illustrate we sketch an implementation in OCaml. Our motivation is practical: the origin of this work is a real-world application of probabilistic programming, in which large algebraic data types cause significant performance issues with a call-by-value interpreter. Our lazy semantics justifies better optimized representations, and provides principled foundations for other methods involving laziness in probabilistic programming.

ABSTRACT. We introduce a dialect of the asynchronous $\pi$-calculus, called AW$\pi$, in which (1) an input name may be owned, at any time, by at most one process; (2) each name has either only the input or only the output capability. As a result, special processes called wires (aka forwarders, that is, processes that receive values at one name and re-transmit) behaves as substitutions when composed with any AW$\pi$ process.Thus AW$\pi$ naturally yields a category, whose morphisms are AW$\pi$ processes (modulo the reference behavioural equivalence, barbed congruence) and whose objects are types; and where wires act as identity morphisms. We show that the category of processes can be further organized into (sub)categories with the structures needed for the interpretation of common higher-order language features in the literature by drawing on insights from game semantics; notably we construct a relative Seely category, the categorical structure that concurrent game semantics has. At the same time, AW$\pi$ follows the tradition of ordinary $\pi$-calculi in that expressiveness is preserved and the operational and algebraic theory are developed in a similar manner, notwithstanding substantial technical differences in their development and proofs.In short, the goal of AW$\pi$ is to remain faithful to the operational and algebraic tradition of the $\pi$-calculi while connecting to the tradition of denotational models for programming languages.

ABSTRACT. Consider a 4-player version of Matching Pennies where a team of three players competes against the Devil. Each player simultaneously says “Heads” or “Tails”. The team wins if all four choices match; otherwise the Devil wins. If all team players randomise independently, they win with probability 1/8; if all players share a common source of randomness, they win with probability 1/2. What happens when _each pair_ of team players shares a source of randomness? Can the team do better than win with probability 1/4? The surprising (and nontrivial) answer is yes! We introduce Dicey Games, a formal framework motivated by the study of distributed systems with shared sources of randomness (of which the above example is a specific instance). We characterise the existence, representation and computational complexity of optimal strategies in Dicey Games, and we study the problem of allocating limited sources of randomness optimally within a team.

ABSTRACT. We consider multi-dimensional payoff functions in partially observable Markov decision processes. We study the structure of the set of expected payoff vectors of all strategies (policies) and study what kind are needed to achieve a given expected payoff vector. In general, pure strategies (i.e., not resorting to randomisation) do not suffice for this problem. We prove that for any payoff for which the expectation is well-defined under all strategies, it is sufficient to mix (i.e., randomly select a pure strategy at the start of a play and committing to it for the rest of the play) finitely many pure strategies to approximate any expected payoff vector up to any precision. Furthermore, for any payoff for which the expected payoff is finite under all strategies, any expected payoff can be obtained exactly by mixing finitely many strategies.