ABSTRACT. We explore a fuzzy modal logic that can formalise probabilistic reasoning about actions and knowledge. In particular, we deal with contexts involving statements about events expressed via modal formulas, e.g., ‘after doing~a, the probability of A~knowing that p holds increases / decreases / is equal to 0.25’, ‘according to A, p is equally likely to happen after doing a or b’, etc. We define the semantics of the logic on Kripke frames equipped with probability measures. We analyse the complexity of deciding the satisfiability of formulas of our logic over finitely branching models for the cases of the full language and its fragments of various expressivity.

ABSTRACT. We study the problem of explaining observations about the probabilities of events such as ‘it rains 20% of the time’, ‘rain and snow are equally likely’, etc. We explain these statements with a probability distribution or a statement about probabilities of (other) events that are consistent with our knowledge and entail the observation. We formalise this problem in a fuzzy probabilistic logic FP. We define and motivate the notions of abduction problems and their solutions. We analyse the complexity of solution recognition and existence for a given abduction problem in FP for the case of full language and its disjunctive-clause fragments. We also obtain a translation of classical probabilistic abduction (finding the most likely explanation of a given event) to FP.

ABSTRACT. Goal recognition aims to infer an agent’s goal from observations of its behaviour. In realistic settings, recognition can benefit from exploiting hierarchical task structure and reasoning under uncertainty. Planning-based goal recognition has made substantial progress over the past decade, but to the best of our knowledge no existing approach jointly integrates hierarchical task structure with probabilistic inference. In this paper, we introduce the first planning-based probabilistic framework for hierarchical goal recognition over Hierarchical Task Networks (HTNs). We instantiate the framework by exploiting an HTN planner with a three-stage generative model for likelihood estimation, yielding posterior distributions over goal hypotheses. Empirical results show improved recognition performance over the existing HTN-based recognizer on HTN benchmarks. Overall, the framework lays a foundation for probabilistic goal recognition grounded in hierarchical planning structure, moving goal recognition toward more practical settings.

ABSTRACT. Recent work by Chatzi et al. and Ravfogel et al. has developed, for the first time, a method for generating counterfactuals of probabilistic Large Language Models. Such counterfactuals tell us what would - or might - have been the output of an LLM if some factual prompt x had been x* instead. The ability to generate such counterfactuals is an important necessary step towards explaining, evaluating, and eventually improving, the behavior of LLMs. We argue, however, that the existing method rests on an ambiguous interpretation of LLMs: it does not interpret LLMs literally, for the method involves the assumption that one can change the implementation of an LLM's sampling process without changing the LLM itself, nor does it interpret LLMs as intended, for the method involves explicitly representing a nondeterministic LLM as a deterministic causal model. We here present a much simpler method for generating counterfactuals that is based on an LLM's intended interpretation by representing it as a nondeterministic causal model instead. The advantage of our simpler method is that it is directly applicable to any black-box LLM without modification, as it is agnostic to any implementation details. The advantage of the existing method, on the other hand, is that it directly implements the generation of a specific type of counterfactuals that is useful for certain purposes, but not for others. We clarify how both methods relate by offering a theoretical foundation for reasoning about counterfactuals in LLMs based on their intended semantics, thereby laying the groundwork for novel application-specific methods for generating counterfactuals.

