ABSTRACT. Proof by induction is common-place in mathematics, logic, formal verification, cybersecurity, and many more areas. This talk overviews recent progress in automating inductive reasoning in saturation-based first-order theorem proving. We show how to formalize applications of induction in the saturation process, without bringing drastic changes into the overall framework of first-order proving. We also synthesize code that satisfies a given (inductive) logical specification, while proving the specification in saturation with induction.

ABSTRACT. Most implementations of sampling algorithms for continuous distributions use floating-point numbers, which introduce round-off errors and approximations. These errors can be difficult to analyze, and can cause security issues when used in algorithms for differential privacy. An alternative is to use exact sampling algorithms based on computable reals, which can lazily generate the digits of a continuous sample to arbitrary precision. However, these algorithms are intricate, and implementing and using them involves a combination of semantically challenging language features, such as probabilistic choice, higher-order functions, and dynamically-allocated mutable state. This paper describes Continuous-Eris, a higher-order separation logic for verifying the correctness of exact sampling algorithms for computable distributions. To demonstrate Continuous-Eris, we have verified the correctness of computable samplers for the uniform, Gaussian, and Laplace distributions, as well as a library for exact real arithmetic for working with generated samples. All of the results in this paper have been verified in the Rocq proof assistant.

ABSTRACT. We introduce a general methodology for the construction of sound and complete proof rules for the almost-sure and quantitative acceptance of reactivity properties on time-homogeneous Markov chains with general state spaces. Reactivity captures $\omega$-regular properties and subsumes linear temporal logic. Our core technical result establishes that every reactivity property admits decomposition into multiple obligations of almost-sure termination into absorbing regions, and that appropriate absorbing regions always exist for time-homogeneous Markov chains. This enables the extension of every complete proof rule for almost-sure termination into a proof rule for reactivity that is complete in the almost-sure case, and complete up to arbitrary $\epsilon$-approximation in the quantitative case. We apply our new methodology to recent results on sound and complete supermartingale certificates for almost-sure termination on countably infinite state spaces alongside standard results on quantitative safety. As a result, we obtain the first sound and complete supermartingale certificates for almost-sure $\omega$-regular properties and the first sound and $\epsilon$-complete supermartingale certificates for quantitative $\omega$-regular properties on time-homogeneous Markov chains with countably infinite state spaces.

ABSTRACT. The problem of determining whether a probabilistic program terminates almost surely (i.e.~with probability one) is undecidable, and actually Pi^0_2-complete. For this reason, a growing literature has explored classes of programs for which this and related problems can be shown (semi-)decidable. In this work we consider the termination problem for the language of Probabilistic Higher-Order Recursion Schemes (PHORS). Using the weighted relational semantics of linear logic, we translate this problem into the computation of suitable generating functions associated with the program interpreted. This way, we establish the decidability of almost sure termination for a class of programs that extends Li et al.'s affine PHORS via a type discipline with bounded exponentials. To achieve this, we show that the generating functions for such programs are always algebraic, that is, solutions of polynomial equations, yielding an effective method to answer the termination problem.

ABSTRACT. Quantitative logic reasons about the degree to which formulas are satisfied. This paper studies the fundamental reasoning principles of higher-order quantitative logic and their application to reasoning about probabilistic programs and processes. We construct an affine calculus for 1-bounded complete metric spaces and the monad for probability measures equipped with the Kantorovich distance. The calculus includes a form of guarded recursion interpreted via Banach's fixed point theorem, useful, e.g., for recursive programming with processes. We then define an affine higher-order quantitative logic for reasoning about terms of our calculus. The logic includes novel principles for guarded recursion and induction over probability measures and natural numbers. We illustrate the expressivity of the logic by a sequence of case studies: Proving upper limits on bisimilarity distances of Markov processes, showing convergence of a temporal learning algorithm and of a random walk using a coupling argument.

ABSTRACT. Monadic stability generalizes many tameness notions from structural graph theory such as planarity, bounded degree, bounded tree-width, and nowhere density. The \emph{sparsification conjecture} predicts that the (possibly dense) monadically stable graph classes are exactly those that can be logically encoded by first-order (FO) transductions in the (always sparse) nowhere dense classes. So far this conjecture has been verified for several special cases, such as for classes of bounded shrub-depth, and for the monadically stable fragments of bounded (linear) clique-width, twin-width, and merge-width. In this work we propose the \emph{existential positive sparsification conjecture}, predicting that the more restricted co-matching-free, monadically stable classes are exactly those that can be transduced from nowhere dense classes using only existential positive FO formulas. While the general conjecture remains open, we verify its truth for all known special cases of the original conjecture. Even stronger, we find the sparse preimages as subgraphs of the dense input graphs. As a key ingredient, we introduce a new combinatorial operation, called \emph{subflip}, that arises as the natural co-matching-free analog of the flip operation, which is a central tool in the characterization of monadic stability. Using subflips, we characterize the co-matching-free fragment of monadic stability by appropriate strengthenings of the known flip-flatness and flipper game characterizations for monadic stability. In an attempt to generalize our results to the more expressive MSO logic, we discover (rediscover?) that on relational structures (existential) positive MSO has the same expressive power as (existential) positive FO.

ABSTRACT. We introduce a new logic for describing properties of graphs, which we call low rank MSO. This is the fragment of monadic second-order logic in which set quantification is restricted to vertex sets of bounded cutrank. We prove the following statements about the expressive power of low rank MSO. * Over any class of graphs that is weakly sparse, low rank MSO has the same expressive power as separator logic. This equivalence does not hold over all graphs. * Over any class of graphs that has bounded VC dimension, low rank MSO has the same expressive power as flip-connectivity logic. This equivalence does not hold over all graphs. * Over all graphs, low rank MSO has the same expressive power as flip-reachability logic. Here, separator logic is an extension of first-order logic by basic predicates for checking connectivity, which was proposed by Bojańczyk [ArXiv 2107.13953] and by Schirrmacher, Siebertz, and Vigny [ACM ToCL 2023]. Flip-connectivity logic and flip-reachability logic are analogues of separator logic suited for non-sparse graphs, which we propose in this work. In particular, the last statement above implies that every property of undirected graphs expressible in low rank MSO can be decided in polynomial time.

ABSTRACT. Algorithmic meta-theorems explain the tractability of large classes of computational problems by linking logical expressibility with structural graph properties. While extensions of first-order logic such as FO+dp admit efficient model checking on graph classes excluding a fixed topological minor, comparable results for richer fragments of CMSO were previously unknown. We further develop the framework of Sau, Stamoulis, and Thilikos [SODA 2025] for fragmenting CMSO via annotated graph parameters, which restrict set quantification to vertex sets satisfying bounded structural conditions. Following this approach, we identify a fragment of CMSO namely the one defined by allowing quantification only over sets having what we call low monodimensionality, that generalizes several previously-known logics and we show that model checking for this fragment, enhanced with the disjoint-paths predicate, is fixed-parameter tractable on topological-minor-free graph classes. Such classes essentially delimit the tractability for this logic on subgraph-closed classes. As a consequence, our results lift several known algorithmic meta-theorems beyond first-order logic to the topological-minor-free setting.

ABSTRACT. We study classes of graphs with bounded clique-width that are well-quasi-ordered by the induced subgraph relation, in the presence of labels on the vertices. We prove that, given a finite presentation of a class of graphs, one can decide whether the class is labelled-well-quasi-ordered. This solves an open problem raised by Daligault, Rao and Thomassé in 2010, and Lopez in 2025. From our proof techniques, we also derive (restricted versions of) conjectures of Pouzet regarding well-quasi-ordering of graphs under the induces subgraph relation. Finally, we provide a structural characterization of those classes as those that are of bounded clique-width and do not existentially transduce the class of all finite paths.

ABSTRACT. Several proof systems for MaxSAT have been proposed in the literature, including MaxSAT resolution and, more recently, systems based on polynomial calculus and tableaux. Although these systems are sound and complete and have varying strengths, they fail to capture the specific inferential strategies used by practical MaxSAT solvers, particularly those used in core-guided approaches. As a result, a formula that is hard to prove in these proof systems may not be hard for a solver, and vice versa. In this paper, we describe a new proof system for MaxSAT, the Comparator Calculus (CC), which models the inferential strategies used in core-guided MaxSAT solvers. Inspired by this formalism, we introduce two new MaxSAT algorithms: a core-guided one (Simple) and one not core-guided (CSat), which uses heuristics to construct new soft formulas and calls a SAT solver on a unique soft formula. We also define a hybrid mechanism (core-guided CSat) that uses cores to guide the heuristics. We evaluate and compare our solvers with OLL on instances from the MaxSAT evaluation 2024, random 2-CNFs, and PHP formulas. Experimental results suggest that, in general, the performance of the distinct MaxSAT solvers depends on the structure of the instances. On the set of industrial instances of the MaxSAT Evaluation 2024, Simple performs better than the others (including OLL).

ABSTRACT. We describe the Scuttlesystem for multi-objective combinatorial optimization. Scuttle accepts multi-objective instances where the constraints are declared either as propositional clauses or pseudo-Boolean constraints, and implements a range of multi-objective maximum satisfiability algorithms (including ones for enumerating all Pareto-optimal and leximax-optimal solutions). Pseudo-Boolean constraints are translated to clauses, allowing for applying any of the implemented algorithms on both the clausal and the pseudo-Boolean level. Scuttle also includes tightly integrated preprocessing (both core boosting and liftings of SAT preprocessing techniques) for multi-objective instances and can provide proof certificates for selected algorithms.

ABSTRACT. Maximum Satisfiability (MaxSAT) has become a key engine for solving complex discrete optimization problems. However, developing high-performance, iterative workflows remains cumbersome due to fragmented, low level solver APIs. To address this, we present Hermax, a Python library and modelling compiler for MaxSAT. At its core, Hermax provides an IPAMIR compliant interface that abstracts incremental and non-incremental solvers under a single API. Hermax also introduces a novel, eager-evaluation compiler inspired by Constraint Programming. This compiler allows users to formulate problems using high level abstractions while actively bypassing traditional pseudo-Boolean encoders when possible. Together, these features enable rapid prototyping and production-level optimization directly from Python in many different environments.

ABSTRACT. We describe HitPBO 1.0, a from-scratch open-source C++ implementation of the implicit hitting set (IHS) approach to pseudo-Boolean optimization. Compared to earlier implementations, HitPBO adds a range of functionalities and search techniques, certificates, and support for various alternative solvers within IHS. We give an overview of the solver's architecture and its functionalities.

ABSTRACT. While Maximum Satisfiability (MaxSAT) has been successfully applied to a wide range of combinatorial optimization problems, the encoding of Nonlinear Integer Programming (NLIP) with polynomial functions into MaxSAT has so far only been studied at a theoretical level. In this paper, we introduce NLIPSat, the first tool capable of encoding bounded polynomial NLIP instances directly into Maximum Satisfiability. Building upon recent MaxSAT formulations for polynomial NLIP proposed in [24], NLIPSat enables the encoding of polynomial non-linear objective functions as weighted soft clauses and also supports the encoding of hard non-linear polynomial constraints within a polynomial setting. Extensive experiments on different benchmarks show that NLIPSat outperforms the state-of-the-art SMT solver Z3 by a wide margin.

ABSTRACT. We introduce a new presentation of the intersection type discipline in which typing judgments derive vectors of types rather than single types. The system uses binary relations to control the flow of information between coordinates of these vectors. We refer to this presentation as system R. The maximal length of type vectors assigned to variables serves as a reasonable notion of dimension for system R, which allows for a natural stratification into fragments of bounded dimension. The present system lies strictly between two known bounded-dimensional systems: the multiset-dimensional system, for which inhabitation is EXPSPACE-complete, and the set-dimensional system, for which inhabitation is undecidable. Our main result is that inhabitation in bounded system R is decidable in 2-EXPTIME, while for each fixed dimension, inhabitation is decidable in EXPTIME. This result is based on a subformula property restricting the inhabitant search space. Unlike in traditional intersection type systems, the proof of the subformula property requires careful treatment of the additional information flow management capabilities. Finally, we argue that system R and its stratification is a valid presentation of the intersection type discipline. First, by proving the subject reduction property for system R in each bounded dimension, and second, by establishing a correspondence with the classical intersection type system of Barendregt, Coppo, and Dezani-Ciancaglini.

