ABSTRACT. This extended abstract summarizes previous results on the repair of inconsistent constraint networks from a viewpoint of explaining the inconsistency. We discuss how explanation could be defined using methods of formal argumentation and illustrate use cases of constraint-based approaches to planning.

ABSTRACT. In the literature, interactive ontology repair approaches assume that users can always decide whether an axiom should be included in a repair, i.e., either kept or removed. In this paper, we present an interactive approach for repairing ontologies in which users are assisted by various decision-support features that provide additional information in cases of uncertainty. This work has been submitted to the Description Logic Workshop 2026 and is currently under review.

ABSTRACT. The extraction of Minimal Unsatisfiable Subsets (MUSes) has been extensively studied in SAT for clauses as well as groups of clauses, but it is also useful in other formalisms such as pseudo-Boolean solving (PB) and constraint programming (CP), especially for explaining unsatisfiability. In this paper we focus on highly efficient deletion-based MUS extraction, where the main bottleneck is the number of solver calls needed to find a MUS. This number can be greatly reduced by techniques such as model rotation (MR), which manipulates a satisfying assignment to find new critical constraints. However, MR has mostly been studied only for (grouped) clausal constraints. We propose generalisations of MR for pseudo-Boolean and CP constraints, and empirically evaluate them on PB and CP instances, including SAT encodings with state-of-the-art SAT-based MUS extractors. Our results show that MR is most effective when applied directly at the level of the original formalism, increasing the number of solved instances for PB and reducing solving times for CP.

ABSTRACT. Automated Essay Scoring (AES) has achieved strong predictive performance with neural and large language models, but often remains opaque. We propose an interpretable AES framework based on Quantitative Bipolar Argumentation Frameworks (QBAFs), representing each essay as an argumentative graph of discourse units linked by support and attack relations. We further augment the graph with feature-derived arguments capturing interpretable essay-level and discourse-unit-level statistics. Experiments show that our approach achieves competitive performance against standard baselines while providing structured explanations, suggesting that QBAFs are a promising formalism for transparent AES.

ABSTRACT. This abstract extends our IJCNLP \& AACL paper published in 2025 with a new study that closes a gap in prior work. It has also been submitted to the 39th International Workshop on Description Logics (DL 2026). Large language models (LLMs) are increasingly applied in domains that demand reliable and interpretable reasoning. While formal reasoning methods can generate correct proofs, these proofs are often inaccessible to non-expert users. This raises a natural question: Can LLMs, when given a proof, faithfully interpret its reasoning and communicate it clearly? Recently, we have introduced \texttt{ProofTeller}, a benchmark that evaluates this ability across three tasks: (1) identifying key proof steps, (2) summarizing the reasoning, and (3) explaining the result in concise natural language. The benchmark covers three domains: \emph{Biology}, \emph{Drones}, and \emph{Recipes}, representing scientific, safety-critical, and everyday reasoning scenarios. We find a consistent near-conclusion bias: LLMs tend to focus on steps closest to the final proof conclusion rather than on the most informative ones. A targeted human study confirms that explanations based on such steps are rated less appropriate for end users. These findings indicate that even when reasoning is provided, current LLMs face challenges in communicating key information in a useful manner, highlighting the need for LLMs that can communicate important details reliably.

ABSTRACT. This is an extended abstract of a paper that has been submitted to the 39th International Workshop on Description Logics (DL 2026). Many techniques have been developed to explain logical reasoning, such as proofs or abduction. However, such methods are useful mainly for experts in logic, e.g., for debugging ontologies. For actually explaining logical consequences and missing consequences to end users of logic-based systems, e.g., in the Semantic Web, it is necessary to study how to adapt and present such explanations in an understandable way. We report on a series of user studies comparing abduction and counterexamples for explaining missing consequences in Description Logic (DL) ontologies, and evaluating the impact of prior knowledge on the level of detail an explanation needs to provide. While we did not find objectively quantifiable results, we analyse and discuss the results of detailed qualitative user interviews, and extract recommendations for executing user studies on logical reasoning systems.