ABSTRACT. Knowledge Compilation (KC) is a powerful paradigm that enables efficient reasoning by transforming propositional formulas into tractable target languages, such as Deterministic, Decomposable Negation Normal Form (d-DNNF). However, as real-world problem instances grow in complexity, the offline compilation phase becomes a significant computational bottleneck, often exceeding the memory and temporal limits of single-node systems. While distributed computing has been successfully applied to model counting (#SAT), extending these techniques to knowledge compilation remains a challenge due to the difficulty of sharing partial circuit fragments across distributed nodes. In this paper, we propose dkc, the first distributed knowledge compiler designed for large-scale Decision-DNNF generation.Leveraging a Cube-and-Conquer strategy, dkc effectively partitions the search space into independent subproblems, mitigating the communication overhead typically associated with work-stealing architectures in circuit-based tasks. Recognizing that the utility of compilation lies in subsequent querying, we further introduce dreasoner, a distributed reasoning engine. dreasoner is capable of performing core inference tasks (including model counting, direct access, and uniform sampling) across a distributed d-DNNF structure, even under variable conditioning. Our experimental evaluation on benchmarks demonstrates that our distributed architecture scales effectively, enabling the compilation and querying of complex formulas that remain beyond the reach of state-of-the-art sequential compilers.

ABSTRACT. Tensor networks and circuits are widely used data structures to represent pseudo-Boolean functions. These two formalisms have been studied primarily in separate communities, and this paper aims to establish equivalences between them. We show that some classes of tensor networks that are appealing in practice correspond to classes of circuits with specific properties that have been studied in knowledge compilation as \emph{tractable circuits}. In particular, we prove that matrix product states (tensor trains) coincide with nondeterministic edge-valued decision diagrams and that tree tensor networks exactly correspond to structured-decomposable circuits. These correspondences enable direct transfer of structural and algorithmic results; for example, canonicity and tractability guarantees known for circuits yield analogous guarantees for the associated tensor networks, and vice versa.

ABSTRACT. Non-monotonic reasoning is essential for drawing plausible conclusions from incomplete information. Many approaches model changing belief states using Ordinal Conditional Functions (OCFs), which assign degrees of surprise to possible worlds. This paper demonstrates how OCFs are ideally suited for the knowledge compilation paradigm, particularly with Binary Decision Diagrams (BDDs). We introduce a compilation pipeline for System Z, a prominent ranking-based semantics, which pre-compiles a conditional knowledge base into a set of materialized theories represented by BDDs. This compilation enables polynomial-time conditional entailment and efficient, incremental updates, avoiding costly re-computation. We further extend this approach using Algebraic Decision Diagrams (ADDs) to directly compile the entire ranking function, facilitating direct and efficient implementation of complex belief revision operations such as Spohn conditioning.

ABSTRACT. We present a knowledge compilation approach for existential and universal quantification in alternating automata. Knowledge compilation transforms formulas into normal forms with special properties that enable efficient answering of questions of interest. For Boolean formulas, several normal forms that have proven effective for existential/universal quantification, and even for functional synthesis, have been studied in the literature. For infinite word automata, quantification is a fundamental operation in verification tasks such as QPTL satisfiability checking and HyperLTL model checking. Existing algorithms rely on nondeterministic infinite word automata, where existential projection can be efficiently performed state-wise, but universal projection requires complementation. Complementing nondeterministic infinite word automata, however, is expensive in practice, making existing algorithms infeasible for automata in practice. Towards addressing this problem, we propose novel knowledge compilation techniques for existential and universal quantification on alternating safety automata. Our approach compiles alternating automata into normal forms where projection can be applied uniformly and efficiently to each state's transition function. Using the compilations for each type of quantification, we can effectively eliminate a sequence of alternating quantifiers in formulas without complementation. Our BDD-based prototype demonstrates the practical effectiveness of our algorithms on a suite of QPTL satisfiability benchmarks.

ABSTRACT. We present a new approach for computing complete, stable and preferred extensions of abstract argumentation frameworks. Unlike existing approaches that reduce these problems to the propositional satisfiability problem and solve them with the help of SAT-solvers, our approach solves them directly by making use of the fact that the mentioned extensions are contained in certain closure systems. Our algorithms enumerate these closed sets and filter the searched extensions. Experimental results show that our approach outperforms the existing approaches for a large number of the test cases.

ABSTRACT. In Dung-style abstract argumentation, various semantics capture notions of acceptability of arguments. The admissibility semantics capture the notion that an argument can be consistently defended from any potential counterargument. Weak semantics often relax the demands of admissibility by restricting which counterarguments must be taken seriously (e.g., discounting self-defeating or otherwise incoherent attacks). Many prominent proposals for weak semantics remain extension-based in a stronger sense. While these semantics discount attacks from arguments which are considered unreasonable, they still require a uniform defense against all reasonable arguments, even if they are collectively incoherent. This uniformity can be too demanding when defensibility is inherently strategic, and thus the appropriate reply depends on the opponent’s line of attack. We introduce tenability, a family of dialogue-based semantics that formalize when a designated argument (or a set of arguments) can be maintained in debate by a proponent against any coherent (conflict-free) attack which the opponent may present. The approach is motivated by three natural benchmark patterns—self-defeating attack, floating assignment, and disjunctive reinstatement—on which tenability behaves differently from all weak semantics previously considered in the literature. We define three variants--static tenability, tenability, and strong tenability--via monotone commitment games over finite conflict-free moves, differing in the obligations imposed on the disputants. We establish the relative strength of these notions, prove implications and separations with previously studied weak semantics, and % (including admissibility) we analyze computational complexity on finite frameworks: deciding static tenability is $\Pi^P_2$-complete, while deciding tenability and strong tenability is PSPACE-complete.

ABSTRACT. Argumentation theory provides a formal framework to represent and analyse debates where participants propose arguments that attack or support others and assign scores expressing their opinions. Quantitative Bipolar Argumentation Frameworks model such debates by assigning initial weights to arguments and using semantics to compute final scores that reflect attackers’ and supporters’ influence. One of the major challenge is setting appropriate initial weights when debaters’ opinions are uncertain. In this paper, we introduce a formal approach to uncertainty propagation in Quantitative Bipolar argumentation frameworks by representing initial weights as belief mass functions over a discretized unit interval. We introduce two new propagation models: (i) an exact model that computes final mass functions by combining focal elements of initial weights with parent arguments via bipolar gradual semantics; (ii) a practical approximation that projects the exact mass onto a user-specified partition and reconstructs masses using the Moebius inverse. We prove mathematical properties of the projection and show that the baseline, while computationally efficient, can be overconfident by failing to preserve expectations. Our approximation reduces the exponential complexity of the exact model while satisfying Epistemic Cautiousness, yielding acceptability intervals that contain true theoretical expectations and balancing tractability with theoretical soundness.

ABSTRACT. Contestable AI requires that AI-driven decisions align with given preferences. Various types of argumentation frameworks have been shown to support forms of contestability. In this paper we focus on the little-studied Edge-Weighted Quantitative Bipolar Argumentation Frameworks (EW-QBAFs), where arguments have a base score as in QBAFs but attacks and supports (edges) are weighted. After generalising gradual semantics and properties thereof from QBAFs to EW-QBAFs, we introduce the contestability problem for EW-QBAFs, which asks how to modify edge weights to achieve a desired strength for a specific topic argument. To address this problem, we propose gradient-based relation attribution explanations (G-RAEs), which quantify the sensitivity of the topic argument's strength to changes in individual edge weights, thus providing interpretable guidance for weight adjustments towards contestability. Building on G-RAEs, we develop a heuristic algorithm that progressively adjusts the edge weights to attain the desired strength. We evaluate our approach experimentally on synthetic EW-QBAFs that simulate the structural characteristics of personalised recommender systems and multi-layer perceptrons, demonstrating that it can support contestability effectively.

ABSTRACT. Autonomous agents acting in realistic Multi-Agent Systems (MAS) should be able to adapt during their execution. Standard strategic logics, such as Alternating-time Temporal Logic (ATL), model agents' state or history-dependent behaviour. However, the dynamic treatment of agents' available actions and their knowledge of required actions is still rarely addressed. In this paper, we introduce ATL with Dynamic Actions (ATL-D), which models the process of granting and revoking actions, and its extension ATEL-D, which captures how such updates affect agents’ knowledge. Beyond the conceptual contribution, we provide several technical results: we analyse the expressivity of our logic in relation to ATL, study its relation to normative systems, and provide complexity results for relevant computational problems.

ABSTRACT. We study an Agentic AI setting where we have only partial control over the strategic actions of a set of autonomous agents with independent sequential decision-making capabilities, building on LTL synthesis originally studied in formal methods. Specifically, we assign to each agent individually a task expressed in LTL, and assumptions on the strategies employed by its peers and that the agent can exploit while synthesizing a strategy to realize its task. While we can solve the synthesis problem under assumptions for each such agent we are not only interested in (1) synthesizing strategies for individual agents. Indeed, assumptions in turn are recursively defined through these strategy spaces. Importantly, we do not assume the ability to access or analyze an agent's internal strategy, as we make no assumptions about the nature of the decision makers, which may be, for example, ML-based. Instead, we focus on (2) characterizing the set of traces that are generated by strategies that realize the specification assigned to each agent. Using this characterization, we are able to (3) verify that the whole system, when in execution, satisfies a global objective, regardless of the strategies chosen by the agents from their allowed spaces. Moreover, by observing the evolution of the execution trace, we can (4) identify whether an agent makes a move that violates its specification and assign precise responsibility for the violation. Technically, we present automata-theoretic techniques to solve these problems, and show that each of them is 2EXPTIME-complete, matching the complexity of classical LTL synthesis.

ABSTRACT. Bisimulation is a crucial tool for investigating and understanding the semantic properties of labeled transition systems (LTSs) and relational models in general. In particular, it plays a fundamental role in characterizing model equivalence with respect to a given logical language and in guiding the construction of minimal models. In this paper, we study bisimulation in the context of a logic for expressing knowing-how assertions, which are related to an agent's ability to achieve a given goal. We begin by revisiting an existing notion of bisimulation for this logic and reformulating it using purely semantic clauses. We then establish adequacy results for this new notion. Next, we provide a computational analysis of the problem of checking whether two models are bisimilar. In particular, we show that this problem is \PSPACE-complete. We also investigate two approaches to model minimization in this setting, each exhibiting different computational properties. Along the way, our systematic study of bisimulation yields additional by-product results, w.r.t., for example, the complexity of the definability problem for this logic.

ABSTRACT. In streaming applications, it is often required to detect situations of interest, by means of temporal pattern matching, with minimal latency. In the maritime domain, e.g., where it is crucial to prevent activities that are harmful to the environment, we need to report illegal fishing activities, based on streams of low-level vessel actions, as soon as possible. Streams often include events with delayed effects. In multi-agent voting protocols, e.g., a proposed motion may be seconded at the latest by some time in the future. In simulations of biological systems, a signal may lead to the deactivation of the functions of a gene after a time delay. We propose a formal computational framework that handles streams including events with delayed effects. We present the syntax, semantics and reasoning algorithms of our proposed framework, and demonstrate its correctness and complexity. Furthermore, we present a reproducible analysis on large synthetic and real data streams, from the fields of composite event recognition, multi-agent systems and biological feedback processes, and compare the efficiency of our approach with state-of-the-art systems that can perform stream reasoning in these domains. Our results demonstrate that our framework is capable of reasoning over very large streams, including events with delayed effects, while outperforming the state-of-the-art, often by orders of magnitude.

ABSTRACT. Abduction in knowledge representation is often framed as “ex- plaining away” inconsistencies between a background theory and observations by hypothesizing missing facts or exceptions. Despite decades of KR work on abduction, there are few mod- ern benchmarks that (i) require genuine first-order relational reasoning, (ii) admit unambiguous, solver-checkable verifica- tion, and (iii) produce informative error analyses rather than binary right/wrong judgments. We introduce ABD, a family of default–exception abduction tasks over small finite relational worlds. Each instance provides (a) a set of finite structures with observed facts, and (b) a fixed default-like first-order theory that may be violated by those observations. A model must output a first-order abnormality rule α(x) that defines an exception predicate Ab(x) ↔α(x), restoring satisfiability while keeping exceptions sparse. We formalize three observation regimes with distinct comple- tion semantics. ABD-Full assumes closed-world observation. ABD-Partial allows unknown atoms under existential com- pletion: α is valid if some completion makes the repaired theory satisfiable, with cost optimized in the best case. ABD- Skeptical uses universal completion: αis valid only if the repaired theory is satisfiable under every completion, with cost measured in the worst case. Because domains are finite, validity and costs are computed via SMT (Z3), enabling exact verification and controlled difficulty. We evaluate eight frontier LLMs on 600 instances spanning all three scenarios and seven default theories. The best models achieve over 90% training validity, but parsimony gaps of∼1– 1.6 extra exceptions per world remain. Holdout evaluation reveals distinct generalization profiles: in ABD-Full and ABD- Partial, the dominant failure is parsimony inflation; in ABD- Skeptical, it is validity brittleness—rules that work on training often break on holdouts—while survivors show smaller gap inflation.

ABSTRACT. Abductive expansion is an AGM-style belief-change operation that accommodates new information by adding explanatory hypotheses rather than incorporating the input outright. In contrast to belief sets, belief bases are finite and non-deductively closed, allowing a distinction between explicit and implicit beliefs. We extend abductive belief-change operations to belief bases relative to a hypothesis space, treating the base as firm beliefs and maintaining a separate space of tentative hypotheses that is conditioned on new inputs. We present constructive methods and an axiomatic characterization, and prove representation theorems for the resulting class of operators.

ABSTRACT. Given a knowledge base (KB) with a non-entailed fact, the ABox abduction problem asks for possible extensions of the KB that would entail this fact. This problem has many applications, ranging from diagnosis to explainability and repair. ABox abduction has been well-investigated for consistent KBs and classical semantics, but little is known for the case of inconsistent KBs which can be caused by erroneous data. In this paper we define suitable notions of abduction in this setting and propose criteria that guide abduction towards "useful" hypotheses. To regain meaningful reasoning in the presence of inconsistencies, we use well-established repair semantics. We provide a comprehensive landscape of the complexity of ABox abduction under repair semantics treating different variants of the abduction problem for the light-weight description logics DL-Lite and EL with bottom.

ABSTRACT. This is an extended abstract of the manuscript ’On Validating Propositional Logic System Descriptions for Fault Diagnosis’ (Diedrich, Moddemann, and Niggemann, 2026) that was published in the journal Engineering Applications of Artificial Intelligence in January, 2026.

ABSTRACT. Inspired by revealed preference in economics, we study revealed epistemic trust: an agent’s (dis)trust in an information source is typically hidden, while her accept/reject behavior leaves observable traces. We model such traces by an acceptance function that maps each reported set of formulas to the subset the agent accepts. We develop two complementary models: a white-list mode, where acceptance is supported by trusted information in the report, and a black-list mode, where acceptance avoids distrusted patterns via a cautious remainder-set/full-meet construction. For both modes, we provide postulate-based representation theorems and show how canonical ``revealed'' trust and distrust cores can be reconstructed from the acceptance function itself.

ABSTRACT. We study belief contraction for multi-agent systems in the framework of ‘soft’ (AGM-friendly) Dynamic Epistemic Logic. We look at three different kinds of belief contraction proposed in the Belief Revision literature (severe withdrawal, conservative contraction and moderate contraction), considering them as operations on epistemic plausibility models. We provide sound and complete axiomatizations for logics having dynamic operators for these forms of contraction, in the presence of known static operators such as conditional belief, infallible knowledge and defeasible knowledge.

ABSTRACT. In this paper, we investigate the belief revision problem in epistemic planning, i.e., what will be the beliefs of all agents in a multi-agent system after one agent gains the belief in some fluent formula. We expand the standard logic of belief revision to the dynamic, multi-agent setting in order to be able to assess approaches to epistemic planning. Based on the standard representation in epistemic planning of agents’ beliefs via a single Kripke model, we develop a generalization of the classical AGM belief revision postulates as a formal evaluation instrument for dynamic epistemic reasoning frameworks in which the beliefs of all agents as the result of actions are computed. We provide an example of a simple, generalized ``full-meet'' multi-agent belief revision operator and prove that it satisfies all of the generalized AGM postulates. We moreover define a generalization of the standard postulates for *iterated* revision, present an event model based belief operator, and discuss the potential issues in defining an epistemic operator on Kripke models that can satisfy these properties as well.

ABSTRACT. We consider the problem of modifying a description logic concept in light of models represented as pointed interpretations. We call this setting \emph{model change}, and eviction, which consists of only removing models; incorporation of models in a single operation. introduce a formal notion of revision and argue that it does not reduce to a simple combination of eviction (removing models) and reception (adding models), contrary to intuition. We provide positive and negative results on the compatibility of eviction and reception for $\EL_\bot$ and \ALC description logic concepts and on the compatibility of revision for \ALC concepts.