ABSTRACT. This paper introduces the hybrid quantum language with general recursion Hyrql, driven towards resource-analysis. By design, Hyrql does not require the specification of an initial set of quantum gates. Hence, it is well amenable towards a generic cost analysis, unlike languages that use different sets of quantum gates, which lead to quantum circuits of distinct complexity. Regarding resource-analysis, we show how to relate the runtime of an expressive fragment of Hyrql programs with the size of the corresponding quantum circuits. We manage to capture the class of functions computable in quantum polynomial time, which, by Yao's Theorem, corresponds to families of circuits of polynomial size. Consequently, this result paves the way for the use of termination and runtime-analysis techniques designed for classical programs to guarantee bounds on the size of quantum circuits.

ABSTRACT. In this paper, we show that the equational theory of relational Kleene algebra with the graph loop operator is PSpace-complete. Here, the graph loop is the unary operator that restricts a binary relation to the identity relation. We further show that this PSpace-completeness still holds by extending with top, tests, converse, and nominals. Notably, by using graph loop and top, we show that for Kleene algebra with tests (KAT), the equational theory of relational KAT with domain is PSpace-complete, resolving a problem left open in previous works, whereas the equational theory of relational KAT with antidomain is ExpTime-complete. To this end, we introduce a novel automaton model on relational structures, named loop-automata. Loop-automata are obtained from non-deterministic finite string automata (NFA) by adding a transition type that tests whether the current vertex has a loop. Using this model, we can give a polynomial-time reduction from the above equational theories to the language inclusion problem for 2-way alternating string automata.

ABSTRACT. Reinforcement Learning (RL) enables autonomous agents to learn policies from experience, but realistic problems often involve enormous state spaces, making learning and generalisation challenging. Abstraction and approximation are therefore essential. Relational Reinforcement Learning (RRL) offers a way to reason about objects and their relations, and the CARCASS framework by Martijn van Otterlo demonstrates how logical representations can model Markov Decision Processes (MDPs) in first-order domains. Originally implemented in Prolog, CARCASS leverages domain knowledge to create powerful abstractions. We explore Answer-Set Programming (ASP), which is a rich and, contrary to Prolog, fully declarative modelling language, to realise CARCASS abstractions. We evaluate our ASP-based implementation in case studies of two domains, viz. Blocks World and Minigrid. Our results indicate that CARCASS with ASP provides a promising approach to constructing abstractions for RL, especially when domain knowledge is available.

ABSTRACT. Large Language Models (LLMs) have recently been adopted for semantic data extraction and parsing from unstructured text, enabling the generation of candidate relational facts from natural language. However, while LLMs are effective at extraction, they are not reliable solvers of complex combinatorial reasoning tasks or global consistency constraints, and logic-based extraction pipelines often require issuing multiple queries while coping with incomplete or spurious outputs. In this paper, we propose a logic-guided data extraction framework that combines LLM-based extraction with Answer Set Programming (ASP), delegating fact extraction to the LLM and all validation, inference, and control to ASP, which plays an active role in structuring and guiding the extraction process. In contrast to baseline pipelines that invoke the LLM independently for all target predicates, our approach uses ASP reasoning to determine which predicates are logically admissible at each stage, thereby guiding the selection of extraction queries. The framework interleaves LLM calls with ASP reasoning and derivation, allowing logically implied facts to be inferred without additional extraction and enabling early consistency checks. We formalize the proposed pipeline and show that, under mild assumptions on the extraction oracle, it is equivalent to the baseline approach in terms of the final extracted facts, while reducing the number of LLM calls. We further introduce a caching mechanism for logic-based control queries, exploiting monotonicity properties of conjunctive queries over incrementally constructed fact sets to reduce the number of solver invocations. An experimental evaluation on benchmarks derived from standard Answer Set Programming domains shows that the proposed framework substantially reduces the number of LLM calls and, in practice, improves extraction quality by mitigating spurious outputs. These results demonstrate the effectiveness of using non-monotonic logic programming as a control mechanism for semantic data extraction from text.

ABSTRACT. Neurosymbolic AI combines neural networks with symbolic programs to create robust and explainable predictions. One such framework is NeurASP, which trains a neural network to predict concepts and reasons over them using rules written in answer set programming (ASP) to solve downstream tasks. Crucially, labels are only provided for the downstream prediction produced by the symbolic rules, not for the latent concepts themselves. Backpropagation through the non-differentiable ASP component requires expensive probability and gradient calculations, which has hindered scalability to more sophisticated tasks. In this paper, we address the current limitations of NeurASP by improving its computational performance through vectorization, batch processing and caching of intermediate computations during training. We compare computation speeds between the original and our new implementation of NeurASP and report speedups of multiple orders of magnitude for larger tasks. To this end, we propose a new dataset of difficult tasks involving playing cards, which we use to test the capabilities of NeurASP's enhanced learning function.

ABSTRACT. Generating accurate and executable code using Large Language Models (LLMs) remains a sig- nificant challenge for underrepresented programming languages, such as Prolog and Lisp, due to the scarcity of public training data compared to high-resource languages like Python. This pa- per introduces a generalizable Reinforcement Learning (RL) approach that combines small-scale versions of the Qwen2.5-Coder model with Group Relative Policy Optimization (GRPO) to en- able effective code generation through reasoning. To address the limitations of sparse datasets, we integrate execution-driven feedback directly into the RL loop, utilizing a reward system that exploits both logical correctness and structural formatting. Experimental results on GSM8K dataset demonstrate significant improvements in reasoning quality and code accuracy across underrepresented languages. These findings underscore the potential of our approach to bene- fit a wide range of programming languages lacking extensive training resources by leveraging symbolic reasoning and interpreter-based feedback.

ABSTRACT. In this paper, we describe methods for drawing conclusions from inconsistent information in a particularly cautious manner. These approaches to cautious paraconsistent reasoning are especially useful in situations where the outcomes of the conclusions are irreversible or have far-reaching consequences in the given context. Such inference methods are therefore more restrictive than standard approaches to reasoning under inconsistency, which rely on (the formulas in the intersection of) consistent subsets of the knowledge base. In particular, the reasoning methods under consideration allow to infer only those conclusions that are fully guaranteed, namely those that are in no way affected by the inconsistencies in the base. The paper presents several techniques for implementing cautious paraconsistent reasoning and compares their basic properties and relative strengths.

ABSTRACT. In response to a concern raised by Horty, this paper develops a two-tiered, preference-based semantic framework for modeling defeasible conditional obligations. The paper extends a Hansson–Lewis style preference semantics for dyadic deontic logic by incorporating a nonmonotonic reasoning mechanism that enables previously derived obligations to be withdrawn when new, potentially conflicting information comes in. The account is bi-preferential: two orderings-ideality and normality-on worlds are employed to address shortcomings in earlier approaches, with a separate ranking method for each. At the nonmonotonic layer, a number of postulates are considered, including antecedent strengthening, inclusion and no-drowning. A connection is established with so-called constrained input/output (I/O) logic-an existing standard for normative reasoning based on a different methodology.

ABSTRACT. Like Pearl’s System Z, c-representations provide a constructive approach to compute a ranking function from a conditional belief base from which further (conditional) beliefs can be derived, meeting major quality standards of nonmonotonic reasoning. This paper proposes a network-based structure for c-representations that allows for cutting down the complexity of reasoning significantly by decomposing the conditional belief base over a hypertree. We introduce c-LEG networks capturing the interactions among conditionals on a syntactical basis in full compatibility with the semantics of c-representations. This allows for reasoning in much smaller local contexts while still complying with the global information provided by the full conditional belief base. Moreover, we generalize the so-called safety property, which was recently presented in the context of conditional syntax splitting, to ensure that local c-representations of subbases over the hyperedges can be merged to yield global c-representations of the full conditional belief base. This allows for computing global c-representations step by step in local contexts, following the structure of the hypertree.

ABSTRACT. This paper establishes and proves representation theorems for cumulative propositional dependence logic and for cumulative propositional logic with team semantics. Cumulative logics are famously given by System C. For propositional dependence logic, we show that System C entailments are exactly captured by cumulative models from Kraus, Lehmann and Magidor. On the other hand, we show that entailment in cumulative propositional logics with team semantics is exactly captured by cumulative and asymmetric models. For the latter, we also obtain equivalence with cumulative logics based on propositional logic with classical semantics. The proofs will be useful for proving representation theorems for other cumulative logics without negation and material implication.

ABSTRACT. As schema languages for RDF data become more mature, we are seeing efforts to extend them with recursive semantics, applying diverse ideas from logic programming and description logics. While ShEx has an official recursive semantics based on greatest fixpoints (GFP), the discussion for SHACL is ongoing and seems to be converging towards least fixpoints (LFP). A practical study we perform shows that, indeed, ShEx validators implement GFP, whereas SHACL validators are more heterogeneous. This situation creates tension between ShEx and SHACL, as their semantic commitments appear to diverge, potentially undermining interoperability and predictability. We aim to clarify this design space by comparing the main semantic options in a principled yet accessible way, hoping to engage both theoreticians and practicioners, especially those involved in developing tools and standards. We present a unifying formal semantics that treats LFP, GFP, and supported model semantics (SMS), clarifying their relationships and highlighting a duality between LFP and GFP on stratified fragments. Next, we investigate to which extent the directions taken by SHACL and ShEx are compatible. We show that, although ShEx and SHACL seem to be going in different directions, they include large fragments with identical expressive power. Moreover, there is a strong correspondence between these fragments through the aforementioned principle of duality. Finally, we present a complete picture of the data and combined complexity of ShEx and SHACL validation under LFP, GFP, and SMS, showing that SMS comes at a higher computational cost under standard complexity-theoretic assumptions.

ABSTRACT. SHACL (Shapes Constraint Language) expresses constraints on RDF data by means of so-called shapes. The central service is validation: verifying whether a data graph complies with a SHACL specification, but there are no static analysis services to compare specifications. In this paper, we study the following problem: decide whether all graphs that validate one SHACL document also validate another. Unlike previous works that have considered the implication of shape expressions only, we consider specifications comprising shape definitions and targets. We show that containment is undecidable under the supported and the stable model semantics, even for the fragment that uses the description logic ALCIO for shape expressions. Under the well-founded semantics, in contrast, it is decidable in single exponential time. Our key technical contributions are a translation of SHACL under well-founded semantics into the full hybrid mu-calculus, revealing a novel link between shape validation and fixed point modal logic, and a worst-case optimal automata-based decision procedure.

ABSTRACT. Computing certain answers is the standard approach when data or knowledge is incomplete. This very natural concept rooted in logical validity suffers from a severe weakness: its generally intractable computational complexity. Consequently, significant effort has been made to find tractable cases, often at the expense of severe restrictions. Here we explore a different approach, relaxing not the classes of allowed queries but the very strict notion of certainty. Our starting point is an observation from Libkin (2018) that replacing certainty with asymptotic probability 1 overcomes intractability for large classes of queries. This theoretical observation was made for relational queries under a simple probabilistic model of uniform distribution and an infinite domain of equally likely values; these are hardly the realities of querying data. We therefore ask whether this phenomenon is robust enough to extend to other, realistic distributions, to be applicable to other data models, and to help with practical query answering. We answer all of these positively. After extending tractability via naïve evaluation to many distributions, we extend the approach to graph data, and then experimentally show that for relational and graph queries from standard TPC and LDBC benchmarks, convergence to high probability query answers is fast and practical.

