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. 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. 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.