ABSTRACT. Gradual argumentation is a sub-field of Computational Argumentation from symbolic AI which is attracting attention for its ability to support transparent and contestable AI systems. It is considered a useful tool in domains such as decision-making, recommendation, debate analysis, amongst others. The outcomes in such domains are usually dependent on the arguments' base scores i.e. their intrinsic strengths, which must be selected carefully. Often, this selection process requires user expertise and may not always be straightforward. However, organising the arguments by preference could simplify the task. In this work, we introduce \emph{Base Score Extraction Functions}, which provide a mapping from users' preferences over arguments to base scores. These functions can be applied to the arguments of a \emph{Bipolar Argumentation Framework} (BAF), supplemented with preferences, to obtain a \emph{Quantitative Bipolar Argumentation Framework} (QBAF), allowing the use of well-established computational tools in gradual argumentation. We outline the desirable properties of Base Score Extraction Functions, discuss some design choices, and provide an algorithm for base score extraction. Our method incorporates an approximation of non-linearities in human preferences to allow for better approximation of the real ones. Finally, we evaluate our approach both theoretically and experimentally in a robotics setting, and offer recommendations for selecting appropriate gradual semantics in practice.

ABSTRACT. Acquiring correct action theories from informal specifications remains a central challenge in KR. Large Language Models can generate plausible domain models from natural language, but the resulting theories frequently contain missing preconditions, incorrect effects, or superfluous actions. Existing refinement approaches either require human experts to correct these errors or assume that the input specification is itself correct. We present a framework that iteratively refines LLM-generated action theories using formal explanations grounded in SAT-based verification. Each candidate theory is encoded as a bounded SAT problem and tested against solvable tasks, which must admit a valid plan, and unsolvable tasks, which must be correctly rejected. When a test fails, we extract a formal explanation that pinpoints the specific theory constraints responsible for the failure, and feed this explanation back to the LLM to guide its next revision. Our initial evaluation across six planning domains shows that our framework can converge to correct theories.

ABSTRACT. Large language models (LLMs) exhibit strong general capabilities, but their deployment in high-stakes domains is hindered by their opacity and unpredictability. Recent work has taken meaningful steps towards addressing these issues by augmenting LLMs with post-hoc reasoning based on computational argumentation, providing faithful explanations and enabling users to contest incorrect decisions. However, this paradigm is limited to pre-defined binary choices and only supports local contestation for specific instances, leaving the underlying decision logic unchanged and prone to repeated mistakes. In this paper, we introduce ArgEval, a framework that shifts from instance-specific reasoning to structured evaluation of general decision options. Rather than mining arguments solely for individual cases, ArgEval systematically maps task-specific decision spaces, builds corresponding option ontologies, and constructs general argumentation frameworks (AFs) for each option. These frameworks can then be instantiated to provide explainable recommendations for specific cases while still supporting global contestability through modification of the shared AFs. We investigate the effectiveness of ArgEval on treatment recommendation for glioblastoma, an aggressive brain tumour, and show that it can produce explainable guidance aligned with clinical practice.