ABSTRACT. Inductive knowledge graph completion models aim to perform link prediction on knowledge graphs with completely new entities and/or relations. The motivation and key goal of these methods is to transfer relational knowledge and patterns across disjoint knowledge graphs. Although such methods have shown promising empirical results across a variety of datasets, we argue here that these results do not provide sufficient evidence for the successful transfer of relational knowledge. We identify biases in the construction principles of the available benchmark datasets, provide a simple baseline method that does not rely on relational paths or more sophisticated relational patterns, and show empirically that this simple baseline performs on par with the state-of-the-art zero-shot model ULTRA. Our results question whether relational knowledge transfer really takes place in recent methods.

ABSTRACT. Supply chain planners are often faced with a recurring routing and packing problem: given a network of suppliers, hubs, and consumers spread across several countries, they must decide which parts travel which routes, at what frequency, and how they should be packed. This paper describes our current research on encoding this problem in Answer Set Programming (ASP). A direct translation did not scale to industrial use cases, so we applied a set of encoding optimisations and decomposed the problem into two stages. The first stage fixed aggregate flows across the network, while the second assigns parts to individual trips using soft constraints that favour robust packings. Preliminary experiments show that the optimised encoding cuts solver search time substantially compared to the baseline encoding, and the two-stage decomposition offers a principled way to encode robustness directly into the network. Remaining work involves a full experimental study of how different encoding choices trade off cost against robustness, and how well a robust solution can service demand under disruption.

ABSTRACT. The Stable Roommates problems are characterized by the preferences of agents over other agents as roommates. A solution is a partition of the agents into pairs that are acceptable to each other (i.e., they are in the preference lists of each other), and the matching is stable (i.e., there do not exist any two agents who prefer each other to their roommates, and thus block the matching). This study focuses on a human-centered and computationally-challenging interdisciplinary problem of the Stable Roommates problem and its variations. Motivated by real-world applications, and considering that stable roommates problems do not always have solutions, the goal is to develop novel computational methods to solve these problems, that are not only computationally efficient but also applicable in real-world to benefit humans.

ABSTRACT. Non-omniscient agents may fail to recognise inconsistencies in their beliefs, either due to incomplete deductive abilities or because beliefs are distributed across multiple agents. However, as inconsistent agents revise their beliefs, they may eventually become consistent. Our goal is to investigate the conditions under which this is possible. To this end, we aim to develop a multi-agent logic of belief and belief revision that represents agents with incomplete deductive abilities. This framework will enable the formal study of belief revision in both individual and distributed settings.

ABSTRACT. KLM-style defeasible justifications, as they are understood in the literature, are displayed mainly in a textual format. This has happened regardless of the logic under consideration. Though this representation is needed for their computation, this might not be the best way for users to understand why a justification holds. Other forms (particularly graphical ones) might be easier for people to understand. But before that hypothesis can be tested, we need to understand if it is even possible to represent justifications graphically in a sensible manner. Our initial idea is attempting to do so in graph format - here "graph" refers to a construction with nodes and edges. A similar notion has already been developed for abstract argumentation frameworks. We plan to leverage some existing mechanisms that have already been developed in the assumption-based argumentation and abstract argumentation use-case for our own.

ABSTRACT. In my PhD, I am investigating the incorporation of defeasible reasoning in Description Logics (DLs) and modal logics. Specifically, I focus on the preferential reasoning of Kraus, Lehmann and Magidor (KLM) and argue that although there exist methods for extending defeasible reasoning into more expressive logics, many of these have shortcomings when it comes to their inferential power, and their sensitivity to binary and relational data. I therefore outline a proposal to establish a semantic-first approach to logics with binary or relational data, which captures many DL and modal logic formalisms. This is done with the aim of working both ``top-down'' and ``bottom-up'': considering specific extensions to concrete systems developed in DLs and modal logics while simultaneously considering generalised semantic principles for preferential semantics with binary data.

ABSTRACT. When a machine learning model produces rules like “feature a predicts label 1, except when b is also present,” it looks like defeasible reasoning. But looking like it is not the same as being it. This thesis asks: under what conditions does a learned rule-based classifier actually behave like a defeasible theory? We answer this for a class of classifiers called Exception Closed Conjunctive Rule Sets (ECCRS). When a learned rule set satisfies a single structural condition, called strict global exception closure, its predictions are shown to agree exactly with three well-known defeasible reasoning frameworks: Rational Closure, Lexicographic Closure, and System W. This gives a formal justification for reading the classifier’s output as defeasible knowledge, not just as a list of patterns. We also show that strict global exception closure is the only condition that needs to be checked directly, since the other required conditions either follow from it or can be enforced by a simple pruning step that does not change any predictions. The results open a path toward what we call defeasible machine learning: designing learners that do not just produce readable rules, but produce rules with a principled defeasible meaning built in.

ABSTRACT. Machine Learning models are nowadays becoming increasingly widespread across a wide range of application domains, and the models that dominate the current scene mainly rely on purely sub-symbolic approaches. However, while effective, these models often face limitations and challenges that symbolic approaches could help overcome. These include the integration of formal logical reasoning to constrain and formally guarantee the behavior of the models, improve their interpretability and explainability, and ensure their trustworthiness. In this paper, we present a novel neuro-symbolic research path that bridges sub-symbolic Machine Learning classifiers with symbolic techniques from the Knowledge Representation and Reasoning field. Unlike previous approaches, our framework enables reasoning simultaneously on both the raw data features used by the classifiers and a symbolic intensional knowledge specified for the domain. This work describes the main technical results we have obtained, the ongoing advancements, and the future challenges we aim to address.

ABSTRACT. Reinforcement learning is often misaligned with designer intentions because reward functions can induce undesirable behaviors. These unintended outcomes are hard to anticipate during design and difficult to analyze formally. To address this, we propose specifying rewards using Knowledge Representation (KR) languages, which inherently impose structural and semantic constraints. Our goal is to determine how well these languages support reasoning about reward functions, whether certain undesirable behaviours are ruled out by construction, how effectively agents can learn from the resulting rewards, and whether the goal specifications themselves can be learned. We identify properties of reward functions that can give rise to misaligned behavior and briefly discuss why KR languages may be better suited to addressing them.

ABSTRACT. Knowledge compilation is a paradigm in knowledge representation and reasoning that transforms complex combinatorial objects into representations supporting tractable query evaluation. Among its most fundamental tools are Binary Decision Diagrams (BDDs), whose efficiency depends critically on variable ordering. In practice, this gives rise to the dynamic variable reordering problem, which is traditionally addressed via local search heuristics such as sifting, guided primarily by diagram size. This proposal develops a structure-aware and planning-based approach to dynamic reordering. We formulate the problem as a sequential decision process and introduce a compositional neural encoder that operates directly on BDD structure, enabling the use of deep reinforcement learning to guide reordering decisions. Furthermore, we exploit the fully observable and deterministic nature of BDD packages to incorporate model-based planning via lookahead search. The resulting framework aims to move beyond size-driven heuristics by enabling decisions informed by both the structure of the diagram and the anticipated long-term effects of reordering actions.

ABSTRACT. Reinforcement learning policies often fail to generalize beyond the specific tasks on which they are trained, and this limitation becomes especially severe in long-horizon settings where success depends on satisfying structured constraints over time. In these settings, task objectives are naturally compositional, reward signals are sparse and delayed, and existing approaches often lack both a clear target notion of generalization and a principled way to evaluate whether the generalization schematic has been learned. This dissertation studies how logical structure can be used to address these challenges. The central research goal is to develop a framework for reliable long-horizon generalization in reinforcement learning from temporal-logic specifications. The key idea is to use logical specifications not only to describe complex tasks, but also to define structured families of related tasks in which generalization can be formalized, learned, and eventually verified. In this setting, tasks evolve according to a fixed update rule, and the objective is to train on a small subset of task instances and produce policies that succeed zero-shot on unseen ones. This perspective opens up several linked research directions such as learning compact policy-evolution rules that capture transfer across task families, scaling such learning to long-horizon problems through decomposition and stable supervision, and developing certificate-based tools that move evaluation beyond empirical rollout success toward more structured notions of correctness. In our current progress, we have formalized inductive generalization over specification-defined task families, developed a scalable decoupled approach for learning policy-evolution templates, and introduced certificate-based methods for evaluating and diagnosing generalization. Taken together, these components motivate a broader thesis program aimed at integrating specification-guided task structure, compositional planning, and certificate-guided reasoning into a unified approach for scalable and reliable reinforcement learning generalization.

ABSTRACT. This PhD research focuses on counterfactual explainability for graph neural networks (GNNs), with an emphasis on local-level, model-agnostic, post-hoc explanations. A novel pipeline is proposed to enable more targeted and controllable graph edits. The approach combines ideas from factual explainability with edge prediction models inspired by link prediction. The aim is to enhance the quality, robustness, and interpretability of counterfactual explanations while keeping the method computationally tractable. Experiments are conducted on real-world and synthetic graph classification benchmarks, and the approach is compared against existing state-of-the-art methods across multiple evaluation metrics.

ABSTRACT. Ontologies formulated in description logics are widely used to formalise knowledge and terminologies in domains such as medicine and biology. One central reasoning task for ontologies is to decide whether one concept is subsumed by the other. While modern reasoners can efficiently determine the subsumptions of large-scale ontologies, they offer little insight into the reasoning process itself. Concept interpolation addresses this by computing an intermediate concept in a user-specified vocabulary that witnesses the subsumption. Concept interpolation can be used to solve a range of problems in KR, including explaining reasoning, extracting explicit definitions, and learning concepts from examples. Despite its relevance, no practical methods for concept interpolation in description logics have been developed. Furthermore, to be used for concept learning, an interpolation method needs to support nominals, which are known to make the interpolation problem harder. In this project, we will develop practical methods for deciding the existence and computing concept interpolants in different logics of the EL and ALC families. If they exist, we want to find the “optimal” interpolant based on specific criteria, and compute approximations otherwise.

ABSTRACT. Existing symmetry-breaking techniques for SAT constrain the search space without simplifying the formula. Lex-leader predicates, the most widely used approach, add global ordering constraints to remove symmetric solutions, but often at the cost of substantial formula blowup and large proofs. Moreover, they ignore structural properties of the formula, such as connectedness, that could enable stronger symmetry breaking. In this paper, we treat symmetry breaking not merely as a restriction mechanism, but as a simplification mechanism. Notably, our algorithm only adds unit and binary symmetry-breaking clauses. This enables strong formula simplifications, which can expose additional symmetries and in turn allows for multiple rounds of symmetry breaking. Crucially, we exploit connectivity in the formula’s graph representation, including the presence of cliques, to guide the order in which to break symmetries. We implemented our algorithm in the satsuma tool and evaluated it on a large set of benchmarks. As a preprocessing step for CaDiCaL, it improves PAR-2 scores by 22% on the SAT competition 2025 and by 12% on the SAT anniversary track. It also substantially outperforms lex-leader and orbitopal fixing while producing compact proof certificates.

ABSTRACT. Parity-SAT is the problem of determining whether a given CNF formula has an odd number of satisfying assignments. As a canonical $\oplus$P-complete problem, it represents a fundamental variant of the exact model counting problem (\#SAT). Under the Strong Exponential Time Hypothesis (SETH), Parity-SAT admits no $O^*((2-\varepsilon)^n)$-time or $O^*((2-\varepsilon)^m)$-time algorithm for any constant $\varepsilon>0$, where $n$ and $m$ denote the numbers of variables and clauses, respectively. Thus, breaking the $2^n$ or $2^m$ barrier appears impossible in full generality. In this work, we revisit this barrier through structural restrictions and a refined exploitation of parity. We study Parity-$d$-occ-SAT, where each variable appears in at most $d$ clauses, and obtain three main results. First, we design an $O^*(2^{m(1-1/O(d))})$-time algorithm, thereby breaking the $2^m$ barrier for every fixed $d$. Second, for the special case $d=2$, we develop a significantly sharper branching algorithm running in $O^*(1.1193^n)$ time or $O^*(1.3248^m)$ time. Third, leveraging the structural insights underlying the $d=2$ case, we obtain an $O^*(1.1052^L)$-time algorithm for general Parity-SAT, where $L$ denotes the formula length. All algorithms use only polynomial space. Notably, our running-time bounds are better than the best known bounds for the corresponding exact counting counterparts, highlighting a genuine algorithmic advantage of parity over counting. Conceptually, our results demonstrate that parity admits finer structural reductions and more efficient branching than exact model counting, and that bounded occurrence can be systematically leveraged to circumvent classical exponential barriers.

ABSTRACT. We introduce \emph{Graphical Algebraic Geometry} (GAG), a family of diagrammatic languages extending the Graphical Linear Algebra programme. We construct several languages within this family and prove that they are universal and complete for the corresponding (co)span semantics of commutative algebras and affine varieties. This framework provides clear graphical representations of algebraic structures --- such as polynomials, ideals, and varieties --- enabling intuitive yet rigorous diagrammatic reasoning. We showcase two practical viewpoints on GAG. First, we show that instances of counting constraint satisfaction problem (\#CSP) are recast as rewrite problems of closed diagrams in GAG. This means that deciding rewriteability in GAG is \#P-hard, and GAG can be viewed as a complete and compositional rewrite system for networks of polynomial constraints. Second, we characterize the qudit ZH calculus, a diagrammatic language for quantum computation, as an extension of Graphical Algebraic Geometry. This establishes the correspondence that \emph{Graphical Algebraic Geometry is to the ZH calculus what Graphical Linear Algebra is to the ZX calculus}. Using this construction, we show that computing amplitudes in qudit ZH requires only a constant number of queries to a GAG oracle.

ABSTRACT. We introduce a complete equational theory for the fragment of quantum circuits generated by the real Clifford gates plus the two-qubit controlled-Hadamard gate. That is, we give a simple set of equalities between circuits of this fragment, and prove that any other true equation can be derived from these. This is the first such completeness result for a finitely-generated, universal fragment of quantum circuits, with no parameterized gates and no need for ancillas.

ABSTRACT. We present sound and complete relational program logics for infinite-dimensional quantum and classical-quantum programs. The logics model assertions as self-adjoint unbounded linear relations, which simultaneously support quantitative and qualitative reasoning. Our main theoretical results include new convergence theorem and infinite-dimensional duality theorems for infinite-dimensional quantum states, which we use to establish completeness.

ABSTRACT. The Kochen-Specker no-go theorem established that hidden-variable theories in quantum mechanics necessarily admit contextuality. This theorem is formally stated in terms of the partial Boolean algebra structure of projectors on a Hilbert space. Each partial Boolean algebra provides a semantics for interpreting propositional logic. In this paper, we examine the complexity of propositional satisfiablity for various classes of partial Boolean algebras. We first show that the satisfiability problem for the class of non-trivial partial Boolean algebras is NP-complete. Next, we consider the satisfiability problem for the class of partial Boolean algebras arising from projectors on finite dimensional Hilbert spaces. For any real Hilbert spaces of dimension greater than 2 and complex Hilbert spaces of dimension greater than 3, we demonstrate that the satisfiablity problem is complete for the existential theory of the reals. Interestingly, the proofs of these results make use of Kochen-Specker sets as gadgets. As a corollary, we conclude that deciding quantum homomorphism in these fixed dimensions are also complete for the existential theory of the reals. Finally, we show that the satisfiability problems for the class of all Hilbert spaces and all finite-dimensional Hilbert spaces is undecidable.

ABSTRACT. Reachability in pushdown vector addition systems with states (PVASS) is among the longest standing open problems in Theoretical Computer Science. We show that the problem is decidable in full generality. Our decision procedure is similar in spirit to the KLMST algorithm for VASS reachability, but works over objects that support an elaborate form of procedure summarization as known from pushdown reachability.

ABSTRACT. We consider a variant of VASS extended with integer counters, denoted VASS+Z. These are automata equipped with N and Z counters; the N-counters are required to remain nonnegative and the Z-counters do not have this restriction. We study the complexity of the reachability problem for VASS+Z when the number of N-counters is fixed. We show that reachability is NP-complete in 1-VASS+Z (i.e. when there is only one N-counter) regardless of unary or binary encoding. For d ≥ 2, using a KLMST-based algorithm, we prove that reachability in d-VASS+Z lies in the complexity class F_{d+2}​. Our upper bound improves on the naively obtained Ackermannian complexity by simulating the Z-counters with N-counters. To complement our upper bounds, we show that extending VASS with integer counters significantly lowers the number of N-counters needed to exhibit hardness. We prove that reachability in unary 2-VASS+Z is PSPACE-hard; without Z-counters this lower bound is only known in dimension 5. We also prove that reachability in unary 3-VASS+Z is TOWER-hard. Without Z-counters, reachability in 3-VASS has elementary complexity and TOWER-hardness is only known in dimension 8.

ABSTRACT. Nested counter systems (NCS) are a generalization of counter systems to higher-order counters. Here, a higher-order counter is allowed to have other (lower-order) counters as elements, instead of just a number. It is known that coverability for NCS is $\mathbf{F}_{\epsilon_0}$-complete, where $\mathbf{F}_{\epsilon_0}$ is a class in the fast-growing hierarchy of complexity classes. In this paper, we consider an extension of NCS called nested reset counter systems (NRCS) that extends NCS with resets. We show that coverability for NRCS over order-$k$ counters is $\mathbf{F}_{\Omega_k}$-complete where $\Omega_k$ is the tower of height $k$ of the $\omega$ ordinal. This gives the first natural complete problems for all of these classes. As an application of our results, we improve existing upper bounds for various problems from XML processing, graph transformation systems, $\pi$-calculus, logic and parameterized verification. Furthermore, using NRCS, we also prove $\mathbf{F}_{\Omega_k}$-completeness of the considered problems from parameterized verification and logic.

ABSTRACT. Indexed languages are a classical notion in formal language theory, which features prominently in higher-order model checking. The downward closure (i.e. set of all subwords) of an indexed language is well-known to be a regular overapproximation. Zetzsche (ICALP 2015) has shown that the downward closure of an indexed language is effectively computable. However, that algorithm yields no complexity bounds, and it has remained open whether there exists a primitive-recursive construction. We settle this question and prove a tight triply exponential upper bound. It relies on recent advances in semigroup theory, which provide bounded-size summaries of words w.r.t. a finite semigroup.

ABSTRACT. The ability to abstract is important in AI systems and in problem solving, as generalizing over irrelevant details facilitates finding solutions. In the context of Answer Set Programming (ASP), abstraction has been recently investigated with a focus on the omission of unnecessary details, which is related to forgetting, as well as on clustering vocabulary of similar concepts into a common abstract representation. In the latter case, a characterization has been provided that identifies when such abstraction is possible without affecting the answer sets under the addition of any set of facts, in the spirit of uniform equivalence and aligned with the ASP methodology where a general problem encoding is used with varying instances. However, when this characterization fails, no abstraction is possible, and even if it succeeds, computing an abstracted program syntactically is only possible for a limited subclass of programs. In this paper, we consider that not all kinds of facts are required to be added in general, and investigate under which conditions such abstraction is indeed always possible as well as when and how to compute abstracted programs, generalizing at the same time (compared to related work) to a larger class of programs with wider applicability.

ABSTRACT. This paper describes the process of translating rules that may contain arithmetic operations into the language of first-order logic. It identifies a normal form for which this transformation can be performed in a particularly simple and natural way. Other rules can be converted to this normal form by steps that preserve their meaning under the stable model semantics.

ABSTRACT. We develop an Answer Set Programming (ASP)-based approach for computing the smallest bidirectional macro schemes (BMSs), a fundamental NP-hard optimization problem in dictionary-based compression. Our approach relies on high-level ASP encodings and delegates both the grounding and solving tasks to an off-the-shelf ASP solver. The proposed encoding is compact and extensible, and leverages advanced ASP techniques to improve scalability, including ASP modulo acyclicity and refined declarative encodings of acyclicity constraints. We further show that our ASP encoding can be naturally extended to compute the smallest straight-line programs (SLPs), another important NP-hard measure of repetitiveness. Furthermore, we establish the competitiveness of our approach by empirically contrasting it with a more dedicated MaxSAT-based approach.

ABSTRACT. Answer Set Programming with Quantifiers (ASP(Q)) extends Answer Set Programming (ASP) by allowing quantification over answer set programs. Although probabilistic extensions to ASP exist, there is no such counterpart for ASP(Q). In this paper, we close this gap and introduce Inferential Quantified Answer Set Programming (ASP(Q)INF), which extends ASP(Q) with probabilistic inference, allowing reasoning on programs characterized by an alternation of quantifiers, where the innermost level may also consider uncertainty. We first showcase the ASP(Q)INF modeling capabilities through three representative real-world problems. Then, we conduct a computational complexity study, propose an encoding within the Algebraic Model Counting framework, and provide a practical implementation on top of an existing solver. Moreover, to assess the viability of our proposal, we carried out an experimental evaluation that confirms the effectiveness and practical applicability of ASP(Q)INF.

ABSTRACT. We consider a particular subclass of normal programs that we call simple guess-and-check (SGC) programs. SGC programs consist of guess rules (i.e. rules without positive body atoms) and arbitrary constraints. Many simple combinatorial problems such as graph coloring can be encoded via SGC programs. Moreover, constraint-free SGC programs are known to have a close relation to abstract argumentation frameworks. Our main result shows that for SGC programs the notions of strong and uniform equivalence coincide (in contrast to general normal programs), but do not amount to classical equivalence (as is the case of positive programs). Moreover, we study the characteristics of SE-models for SGC programs; this allows to check whether an arbitrary program (part) can be equivalently formulated within the simpler class of SGC programs. Finally, we briefly discuss our results in relation to other classes of programs.

ABSTRACT. Aiming to harmonise finite and infinite model reasoning, we initiate the study of partially finite models, where the reasoning task comes with a formula that specifies a part of the model that must be finite. We focus on the problem of partially finite query entailment in description logics (DLs): given a knowledge base (KB), a query, and a distinguished concept, decide whether the query holds in all models of the KB that interpret the distinguished concept as a finite set. To break the ground, we work with the DL S, an extension of the basic DL ALC with transitive roles, which is one of the simplest cases where finite and infinite query entailment diverge. Generalising previous results on the finite and infinite cases, we show that also partially finite entailment of conjunctive queries is in 2-Exp for S. The solution involves sophisticated infinite model surgery and goes far beyond combining the arguments for the two special cases. As a direct application, we show how the problem of query containment in the presence of closed predicates can be solved by reduction to partially finite query entailment

ABSTRACT. We consider the following fundamental problem: given a database D, Boolean conjunctive query (CQ) q, and fact f from D, decide whether f is relevant to q w.r.t. D, i.e. does f belong to a minimal subset S of D that makes q hold. Despite being of central importance to query answer explanation, the combined complexity of deciding query relevance has not been studied in detail, leaving open what makes this problem hard, and which restrictions can yield lower complexity. Relevance has already been shown to be harder than query evaluation: namely, it is Sigma^p_2 -complete for CQs, even over a binary signature. We further observe that NP-hardness applies already to (acyclic) chain CQs. Our work identifies self-joins (multiple atoms with the same relation) as the culprit. Indeed, we prove that if we forbid or bound the occurrence of self-joins, then relevance has the same complexity as query evaluation, namely, NP (without structural restrictions) and LogCFL (for bounded hypertreewidth classes). In the ontology setting, we establish an analogous result for ontology-mediated queries consisting of a CQ and DL-Lite_R ontology, namely that relevance is no harder than query answering provided that we bound the interaction width (which generalizes both self-join width and a recently introduced ‘interaction-free’ condition). Our results thus pinpoint what makes relevance harder than query evaluation and identify natural classes of queries which admit efficient relevance computation.

ABSTRACT. We study the expressive power and computational properties of first-order logic and its extensions under the semiring semantics originating from the seminal work of Green, Karvounarakis, and Tannen. While semiring semantics is currently extensively used, e.g., in the study of provenance in database theory and description logic, a comprehensive computational analysis of these logics acting over general semirings is still lacking. We analyse expressivity, and complexity of model-checking of first-order formulas in this framework, providing characterizations in terms of generalized Blum–Shub–Smale machines over semirings. We also show a variant of Fagin's theorem, i.e., a logical characterization of nondeterministic polynomial time over semirings using a version of existential second-order logic. We further generalize Cook's theorem for the semiring framework and show that propositional satisfiability in the semiring semantics is complete for this notion of NP, and that the true existential first-order theory of the semiring is complete for its Boolean fragment.

ABSTRACT. We report on our recent contribution that has been briefly presented earlier this year at AAAI'26. We study the data complexity of querying inconsistent weighted description logic (DL) knowledge bases under recently-introduced cost-based semantics. In a nutshell, the idea is to assign each interpretation a cost based upon the weights of the violated axioms and assertions, and certain and possible query answers are determined by considering all (resp. some) interpretations having optimal or bounded cost. Whereas the initial study of cost-based semantics focused on DLs between EL_⊥ and ALCO, we consider DLs that may contain inverse roles and role inclusions, thus covering prominent DL-Lite dialects. Our data complexity analysis goes significantly beyond existing results by sharpening several lower bounds and pinpointing the precise complexity of optimal-cost certain answer semantics (no non-trivial upper bound was known). Moreover, while all existing results show the intractability of cost-based semantics, our most challenging and surprising result establishes that if we consider DL-Lite-bool-H ontologies and a fixed cost bound, certain answers for instance queries and possible answers for conjunctive queries can be computed using first-order rewriting and thus enjoy the lowest possible data complexity (AC^0 ).

ABSTRACT. Inclusion dependencies form one of the most widely used classes of database dependencies. We expand existing results on the axiomatization and computational complexity of their implication problem to two extended variants. First, we present an alternative completeness proof for standard inclusion dependencies and generalize it to inclusion dependencies with repetitions that can express equalities between attributes. The proof uses only two values, enabling us to work within the Boolean setting. Furthermore, we study inclusion dependencies with Boolean constants, provide a complete axiomatization, and show that no such axiomatization is k-ary. We also establish that the decision problems for both extended versions remain PSPACE-complete. The extended inclusion dependencies are common in team semantics, which serves as the formal framework for the results.

ABSTRACT. Logic-based eXplainable Artificial Intelligence (XAI) represents a rigorous alternative to non-symbolic XAI. However, one critical limitation of logic-based explanations is the complexity of reasoning about machine learning (ML) models. Sample-based explanations represent a rigorous, model-agnostic, but also scalable alternative to model-based explanations. Whereas finding one sample-based explanation can be done in polynomial time, the computation of a smallest explanation is computationally hard. This paper develops a novel heuristic method for the computation of small sample-based explanations. The experiments confirm that the explanation size is often the smallest possible, that computation times are a fraction of existing alternatives, and that explanation quality is most often better than existing alternatives.

ABSTRACT. We address the fundamental task of computing rigorous, sample-based abductive explanations for machine learning predictions. In this setting, we propose a new class of explanations derived from a generalization of the consensus operation in propositional logic. We prove that these explanations are precisely those that satisfy a monotonicity property ensuring they remain valid as the sample grows. Furthermore, we show that their computation can be performed efficiently. As a direct application, we also show how these explanations can be used to identify necessary and relevant features. The proposed framework provides a robust and scalable approach to formal model-agnostic XAI.

ABSTRACT. In recent years, explainable AI has become a major focus of research, driven by the need to better understand how AI systems arrive at their decisions in order to ensure trust and effective deployment. A central challenge in this field is the explanation of classifiers. Existing approaches typically distinguish between local explanations, which account for a classifier’s decision on an individual input, and global explanations, which aim to characterize the classifier’s behavior as a whole, independent of any particular input. This work concentrates on global explanations and characterizes classification decisions through "maximal" sufficient conditions that, when satisfied, guarantee that the classifier assigns the desired class to any input. We present a detailed analysis of the computational complexity of key problems in this setting across several important families of classifiers considered in the literature.

ABSTRACT. We study answer set verbalization: generating readable natural-language descriptions of ASP solver outputs. Unlike standard data-to-text settings, answer sets often lack an explicit schema and may involve structured, non-relational representations through complex terms rather than flat records. We propose a modular map–summarize framework that first maps atoms into predicate-aware textual fragments (via schema guidance, LLM-based mapping, or deterministic templates) and then uses a language model primarily for fluent aggregation. We evaluate the framework through a quantitative benchmark on structured ASP request databases, and a human evaluation of solver-generated explanation graphs. Results show that predicate-aware structured methods improve faithfulness and efficiency over direct LLM prompting.

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

ABSTRACT. Logics of definitions extend first order intuitionistic logic with fixed-point definitions which associate formulas to atomic predicates. These associated formulas must be constrained for consistency. In the original formulation, predicate symbols were required to be ordered and only predicates lower in the order were allowed to appear negatively in the defining formula. This constraint renders ineligible definitions such as those of logical relations in which the predicate being defined must be allowed to appear negatively, albeit with smaller arguments. Tiu has formalized a weaker constraint called ground stratification that permits such definitions and has shown that it suffices for consistency. Definitions can also be given a least fixed-point interpretation via a special induction rule. We address the question of whether Tiu's relaxation carries over to such a treatment. We propose a new induction rule for ground stratified inductive definitions that takes into account the fact that the definition of the predicate in question must itself be considered to be stratified by the complexity of its arguments to obtain a least fixed-point interpretation. We establish the consistency of the resulting logic and we illustrate its new capabilities via an example that encodes a strong normalizability proof for the simply typed $\lambda$-calculus in which the reducibility predicate is inductively defined by recursion on its arguments.

ABSTRACT. While Gentzen’s sequent calculus is a foundational tool for describing and investigating provability, its fine-grained inference rules generally do not directly support automated proof search. While aggregating some introduction rules into synthetic inferences, these do not provide mechanisms for reasoning naturally about the elementary mathematical notions of equivalence and congruence. In this paper, we present a first-order framework for reasoning modulo these relations within the sequent calculus. We provide a setting in which congruences can be treated as actual equalities, mirroring the informal practice of mathematicians and eliminating the need to explicitly use the lemmas typically required for formal congruence proofs. We demonstrate that this approach remains strictly first-order, avoids the complexity of higher-order or set-theoretic constructions, and yields proof systems that retain essential meta-theoretic properties.

ABSTRACT. Reasoning abut equality in calculi that involve binders and structural congruences is challenging because binding and equational theories interact in unexpected and non-obvious ways. We provide a sound and complete proof system to reason about equality modulo alpha-equivalence plus an arbitrary nominal equational theory, generalising nominal algebra by including general permutation fixed-point constraints. We provide examples of application in Milner's pi-calculus, a powerful model of concurrent computation that includes binders and a structural congruence.

ABSTRACT. One of the most significant achievements of equilibrium logic was the characterization of strong equivalence, a property crucial for program transformation and optimization in Answer Set Programming (ASP). While ASP has recently been extended to a higher-order setting to enhance its expressive power, the lack of a comparable purely logical foundation has made verifying strong equivalence for higher-order programs or even proving the correctness of simple program transformations, a difficult challenge. This paper addresses this gap by developing a logical semantics for higher-order ASP by extending the equilibrium logic framework. Within this extended framework we demonstrate that every stratified higher-order logic program possesses a unique equilibrium model. Moreover, we establish definability results demonstrating that the syntax of our higher-order language is sufficiently expressive to capture its semantic domains. Finally, and most importantly, we generalize the classical theorem of strong equivalence to the higher-order setting: we prove that two programs are strongly equivalent if and only if they share the same higher-order models.

ABSTRACT. The Event Calculus (EC) implemented in answer set programming (ASP) has proven suitable for specifying requirements put on safety-critical systems thanks to its elegant representation of both discrete and continuous changes and its semantic closeness to semi-formal natural language. However, continuous changes and the size (and possible unboundedness) of value domains of time and various system properties (fluents) pose significant challenges. Grounding-based ASP solvers, such as clingo, which only implement Discrete EC (DEC), lead to combinatorial explosion in program size as well as inaccuracies in the representation. On the other hand, the grounding-free s(CASP) does not discretize but struggles with non-termination due to its top-down execution. In this paper, we introduce Hybrid EC, an extended axiomatization of DEC, that tackles the challenges via so-called functional fluents and a mapping of time to abstract steps. We implement it using clingcon and clingo-lpx (Hybrid ASP systems over integers and rationals, respectively) where the (dense) value domains of fluents and time are represented as linear constraints and evaluated by external solvers, while ensuring termination whenever solutions exist. We validate both implementations on a number of examples and observe that, unlike clingo, they are indeed unaffected by the size of the domains and that handling rationals instead of integers does not impact scalability. Most importantly, the ability of clingo-lpx to handle dense domains enables accurate modeling of examples involving continuous change.

ABSTRACT. We prove the existence of two thresholds regarding the compilability of random 2-CNF formulas to OBDDs. The formulas are drawn from $F_2(n,\delta n)$, the uniform distribution over all 2-CNFs with $\delta n$ clauses and $n$ variables, with $\delta \geq 0$ a constant. We show that, with high probability, the random 2-CNF admits OBDDs of size polynomial in $n$ if $0 \leq \delta < 1/2$ or if $\delta > 1$. On the other hand, for $1/2 < \delta < 1$, with high probability, the random 2-CNF admits only OBDDs of size exponential in $n$. It is no coincidence that the two ``compilability thresholds'' are $\delta = 1/2$ and $\delta = 1$. Both are known thresholds for other CNF properties, namely, $\delta = 1$ is the satisfiability threshold for 2-CNF while $\delta = 1/2$ is the treewidth threshold, i.e., the point where the treewidth of primal graph jumps from constant to linear in $n$ with high probability.

ABSTRACT. We introduce Tree Decision Diagrams (TDD) as a model for Boolean functions that generalizes OBDD. They can be seen as a restriction of structured d-DNNF; that is, d-DNNF that respect a vtree $T$. We show that TDDs enjoy the same tractability properties as OBDD, such as model counting, enumeration, conditioning, and apply, and are more succinct. In particular, we show that CNF formulas of treewidth $k$ can be represented by TDDs of FPT size, which is known to be impossible for OBDD. We study the complexity of compiling CNF formulas into deterministic TDDs via bottom-up compilation and relate the complexity of this approach with the notion of factor-width introduced by Bova and Szeider.

ABSTRACT. A standard intensional account of probabilistic computation represents a randomized program as a deterministic computation that consumes an explicit random tape. This yields a two-layer perspective: an intensional layer that makes reuse of randomness and correlation visible, and an extensional layer obtained by interpreting tapes under a chosen probability measure. We develop an evidence-tracked tape semantics using the monadic-core-to-evidenced-frame pipeline (and its induced realizability tripos), obtaining a higher-order logic in which entailments are witnessed by uniform evidence transformers. Quantitative statements are recovered by interpretation: once a tape measure is fixed, probabilities and expectations arise by extracting numerical summaries from tape-indexed predicates, and entailments yield sound inequalities, with an almost-sure quotient supporting probability-one reasoning. We also study intensional principles that are lost at the level of laws, including proof-relevant transport along realizable tape-rewiring maps and a canonical splitting discipline for stream tapes enforcing independent draws. Finally, we relate tape-based reasoning to an extensional law semantics via pushforward, isolating a probability-one must abstraction as a sound summary of tape-based proofs.

ABSTRACT. The (bi)category of profunctors on groupoids is a categorification of the relational model of linear logic. Its objects are not just sets but rather sets whose elements are equipped with groups encoding their symmetries, and its morphisms carry actions by these symmetries. While detailed information on such symmetries helps, e.g., adequacy proofs of profunctorial models, it makes operations such as composition more difficult to compute. A way to ease the computation is to transform a profunctor into a matrix. Although the matrix representation is not functorial in general, it is known to behave well for profunctors definable by \( \lambda \)-terms. The mathematical reason behind this phenomenon, however, was not understood. This paper shows that the key is stability. Stability is a classical concept in domain theory, and has been extended to profunctors in Taylor's work and further developed by Fiore et al. All \( \lambda \)-definable profunctors are known to be stable, and we show that the matrix representation behaves well for stable profunctors. We prove that the matrix representation defines a functor from stable profunctors to matrices that preserves the linear logic structures.

ABSTRACT. Erasure enriches type theory with a distinction between runtime relevant and irrelevant data, allowing the compilation step to safely erase the latter. Versions of this feature are implemented by many systems, including Agda, Idris, and Rocq. We present a structural version of type theory with erasure, formulated as a second-order generalised algebraic theory (SOGAT). Erasure is encoded as a phase distinction between runtime and erased terms, in the form of a proposition that can appear in a context. This formulation has several advantages: it generates models based on categories with families, is compatible with other structural features such as staging, and provides a better guideline for implementation. Through the model theory of SOGATs, we study the semantics of type theory with erasure in families of sets, and more generally in Grothendieck toposes equipped with a tiny proposition. We establish conservativity over Martin-Löf type theory in both phases. For code extraction, we construct a presheaf model that produces untyped lambda calculus programs and prove its correctness through gluing. Our results are formalised in Agda and we provide a toy elaborator implementation.

ABSTRACT. Grassroots platforms are distributed systems with multiple instances that can (1) operate independently of each other and of any global resource other than the network, and (2) coalesce into ever larger instances, possibly resulting in a single global instance. Here, we present Grassroots Logic Programs (GLP), a multiagent concurrent logic programming language designed for the implementation of grassroots platforms. We introduce the language incrementally: We recall the standard operational semantics of logic programs; introduce the operational semantics of Concurrent (single-agent) GLP as a restriction of that of LP; recall the notion of multiagent transition systems and atomic transactions; introduce the operational semantics of multiagent GLP via a multiagent transition system specified via atomic transactions; and prove multiagent GLP to be grassroots. The accompanying programming example is the grassroots social graph---the fundamental grassroots platform on which all others are based. With the mathematical foundations presented here: a workstation-based implementation of Concurrent GLP was developed by AI, based on the operational semantics of Concurrent GLP; a distributed peer-to-peer smartphone-based implementation of multiagent GLP is being developed by AI, based on the operational semantics of multiagent GLP; a moded type system for GLP was implemented by AI, to facilitate the specification of GLP programs by human and AI designers, for their programming by AI; all reported in detail in companion papers.

ABSTRACT. Event-B is a formal method rooted in predicate logic and set theory. We encoded its over 600 proof rules in Prolog enabling a systematic, comprehensible proof analysis and construction. By integrating the proof rules into the Prolog-based validation tool ProB, we can bring the proof rules to life and obtain an interactive proof system with proof tree visualisation. This has advantages in teaching, enabling students to precisely control the application of proof rules. Our tool can import proof obligations from the Rodin platform and provides multiple exports: a trace file for proof replay in ProB, an interactive HTML document for tool-independent exploration of the proof tree, and an export back to Rodin, allowing the ProB prover to be used as second chain. Compared to the previous implementation of the proof rules in Java, the encoding in Prolog is much more compact, maintainable and extensible. In future we also hope to obtain fast automatic provers; a preliminary iterative deepening prover with simple heuristics is already available and useful for finding short proofs.

ABSTRACT. ProB is a Prolog-based model checker, animator and constraint solver for high-level formal spec ifications. It can also be used to animate transition systems defined by Prolog predicates, allowing the application of its various validation techniques. In this work, we present the existing features of ProB’s Prolog animation mode and its recent extensions. The extended capabilities include sim ulation for statistical checks, more reliable trace replay, transitions with user input and improved state visualisation. We apply the new features to case studies, particularly for evaluating different strategies in game play, such as Connect Four. The features are useful for many other applications, especially for ProB’s new sequent prover for Event-B proof obligations, as well as for demonstration models for teaching in combination with interactive visualisation.

ABSTRACT. Automated feedback tools for logic programming education depend on realistic bug datasets that reflect the mistakes students actually make. However, existing mutation testing frameworks for Prolog treat all mutations as equally likely, producing synthetic faults that diverge from classroom reality. We present an empirical study of 7,201 Prolog submissions from 265 undergraduate students, from which we derive a fine-grained taxonomy of student bugs through manual classification of 200 bug-fixing submissions. Guided by this taxonomy, we develop a data-driven mutation tool whose 17 operators are weighted according to the observed error distribution. The tool enumerates valid mutation sites on the abstract syntax tree, samples operators proportionally, injects faults, delegating to an SMT-based synthesizer when new code fragments are needed, and validates each mutant against a reference test suite. An evaluation of 16,000 generated mutants shows that the synthetic error distribution closely matches the student distribution, with most bug categories agreeing to within two percentage points. We identify cut-related mutations and synthesizer-generated code as the main sources of residual divergence, and outline how combining the SMT back-end with a language model fine-tuned on student code can further improve realism.

ABSTRACT. Providing personalized feedback is essential for effective learning, but delivering it promptly can be challenging in large-scale courses. In this work, we present ProHelp, an automated assessment platform for Prolog built on top of the GitSEED framework, and we evaluate it through a survey of 144 students from a 365-student undergraduate logic programming course. We assessed the perceived usefulness of seven types of automated feedback, including automatic testing, predicate scoring, syntax error highlighting, open choice point warnings, score rankings, solution type validation, and unknown predicate name suggestions. Our results show that 74% of students agreed the feedback helped increase their grade, and the system achieved a System Usability Scale score of 78.5 (grade B+). Among the feedback types, automatic testing was ranked as the most useful, followed by open choice point warnings and predicate scoring, with statistically significant differences. We found no significant effect of students' interest level, engagement with optional exercises, or use of large language models on their perception of feedback usefulness. We also explore student preferences for future feedback features, finding a significant preference for showing the differences between generated and expected test outputs.

ABSTRACT. Chess is a two player strategic game that is embedded in classical AI culture as it was once the frontier for intelligent behaviour. There was the silent assumption that the advent of computer engines that play better than the best humans will extinguish interest in the game. However, the opposite has come to pass, with a growing following for the game. A lot of the computational resources are now centered around training of players, where the engine output is just one aspect. Access to past games is also an essential part, both in knowing what games a specific player has played previously, and also which continuations at a certain position have led to victory more often for each of the two colour players. We present chess db a suit of logic programming tools that can effectively manipulate games both in memory and via creating back end databases. In particular, we provide versatile code that creates databases from PGN game files and explore the suitability of open source key-value databases for storing position tables that provide near- instant access to information pertaining to substantially large number of games.

ABSTRACT. Ninety-Nine Prolog Problems (P-99) is a famous set of Prolog exercises. We solved the first thirty three just by prompting an LLM (Large Language Model). We used Claude from Anthropic. By "solved'' we mean: generate the Prolog code and a test file, run the tests and check whether they pass, then formally prove types, groundness, termination, uniqueness, existence and also sometimes functional correctness with LPTP (Logic Program Theorem prover). Hence our approach is an experiment in vibe-coding/vericoding of P-99. It is a vibe-coding experiment because we started from informal specifications written in English and let Claude generate the Prolog code. It also fits within vericoding because the LLM proved reliability guarantees on the generated Prolog code. Claude wrote 58 logic procedures, 508 tests, 257 lemmas for a total of 11800 proof lines. We manually checked each file generated by the LLM. We checked the Prolog code, ran the tests, examined the logical statements generated by Claude and proof-checked Claude's proofs with LPTP. This paper describes this experiment and provides the main details so that it can be reproduced by the interested reader.

ABSTRACT. Abstract interpretation–based verification is a central component of the Ciao Prolog system, enabling expressive specifications of properties of programs, predicates, and execution states. Independently, the LPTP (Logic Programming Theorem Proving) framework offers a first-order logical formalism for expressing and proving properties of predicates. In this paper, we address the problem of relating these two frameworks by studying the translation of Ciao assertions into LPTP formulae and identify a partial correspondence between assertion-based and logic-based specifications. We introduce a systematic translation scheme, characterize assertion classes according to their logical encodability, and propose approximation strategies and auxiliary constructs for non-translatable cases. We analyze the resulting soundness and completeness trade-offs and demonstrate how the proposed approach enables a tight integration of Ciao’s assertion checking with LPTP-based deductive verification, thereby leveraging their complementary capabilities.

ABSTRACT. The Boolean Satisfiability (SAT) problem is a fundamental NP-complete problem. Algorithms for SAT include complete ones, typically based on Conflict-Driven Clause Learning (CDCL) methods, and incomplete ones, mostly following local search frameworks. CDCL solvers perform very well on complex structured instances. Local search (LS) algorithms cannot compete with CDCL solvers on structured instances, but show good performance on random and crafted instances, and also serve as an important component in top CDCL solvers. This raises a natural question: can techniques from complete SAT solving be used to improve incomplete solvers? This paper proposes the PASSAT (Progressive Activation Search for SAT) incomplete solver to answer it, which integrates the core techniques from both sides, Unit Propagation (UP) and LS. PASSAT starts from a subproblem, which relaxes many variables, and uses UP to progressively activate the search space (\ie, expand the subproblem). When a conflict is encountered, LS is invoked to repair it by searching all variables induced in the subproblem and the conflict. PASSAT ensures that the subproblem size increases monotonically and that the search process gradually approaches the full formula. In PASSAT, UP can guide growth direction based on the structure, and LS can efficiently repair conflicts. Their cooperation leads to some promising results. After a decade of evolution in CCAnr and ProbSAT variants, PASSAT represents a new incomplete algorithm framework with significantly better performance across various benchmarks.

ABSTRACT. We present graph backtracking, a novel, fine-grained backtracking scheme for CDCL-based SAT solving, parametrized by a user-defined weight function. For conflict repair, we challenge the decision level abstraction and use the implication graph as a precise guiding structure to minimize the weight of literals that are unassigned. Graph backtracking is sound, complete, and terminating. We show that it is a generalization of chronological and non-chronological backtracking by simulating them with specific weight functions. Our approach is implemented in the experimental solver NapSAT. Empirical results show that graph backtracking requires fewer literal propagations than standard approaches, leading to improved solver runtime.

ABSTRACT. Unsatisfiability proofs are valuable artifacts in propositional satisfiability (SAT) since they can provide correctness guarantees and thus complete trust in reported results. In powerful parallel and distributed clause-sharing SAT solvers, existing proof technology either funnels all solver threads' relevant reasoning steps into a single proof file, which leads to scalability problems for large setups and long running times, or checks proof information in parallel in real-time, which is fully scalable but leaves no persistent artifact. We suggest an alternative approach to achieve the best of both worlds. Specifically, we consider parallel proof files that are logged and also checked in parallel. To this end, we introduce PalRUP – an LRUP-based proof format and a bottleneck-free, decentralized parallel checking procedure that only uses the (parallel) file system and is composed of a set of small, sequential trusted components. In evaluations on up to 3072 cores, we observe that our approach allows for low-overhead proof logging during solving and substantially outscales prior proof producing approaches in terms of checking performance.

ABSTRACT. The propositional satisfiability (SAT) solver Kissat supports a relatively narrow feature set in favor of bare-metal performance and targeted improvements to core solving techniques, which helped it dominate the International SAT Competition since 2024. However, many applications rely on advanced SAT solver features such as incremental interaction schemes, finding direct consequences of assumed literals, or expressive proof logging that allows for real-time checking. This system description reports on how we successfully adapted Kissat's award-winning techniques to the full-featured incremental SAT solver CaDiCaL, including clausal congruence closure, clausal equivalence sweeping, and bounded variable addition. The main challenge was to support efficient linear proof production with hints. We further extended CaDiCaL's API to extract implied literals under assumptions and applied advanced deterministic scheduling of inprocessing based on the ticks metric for approximating cache line accesses. Experiments confirm the benefits of these efforts.

ABSTRACT. Many SAT benchmark datasets contain structurally identical instances, either due to repeated shuffling or duplication by generators. We present an efficient, open-source, isomorphism-invariant hashing algorithm for SAT instances, based on Weisfeiler--Leman (WL) label refinement. Each instance is represented as a bipartite clause--literal graph, and iterative label refinement computes a canonical signature, with instances having identical signatures treated as isomorphic. When integrated into our benchmark toolset, the method eliminates false positives produced by a previous naive approach based on sorted sequences of literal degrees, with minimal runtime overhead, demonstrating that WL-based hashing enables more accurate isomorphism detection and reliable benchmarking.

ABSTRACT. Datalog is a powerful rule-based language with numerous applications in databases and knowledge representation and reasoning. Explaining why a fact belongs to the output of a Datalog program over a database is an essential task towards explainable and transparent data-intensive applications. A standard way of explaining a fact is the so-called why-provenance, which provides witnesses in the form of subsets of the input database that as a whole can be used to derive that fact. The notion of why-provenance for Datalog is naturally obtained from the proof-theoretic semantics of Datalog, where the output of a Datalog program over a database is the set of facts that admit a proof tree, and the set of database facts that label the leaves of this tree forms a why-provenance explanation. While why-provenance for Datalog has been extensively studied in the literature, the analogous notion for Datalog with negation remains unexplored. Our goal is to study why-provenance for Datalog with negation under the standard well-founded and stable model semantics inherited from Logic Programming. To this end, we use the machinery of justification theory, originally introduced for the study of inductive definitions and later adopted as a unifying framework for the semantics of a wide range of non-monotonic logics, including logic programs, to define the proof-theoretic semantics of Datalog programs with well-founded and stable model semantics, which then leads to natural notions of why-provenance. To the best of our knowledge, this is the first time that the proof-theoretic semantics of Datalog programs with well-founded and stable model semantics are made explicit and used for explainability purposes. We then perform a thorough data complexity analysis of the problem of why-provenance for Datalog with negation and show that it is in general intractable for both well-founded and stable model semantics; in particular, it is NP-complete, which is the best that we can hope for since the problem is already NP-hard for Datalog without negation. Interestingly, the machinery for why-provenance allows us also to study the notion of why-not-provenance for Datalog with negation under the well-founded and stable model semantics.

ABSTRACT. Several applications demand the timely detection of critical situations, such as threats to safety and transparency, over high-velocity streams of symbolic events. This demand has motivated the development of (i) event specification formalisms, which define composite events via temporal patterns over simpler events, and (ii) stream reasoning frameworks tailored to fragments of these formalisms. However, event specification formalisms are typically studied in isolation, complicating their comparison in terms of expressivity and obscuring the scope of their associated stream reasoners. To mitigate this issue, we map practical fragments of prominent event specification languages into a temporal extension of Datalog with stratified negation. To support efficient stream reasoning over this Datalog variant, we propose Temporally Stratified Trigger Graphs (TSTGs), an extension of a state-of-the-art technique for Datalog materialisation. Our approach yields a uniform composite event recognition mechanism that generalises across event specification languages and achieves high efficiency in practice, with performance competitive with well-established stream reasoners.

ABSTRACT. We present a translation of DatalogMTL, a temporal extension of the Datalog rule language with operators from metric temporal Logic (MTL), into standard, non-temporal Datalog with arithmetics. As we prove, the translation preserves such key semantic properties as entailment, consistency, and finiteness of materialisability. As a result, our approach yields a faithful embedding of DatalogMTL into classical Datalog, enabling complex temporal reasoning tasks to be executed without the need for specialised temporal reasoning engines. We implement and evaluate our translation using three state-of-the-art Datalog systems: Nemo, EYE and Eyelet. Remarkably, non-temporal Datalog engines are able to out-perform dedicated temporal reasoning engines on their own turf, demonstrating the practical viability and efficiency of our approach.

ABSTRACT. The chase is a sound, complete, but possibly non-terminating algorithm for reasoning with existential rules (aka. tuple-generating dependencies), a highly expressive knowledge representation language. Although the procedure appears simple, research on theoretical properties and optimization for practical implementations has grown to a point where verifying correctness and reproducing proofs becomes challenging and intuition can sometimes be misleading. Lean is a purely functional programming language and interactive theorem prover whose community actively develops formal libraries for mathematics (Mathlib) and computer science (CSLib). In this work, we present our own endeavor of crafting a Lean framework around existential rules and the chase. We discuss design decisions concerning the nuances of chase definitions commonly found in the literature and show how these translate into Lean. To illustrate the framework’s capabilities using known results, we show that the result of a chase is a universal model and outline the formalization for proving that without so-called “alternative matches” it is even a core. Beyond existing literature, we unify sufficient chase termination conditions in the likeness of Model-Faithful Acyclicity (MFA) into a common framework while also adding support for constants in rules.

ABSTRACT. Decision-making in real-world settings rarely follows a fixed script. Instead, it unfolds as a dynamic reasoning process in which the appropriate course of action evolves as new context and data become available. Traditional Business Process Management systems provide rigor, determinism, and auditability, yet they generally struggle to adapt their execution at runtime. Conversely, agentic systems based on Large Language Models (LLMs) bring flexibility to decision-making, but they are inherently opaque, often unreliable, and suffer from significant scalability constraints when operating over large datasets. To combine these complementary paradigms, we introduce VADAOrchestra, a neurosymbolic framework that models complex workflows as evolving reasoning processes. The framework adopts a hybrid approach: given a user query and a collection of data sources, an LLM-based orchestrator incrementally plans and adapts the workflow. This is encoded as a logic program in a fragment of Datalog+/- where predicates correspond to tool invocations and rules represent both predefined domain dependencies and logic constructs synthesized on demand to manipulate intermediate results. All logical inference tasks are then executed by a state-of-the-art Datalog+/- symbolic engine. This approach provides a verifiable reasoning trace, supporting the auditability and reproducibility of the entire process. Furthermore, by decoupling high-level orchestration from symbolic inference, it addresses scalability concerns, enabling complex reasoning over large datasets through targeted data querying. We evaluate VADAOrchestra on real-world financial use cases, demonstrating faithfulness, scalability, and explainability compared to standard agentic architectures.

ABSTRACT. PDDL 2.1 is the community standard for specifications of temporal planning problems, involving actions that have a duration and can overlap in time. Recent work has shown that some modelling features, such as intermediate and conditional effects, can be expressed in PDDL 2.1 by means of specific encodings. At the core of these encodings is a construction that requires two events to happen simultaneously. However, in practice, almost none of the state-space heuristic search planners known in the literature are capable of finding plans exhibiting this required simultaneity, suggesting that the search approach they use is actually incomplete with regards to the official PDDL 2.1 semantics. In this paper, we explore this issue both theoretically and experimentally. On the theoretical side, we define two different notions of required simultaneity, and we isolate which features of the semantics of PDDL 2.1 allow for such behaviors and how to possibly change the semantics to forbid each of them. In particular, we prove that the crucial detail is how the over-all conditions interact with the mutex relation. From these observations we isolate the reason why most search-based planners cannot find plans with required simultaneity, and provide an updated search strategy that recovers semantic completeness at the cost of a larger branching factor which, however, can be suitably pruned thanks to an application of our results. On the experimental side, we compare the proposed search strategies, showing that our pruning criterion allows us to recover semantic completeness without significant overhead.

ABSTRACT. Autonomous agents' goals typically change as they operate. Handling this is particularly challenging when the environment is nondetermnistic and the goals are temporally extended. In this paper, we assume that the agent operates in a fully observable nondeterministic (FOND) domain and uses Linear Temporal Logic over finite traces (LTLf) to represent goals. We use LTLf synthesis notions to formalize this problem of online agent goal management, handling goal adoption, goal dropping, and performing steps of the synthesized strategy, while ensuring that the agent's goals always remain realizable. We propose automata-based and formula progression-based methods to manage LTLf goals. We implement these methods and evaluate their effectiveness experimentally.

ABSTRACT. LTLf synthesis under partial observability requires reasoning about unobservable environment variables, which is typically handled by constructing a belief-state DFA via subset construction that universally quantifies these variables. Existing approaches perform this construction as a separate step prior to game solving, often generating belief states that are unnecessary in practice. We propose an on-the-fly approach to LTLf synthesis under partial observability based on observable progression. Our method incrementally builds the belief-state DFA by progressing the specification with respect to observable variables only, universally quantifying unobservable variables on the fly. We prove the correctness of the construction and show that it naturally enables on-the-fly game solving, leading to a fully on-the-fly synthesis framework. Our implementation leverages DFAs represented using Multi-Terminal Binary Decision Diagrams: a compact representation that has proven highly effective for LTLf synthesis under full observability. Experimental results demonstrate that our approach significantly outperforms existing methods and further highlight the practical benefits of integrating on-the-fly game solving with belief-state construction.

ABSTRACT. Golog programs over Situation Calculus action theories were introduced as a specification of desired agent behavior, very much like temporally extended goals in planning, but with a focus on procedural aspects typical of programs. In the words of the original paper: "Golog allows the programmer to strike a compromise between the often computationally infeasible classical planning task, in which a plan must be deduced entirely from scratch, and detailed programming, in which every little step must be specified." In this paper, we study temporal synthesis with Golog programs as specifications over nondeterministic propositional action theories. We show that Golog has the same expressive power as linear dynamic logics on finite traces (LDLf), namely that of regular languages or monadic second-order logic (MSO) over finite traces, while exhibiting a markedly lower synthesis complexity: synthesis can be performed by constructing a polynomial-size program graph and taking its cross-product with the domain, whereas LDLf synthesis requires building a deterministic automaton of worst-case doubly exponential size. This advantage is confirmed experimentally.

ABSTRACT. The Optimal In-Station Train Dispatching (InSTraDi) problem consists in commanding the movements of trains inside a railway station while both (i) respecting safety, time, and travel constraints and (ii) minimizing delays. In Symbolic Pattern Planning (SPP), a pattern, suggesting the sequence of happenings to reach the goal, is encoded in a logic formula whose models correspond to valid plans. If no valid plan is found, the pattern is extended until it covers a valid plan. However, plans of better quality could exist if we had continued extending the pattern. In this paper, we formalize the InSTraDi problem as a Temporal Planning Task with Intermediate Conditions and Effects, and we show an InSTraDi-dependent way to construct, in polynomial time, a pattern ensuring the optimal plan can be found by the SPP approach without never extending the pattern. Analysis on realistic railway data validate our approach.

ABSTRACT. Neuro-symbolic AI aims to integrate learning-based and symbolic reasoning components within a unified framework. While most existing work focuses on single-agent settings and engineering architectures, formal foundations for neuro-symbolic multi-agent systems remain limited. In this paper, we introduce a game-theoretic formal model capturing the interaction between probabilistic neural evaluation and symbolic strategic reasoning in multi-agent environments. The framework extends logical models of strategic reasoning while embedding probabilistic propositional inference into a distributed setting. We establish basic properties of the model and provide a comprehensive complexity-theoretic analysis of optimally stable strategic behaviour. In particular, for one-shot games, we show that utility evaluation corresponds to weighted model counting and characterise the complexity of the main associated Nash equilibrium problems, ranging from FP and #P to PP and Sigma^PP_2. We further study an iterated variant of the core model, showing PSPACE-completeness for the main decision problem in such a class of multi-player games. These results provide formal foundations for reasoning about neuro-symbolic multi-agent systems and clarify the computational limits of combining learning, uncertainty, and strategic interaction within the same framework.

ABSTRACT. Despite the remarkable progress in neural models, their ability to generalize—a cornerstone for applications like logical reasoning—remains a critical challenge. We delineate two fundamental aspects of this ability: compositionality, the capacity to abstract atomic logical rules underlying complex inferences, and recursiveness, the aptitude to build intricate representations through iterative application of inference rules. In the literature, these two aspects are often confounded together under the umbrella term of generalization. To sharpen this distinction, we investigated the logical generalization capabilities of pre-trained large language models (LLMs) using the syllogistic fragment as a benchmark for natural language reasoning. We extend classical Aristotelian syllogistic forms to build more complex structures, providing a foundational yet expressive subset of formal logic that supports controlled evaluation of essential reasoning abilities. Our findings reflect this non-trivial benchmark: while LLMs demonstrate reasonable proficiency in recursiveness, they struggle with compositionality. This disparity, however, is not uniform, as a more detailed analysis reveals variability in generalization performance across individual syllogistic types, ranging from near-perfect to significantly lower accuracy. To overcome these limitations and establish a reliable logical prover, we propose a hybrid architecture integrating symbolic reasoning with neural computation. This synergistic interaction enables robust and efficient inference—neural components accelerate processing, while symbolic reasoning ensures completeness. Our experiments show that high efficiency is preserved even with relatively small neural components. As part of our proposed methodology, this analysis provides a rationale and highlights the potential of hybrid models to effectively address key generalization barriers in neural reasoning systems.

ABSTRACT. Reinforcement Learning (RL) provides a principled framework for sequential decision-making in complex environments. However, state-of-the-art Deep Reinforcement Learning (DRL) algorithms typically require large amounts of training data and often fail to generalize beyond small-scale training scenarios, even on standard benchmarks. We propose a neuro-symbolic DRL approach that incorporates background symbolic knowledge to improve both sample efficiency and generalization to more challenging, unseen tasks. Specifically, partial policies learned in simple domain instances, where high performance can be achieved reliably, are transferred as structured priors to accelerate learning in more complex environments, eliminating the need to tune DRL parameters from scratch. Our method represents partial policies as logical rules in the Answer Set Programming (ASP) formalism and performs online reasoning to guide training through two complementary mechanisms: (i) biasing the action distribution during exploration, and (ii) rescaling Q-values during exploitation. This integration of ASP reasoning with DRL enhances interpretability and trustworthiness while accelerating convergence, particularly in sparse-reward settings and tasks with long planning horizons, without introducing significant computational overhead. We empirically evaluate our approach on challenging variants of gridworld environments under both fully and partially observable settings. Results demonstrate consistent performance improvements over a state-of-the-art reward machine baseline.

ABSTRACT. Large language models (LLMs) are increasingly used to control embodied agents by mapping natural-language commands to high-level actions. While this paradigm enables flexible human--robot interaction, it also introduces significant safety risks, as LLM-generated commands are not guaranteed to respect physical, environmental, or mission-critical constraints. In this paper, we present an application of \emph{reactive synthesis modulo theories} to the real-time guardrailing of an LLM-controlled quadruped robot, using the first-order theory of bitvectors as a symbolic abstraction of the robot's action space and environment. Our system translates natural-language commands into discrete bitvector-encoded actions, which are then filtered by a formally synthesized guardrail (also called \textit{shield}) that enforces safety and liveness properties expressed in Linear Temporal Logic modulo bitvector constraints. The shield operates online and corrects unsafe commands while preserving the intent of the human operator. We instantiate our framework in a realistic locomotion setting, inspired by recent work on language-driven robot control, and demonstrate that the robot maintains safety under adversarial and dynamic environmental conditions. This work illustrates how theory-aware synthesis can serve as a practical foundation for trustworthy human--robot interaction, enabling the deployment of learning-based controllers in safety-critical settings with formal guarantees.

ABSTRACT. Attributing business fluctuations to actionable drivers is a critical component of decision-making in high-stakes domains. However, prevailing predictive models, predominantly driven by correlations, often yield inconsistent explanations that degrade under distribution shifts or latent confounding. Empirical causal inference to address this limitation remains challenge due to the identifiability gap in purely data-driven discovery and the complexity of encoding domain knowledge into differentiable learning pipelines. To bridge this gap, we propose Neuro-Symbolic Causal Boosting, a unified framework that integrates semantic domain priors with gradient-based causal estimation. First, we introduce the Complete Cause Identification Algorithm (CCIA). Unlike global search methods, CCIA recursively reconstructs the ancestral causal graph of the target variable by employing Kolmogorov-Arnold Networks (KANs) as high-precision filters for low-order independence testing, coupled with a neuro-symbolic adjudication based on Large Language Model to resolve directionality. Subsequently, the identified structure scaffolds the Causal Additive Boosting Network (CABN). Grounded in the theory of structural identification, CABN enforces a reverse topological learning process. It utilizes weighted KANs to sequentially estimate downstream effects and adjust for confounding, thereby isolating invariant causal mechanisms. Empirical evaluation on a real-world telesales dataset and synthetic benchmarks demonstrates that our framework achieves a 57.5% reduction in Out-of-Distribution prediction error compared to strong correlation-based baselines. Additionally, it identifies and quantifies the impact of actionable drivers, providing a structured approach from observational data to trustworthy and interpretable business strategies.

ABSTRACT. Coherent control, aka quantum control, is a central concept in quantum computing that is attracting increasing attention from both the quantum foundations and quantum software communities. Defining coherent control in the presence of recursion and measurement has long been known to be a major challenge. In particular, no-go results have been established for standard semantical domains like completely positive maps. We address this problem by introducing the first quantum programming language with recursion that allows for the coherent control of arbitrary quantum operations. We equip this language with both an operational and a denotational semantics that we prove to be adequate. To design these semantics, we show that combining coherent control, recursion, and measurement crucially requires describing the evolution of subprograms in the absence of input. To address this, the operational semantics takes into account a default evolution branch, while the denotational semantics uses the concept of coherent quantum operation, based on vacuum extensions. We strengthen the validity of our approach by developing an observational equivalence: two programs are equivalent if their probability of termination is the same in any context. The denotational semantics is shown to be fully abstract with respect to this observational equivalence.

ABSTRACT. Indefinite causal order is a characteristic phenomenon in quantum computation, with examples including the quantum SWITCH and the OCB process. Not all such processes are believed to be physically realizable: while some implementations of the quantum SWITCH have been proposed, the OCB process is suspected to be unrealizable. This difference in realizability is commonly attributed to constraints imposed by physical causality. This paper studies such a causality issue in a higher-order setting, proposing a typed lambda calculus with quantum control and its categorical semantics. Our calculus extends pure quantum computation with higher-order functions and quantum conditional branching, and it is equipped with a type system based on intuitionistic BV logic to enforce causality. We also present a novel model that is closely related to the Caus construction, by which we prove that some physically-unrealizable processes are not definable in our language.

ABSTRACT. Controlled commands---computations whose execution depends on a separate input---play a central role in reversible Boolean circuits and quantum circuits. However, existing formalisms typically treat control only implicitly, entangled with other aspects of computation. From a semantic perspective, control is most naturally expressed in semisimple rig categories, which---unlike standard circuit models such as props---support both parallel and conditional composition. We present a construction that freely adjoins an explicit syntactic notion of control to a circuit theory specified as a suitable prop, subject to eight universally quantified equations. Our main result is that these equations are sound and complete for the intended semantics of control: the resulting theory satisfies a universal property, identifying it exactly as the circuit subtheory of the free semisimple rig completion. The proof combines coherence for rig categories with a new method based on induction over Gray codes. We illustrate the usefulness of the framework by showing that it simplifies several existing sound and complete axiomatisations of quantum circuits, isolating a small and conceptually clean set of generators and equations. In addition, the same equations yield a sound and complete axiomatisation of the multiply controlled Toffoli gate set, that is universal for reversible Boolean circuits.

ABSTRACT. Finite-state dimension, introduced as a finite-state analogue of Hausdorff dimension, quantifies the lower asymptotic density of information in an infinite sequence as perceived by finite-state automata. It admits several equivalent formulations; two particularly useful are via finite-state gambling strategies and via the optimal asymptotic compression ratio achieved by information-lossless finite-state compressors. Normal sequences represent the highest level of algorithmic randomness visible to finite automata, and are exactly those sequences having finite-state dimension equal to $1$. This motivates a bounded-memory notion of randomness extraction: can a finite-state transducer, reading a single sequence streamingly, extract a normal output from a single input source? More modestly, can it always transform the input into an output of strictly higher finite-state dimension? Finite-state transducers can perform surprisingly effective one-pass transformations: even with constant memory they can implement variable-length coding schemes including Shannon--Fano coding, remove local redundancy, and increase the apparent randomness rate on many structured or stochastic inputs. We show randomness extraction using transducers is impossible in a strong, explicit form. For every rational $s \in (0,1)$, we construct a near linear-time computable binary sequence $X$ with $\dim_{\mathrm{FS}}(X)=s$ such that for every finite-state transducer $T$, the output satisfies $\dim_{\mathrm{FS}}(T(X)) \le s$. Thus, for these sequences, finite-state transduction cannot extract normality---indeed it cannot even improve finite-state dimension. Our proof proceeds by a structural analysis of finite-state transducers together with a dimension-preserving diagonal construction that, for each target $s$, builds a sequence whose organization defeats every such transducer's attempt to concentrate randomness. The result is a finite-state analogue of Miller's non-extractability phenomenon for effective dimension, but its proof relies on substantially different techniques, tailored to the finite-state setting. Furthermore, we show that the impossibility persists even with multiple independent input streams. We treat two notions of independence: (i) Kolmogorov-complexity–based independence (via joint prefix complexity), and (ii) a finite-state notion of relative independence, formulated via relative finite-state dimension. By sharp contrast with the effective-dimension setting—where two independent sources suffice for a uniform effective procedure that boosts randomness rate arbitrarily close to~$1$—we show that finite-state dimension exhibits no comparable multi-source extraction phenomenon. Specifically, for every rational $s\in(0,1)$ and every fixed $k\ge 2$, there exist $k$ independent sources, each of finite-state dimension~$s$, such that for every $k$-input finite-state transducer $T$, the output satisfies $\dim_{\mathrm{FS}}(T(X_1,\dots,X_k))\le s$. Thus, even independent streams do not allow bounded-memory transduction to output a normal sequence or to increase finite-state dimension.

ABSTRACT. We study contextual interactions in an ML-like language equipped with general references and continuations, focusing on the reachability and approximation problems. Previous work addressed higher-order programs with first-order references in the absence of loops using automata over nested data; however, extending these techniques to programs with loops encountered fundamental technical obstacles, stemming from the need to bound the depth of data. We introduce a new class of automata over infinite alphabets that supports unbounded nesting of data. We establish a precise correspondence between these automata and higher-order programs with loops: the trace semantics of any such program can be captured by an automaton, and conversely, the trace language of any such automaton can be realised by an imperative higher-order program with loops. This correspondence enables the transfer of decidability and undecidability results between the automata and programs. In particular, we show that adding loops preserves decidability of reachability, while rendering approximation undecidable.

ABSTRACT. It has been conjectured that the Parikh (commutative) image of every language over an infinite alphabet recognized by an automaton with registers is defined by a rational expression. This conjecture is known to hold for all languages recognized by one-register automata. We refine this result by proving that the star-height of the Parikh image of any language recognized by a one-register automaton is universally bounded by two. Furthermore, we show that one-register context-free languages have rational commutative images of arbitrarily high star height. We then disprove the conjecture for multiple registers, as well as disprove the equivalence of commutative expressive power between context-free grammars and automata over infinite alphabets.