ABSTRACT. Understanding the internal `thinking' process of Large Language Models (LLMs) and the cause of hallucinations remains a key challenge. To this end, we introduce latent debate, a structured surrogate framework for interpreting model outputs on True/False prediction tasks through the lens of internal latent arguments and interactions amongst them. Unlike human debates, latent debate captures the hidden supporting and attacking signals that arise within a model during a single inference. We first present a model- and task-agnostic conceptual framework, and then instantiate it symbolically to approximate the thinking process of LLMs towards binary decisions. Empirical studies demonstrate that our latent debate is a faithful structured surrogate model that has highly consistent predictions with the original LLM, while providing a form of interpretability. We also demonstrate that our latent debate provides a strong baseline for hallucination detection. Specifically, we identify strong correlations between debate patterns and hallucinations, such as a high degree of disagreement in the middle layers of the latent debate surrogate is linked to a higher risk of hallucinations. Our findings suggest that latent debate shows potential to analyze internal signals in LLMs for binary decision settings.

ABSTRACT. Scheduling is a highly relevant aspect of industrial work. From assigning jobs to machines to creating shift plans for employees; schedules must be created to ensure efficiency, cover requirements and adhere to working regulations. As creating schedules while keeping track of all constraints is often a notoriously difficult job, automated methods can be employed. However, sometimes no solution can be found due to conflicting problem specifications. In this case, it is important to explain which constraints contribute to infeasibility and how the problem can be relaxed. We study the Rotating Workforce Scheduling Problem, for which we develop a framework that generates explanations for instances with incompatible constraints. We show how Minimal Correction Sets can be used to provide detailed explanations for infeasible problems, caused by hard constraint violations or by conflicting optimisation goals. We perform a case study and experiments on (real-life) instances that reveal that explanations can be efficiently generated.

ABSTRACT. Formal explainability methods provide logic-based explanations with precise semantic guarantees, yet they often require full access to a model's symbolic encoding. Sample-based approaches relax this requirement by deriving explanations from finite observations of model behavior, but existing methods largely produce static explanations that ignore user context and domain constraints. This paper proposes a framework that integrates sample-based formal explainability with restricted constraint reasoning, where constraints encode user preferences as inclusion and exclusion of features. We show that, under these restrictions, the validation of the existence of both abductive and contrastive explanations can be decided in polynomial time. We further embed this mechanism into a dialogical framework that allows users to interactively refine constraints and obtain adapted explanations without sacrificing formal guarantees. A running example illustrates how the dialogue evolves as constraints are revised.

ABSTRACT. We investigate how the recently proposed framework of answer set programming with quantifiers (ASP(Q)) can be applied to the task of computing step-wise explanation sequences for the classic puzzle game Sudoku.

ABSTRACT. Explainable Reinforcement Learning (XRL) seeks to make Reinforcement Learning (RL) policies more transparent and interpretable, a key requirement in safety-critical and human-centric scenarios. However, it is mostly based on user studies, thus targeting the needs of a specific audience and lacking shared evaluation metrics. On the other hand, logic-based approaches within eXplainable Artificial Intelligence (XAI) provide compact, human-readable abstractions of decision-making. However, the systematic quantification of the explainability degree of logical representations remains an open problem. This work aims to advance the state of the art in XRL by introducing objective and planning-oriented metrics for policy explainability in single-and multi-agent RL settings. At the same time, it contributes to the field of logics for XAI by providing a principled way to quantify the explainability of logical rules, moving beyond common-sense assessments and simple propositional fragments. We employ Inductive Logic Programming (ILP) to extract symbolic representations of RL policies and define a novel set of explainability metrics, including \textit{activation rate}, \textit{feature coverage}, \textit{syntactic distance} and \textit{semantic distance}. These metrics quantify alignment between symbolic rules and agent behavior, the role of features in decision-making, and the evolution of policies during training and across agents in single and Multi-Agent RL (MARL). Experiments across different RL domains show that the proposed metrics highlight action-specific learning dynamics beyond global return, provide fine-grained insights into domain features beyond classical approaches for global feature importance estimation, and uncover coordination, specialization, and adaptation patterns in MARL. Moreover, they provide crucial insights for the transfer and generalization of action-specific policies. Our framework advances XRL by offering rigorous, objective, and interpretable metrics to evaluate symbolic policy representations. This contributes to understanding, debugging, and refining RL agents, paving the way for more robust and trustworthy applications in dynamic, safety-critical, and multi-agent environments.

ABSTRACT. Neural networks (NNs) are the core of AI-based technologies. However, the degree of reliability in performing the task is an open problem. The explainability of a central task of NNs, classification, is of immense importance. While at the rise of AI-based reasoning, explainability of the NN classification has mostly been done using statistical methods, nowadays, a more reliable trend of formal logic-based methods is gaining popularity. The advantage of the formal approach is that it gives strict and provable guarantees of the classification. Formal methods is a mature field that has delivered a number of efficient computational solutions already applied in the analysis of software and hardware systems. Formal explainability methods naturally have the ability to reuse existing techniques and tools for a newly emerging field of formal explainability of NN classification. This paper surveys existing efforts to compute explanations of neural network classification based on logical abductive reasoning. The abduc- tion approach is crucial for generalizing the results, capturing the underlying behavior of the classifier. We present the existing techniques as instances of a general formalization that allows contrasting them against each other. In addition, we discuss the issue of the quality of explanations, focusing on their key metrics and factors. As an illustrative example, the paper also presents a practical framework, SpEXplAIn, which automatically computes Space Explanations, the most general abduction-based explanations for classifying NNs with provable guarantees of the behavior of the network in continuous areas of the input feature space. The tool leverages an SMT solver compatible with a range of flexible Craig interpolation algorithms and unsatisfiable core generation, and is applicable to a wide range of applications.

ABSTRACT. In knowledge distillation, a student model learns from the outputs produced by a teacher model. Recent studies have shown that, beyond explicit task knowledge, student models may also acquire hidden behavioural traits from teacher models, a phenomenon known as subliminal learning. Yet, its underlying mechanism remains unclear. In this paper, we use argumentative explanations to investigate this phenomenon. Specifically, we represent Multi-layer Perceptron (MLP)-based teacher and student models as quantitative bipolar argumentation frameworks (QBAFs), and apply argument attribution explanations (AAEs) to measure the contribution of each argument to the final output argument. Our experimental results show that student models exhibiting subliminal learning are more closely aligned with their teacher models in AAE patterns than non-subliminal student models.