ABSTRACT. Assumption-Based Argumentation (ABA) is a well-established formalism for modelling and reasoning over debates, with a wide range of applications. However, the high computational complexity of core reasoning tasks in ABA poses a significant challenge for its applicability. This issue is further aggravated when ABA frameworks (ABAFs) are instantiated into graph-based argumentation formalisms, such as Dung's Argumentation Frameworks (AFs) and Argumentation Frameworks with Collective Attacks (SETAFs). In knowledge representation and reasoning, a key strategy to address computational intractability is to optimise reasoning over a given knowledge base through divide-and-conquer algorithms. A paradigmatic example of this approach is splitting, where extensions of a given framework are computed incrementally, by restricting the search space to sub-frameworks only, and then combining the obtained results. This approach has been successfully applied to AFs, for which also a parametrised version has been introduced under stable semantics. However, the exponential growth produced by the instantiation might undermine the usefulness of splitting on the argument graphs induced by ABAFs. To address this issue, our work investigates the concept of splitting on the knowledge base rather than on its graph-based instantiation. Furthermore, we generalise splitting to its parametrised version for ABAFs.

ABSTRACT. Timed Argumentation Frameworks (TAFs) allow taking into account the availability of arguments and attacks in abstract argumentation. We propose a new reasoning approach for TAFs, where a standard Dung-style AF can be associated with each timepoint. We show that, although this framework is more expressive than Dung's framework, our approach does not lead to an increase in computational complexity for most reasoning problems and classical extension-based semantics.

ABSTRACT. This work proposes novel splitting techniques for argumentation formalisms that incorporate supports between defeasible elements. We base our studies on Bipolar Set-Based Argumentation Frameworks (BSAFs), which generalize argumentation frameworks with collective attacks (SETAFs), as well as Bipolar Argumentation Frameworks (BAFs), by incorporating both collective attacks and supports. Notably, BSAFs establish a crucial link to structured argumentation as they naturally capture general (potentially non-flat) assumption-based argumentation. The increase in expressiveness calls for diverse forms of splitting. We consider splits over collective attacks (thereby generalizing the recently proposed splitting techniques for SETAFs), splits over collective supports, as well as splits over both collective attacks and supports. We establish suitable splitting schemata and prove their correctness for the most common argumentation semantics.

ABSTRACT. To better understand, and analyse, natural language arguments, it is desirable to represent them as logical arguments. However, most real-world arguments are enthymemes (i.e. some of the premises and/or claims are implicit), and therefore, there is a need to identify these implicit aspects. A ramification of this is that we may then need to edit some of the explicit premises and/or claim to remove redundant aspects and/or to allow the newly identified implicit formulae to work correctly with the explicit formulae. Furthermore, we may need to edit the claim so that it correctly attacks or supports other arguments as predicted by argument mining or as required by the user. To address these requirements, we propose a logic-based framework, based on classical propositional logic, for representing enthymemes, and manipulating them through a range of logical operations. We introduce meta-level rules to manipulate arguments (e.g. to add or delete premises, to edit claims, to split an argument into two arguments, and to merge two arguments into one). In order to direct the use of meta-level rules, we also introduce gain measures. When choosing a sequence of meta-level rules to apply, we can choose those that increase gain. This meta-level reasoning framework provides some clarity on the nature of enthymemes, and on how agents might elucidate them through a transparent and incremental process.

ABSTRACT. Logical argumentation uses calculi to generate arguments and counter-arguments to capture defeasible reasoning. In this paper, we introduce modular proof-search procedures for a large class of such argument calculi developed to capture two core forms of defeasible reasoning: normative reasoning, formalized via input/output logics, and doxastic reasoning, formalized via normal default logic. Our approach relies on modular, rule-based, and terminating decomposition trees via step-by-step decomposition of norms and defaults. When successful, a terminated decomposition trees certifies derivability of a given argument in its corresponding calculus, including arguments for obligations and beliefs, as well as defeating arguments concluding inapplicability of norms and defaults. We show how rule-based decomposition of norms and defaults is used to determine nonmonotonic inference for credulous reasoning with maximal consistent sets of norms and defaults and stable extensions of arguments in formal argumentation.

ABSTRACT. We study the problem of fitting a description logic (DL) ontology to a given set of positive and negative examples that take the form of an ABox and a Boolean query. While previous work has investigated this problem for the expressive DLs ALC and ALCI, we here focus on the Horn DLs EL and ELI, as well as their extensions with the bottom concept. As the query language, we consider atomic queries (AQs), rooted conjunctive queries (rooted CQs), and unions thereof (rooted UCQs). We provide characterization of the existence of a fitting ontology based on simulations, use them to develop decision procedures, and clarify the exact computational complexity. For AQs, the problem is in PTime for both EL and ELI. For rooted CQs and UCQ, it is Sigma_P^2-complete for EL and ExpTime-complete for ELI. Adding the bottom concept does not change any of these complexities. Interestingly, moving from ALC and ALCI to EL and ELI introduces additional technical challenges rather than simplifying the matter.

ABSTRACT. We present a probably approximately correct algorithm for learning the terminological part of a description-logic knowledge base via subsumption queries. The axioms we learn are concept inclusions between conjunctions of concepts from a specified set of concept descriptions. By varying the distribution of queries posed to the oracle, we adapt the algorithm to improve the recall when using the resulting TBox for ontology-mediated query answering. Experimental evaluation on OWL 2 EL ontologies suggests that our approach helps significantly improve recall while maintaining a high precision of query answering.

ABSTRACT. Expressive power is a recurring theme in Knowledge Representation and Reasoning and has recently become a bridge connecting neural and symbolic representations. Notably, in the domain of graph representation learning, prior work has either established lower bounds on the logical expressive power of graph neural networks (GNNs) or exact correspondences between GNNs and non-standard logics. In this paper, we propose GNN architectures that correspond precisely to prominent fragments of first-order logic (FO), including various modal logics as well as more expressive two-variable fragments. Our results provide a unifying framework for understanding the logical expressiveness of GNNs within FO.

ABSTRACT. Light-weight description logics like EL have been successfully used to represent the terminological knowledge of many application domains. Yet, identifying the characteristics of instances often requires sub-symbolic approaches. We introduce a neuro-symbolic extension of EL which allows for (neural) perception and classification of properties, accompanied by formal (symbolic) reasoning based on these perceptions. Through a prototypical implementation, based on a reduction to logic programming, we show that inferences and learning are effectively achievable.

ABSTRACT. Knowledge base (KB) embeddings aim at combining the capability of classical knowledge graph embeddings to generalize the information present in facts, the ABox, with conceptual knowledge represented in an ontology language, the TBox. Several authors have recently explored the idea of mapping concepts to convex regions in a vector space. This is useful to represent hierarchies, typically present in TBoxes, since more general concepts can be mapped to larger regions, containing those regions associated with more specific concepts. However, the power of convexity is rarely leveraged during the actual learning tasks. Here, we introduce BoxLitE, a KB embedding model for DL-Lite that allows for convex optimization. We show that for any satisfiable DL-Lite KB, there is a BoxLitE embedding that is a weakly faithful model. As a proof of concept, we show how to formulate the KB embedding task as a convex optimization problem and how to obtain embeddings with such desirable faithfulness properties.

ABSTRACT. A fundamental challenge in neurosymbolic systems is applying continuous gradient-based optimization to discrete logical domains. While fuzzy relaxations provide differentiability, they often lack a formal structural alignment with classical logic. In this work, we show that Gödel semantics addresses this limitation through a homomorphism that maps its continuous interpretations to Boolean ones, allowing discrete variables to be encoded while maintaining full differentiability. Building on this foundation, we show that gradient-based optimization on Gödel logic instantiates a discrete local search for Boolean satisfiability. Our formal analysis proves that each optimization step identifies and modifies a single variable within an unsatisfied clause, precisely mimicking the steps of a discrete solver. We identify local optima as the primary limitation of such dynamics and introduce the Gödel Trick, a stochastic reparameterization technique designed to improve the exploration of the solution space. We further show a formal connection between this approach, probabilistic inference, and the Gumbel-Max trick. Experimental results on SAT benchmarks and the Visual Sudoku task validate our theoretical findings, demonstrating that our approach effectively navigates complex combinatorial landscapes and provides a solid foundation for differentiable discrete search.

ABSTRACT. Neurosymbolic integration (NeSy) blends neural‐network learning with symbolic reasoning. The field can be split between methods injecting hand-crafted rules into neural models, and methods inducing symbolic rules from data. We introduce Logic of Hypotheses (LoH), a novel language that unifies these strands, enabling the flexible integration of data-driven rule learning with symbolic priors and expert knowledge. LoH extends propositional logic syntax with a choice operator, which has learnable parameters and selects a subformula from a pool of options. Using fuzzy logic, formulas in LoH can be directly compiled into a differentiable computational graph, so the optimal choices can be learned via backpropagation. This framework subsumes some existing NeSy models, while adding the possibility of arbitrary degrees of knowledge specification. Moreover, the use of Gödel fuzzy logic and the recently developed Gödel trick yields models that can be discretized to hard Boolean-valued functions without any loss in performance. We provide experimental analysis on such models, showing strong results on tabular data and on two NeSy tasks with a perceptual component.

ABSTRACT. Neurosymbolic systems can satisfy logical constraints during learning without achieving the intended concept-label correspondence; this is a problem known as reasoning shortcuts. We formalize reasoning shortcuts as a constraint satisfaction problem and investigate under which conditions concept mappings are uniquely determined by the constraints. We prove that a discrimination property (requiring that no valid concept mapping can be transformed into another valid mapping by swapping two concept values) is necessary for shortcut-freeness under bijective mappings, but demonstrate via a counterexample that it is insufficient even when the constraint graph is connected. We develop an ASP-based algorithm that verifies whether a given constraint set uniquely determines the intended concept mapping, with proven soundness and completeness. When shortcuts are detected, a greedy repair algorithm eliminates them by augmenting the constraint set, converging in at most $k$ iterations, where $k$ is the number of alternative valid mappings. We further provide a complexity classification: deciding shortcut-freeness is coNP-complete, counting shortcuts is \#P-complete, and finding minimal repairs is NP-hard. We also establish sample complexity bounds showing that a logarithmic number of label queries suffices for disambiguation in favorable cases, while querying all ambiguous positions suffices in the worst case. Experiments across eight benchmark domains validate our approach.

ABSTRACT. The use of deep learning to solve fundamental AI problems such as Boolean Satisfiability (SAT) has been explored recently to develop robust and scalable reasoning systems. This work advances such neural-based reasoning approaches by developing a new Graph Neural Network (GNN) to differentiably solve (weighted) Maximum Satisfiability (MaxSAT). To this end, we propose SAT-based Graph Attention Networks (SGATs) as novel GNNs that are built on t-norm based attention and message passing mechanisms, and structurally designed to approximate greedy distributed local search. To demonstrate the effectiveness of our model, we develop a local search solver that uses SGATs to continuously solve any given MaxSAT problem. Experiments on (weighted) MaxSAT benchmark datasets demonstrate that SGATs significantly outperform existing neural-based architectures, and achieve state-of-the-art performance among continuous approaches, highlighting the strength of the proposed model.

ABSTRACT. In real-world scenarios, reinforcement learning (RL) agents must not only maximize reward but also behave safely, including during training. This has led to growing interest in Safe RL, where the objective is to learn an optimal policy among those satisfying given safety constraints. Most existing approaches focus on constraints expressed either as expected costs or as avoidance properties. However, safety in dynamical systems is often expressed using rich temporal languages, such as Probabilistic Computation Tree Logic (PCTL). In this paper, we address the Safe RL problem under constraints expressed in CPCTL, a fragment of PCTL that generalizes avoidance constraints and enables the specification of complex, nested behaviours. To this end, we leverage Shielding, a technique that restricts the agent’s actions during both training and deployment to enforce safety over an infinite horizon. We first introduce a general framework based on an augmentation method and provide its theoretical foundations. Building on this framework, we propose an algorithm that is provably safe at all times, including during training, while remaining optimal among all safe policies. Finally, we present an experimental evaluation demonstrating the effectiveness of our approach.

ABSTRACT. We explore the use of answer set programming (ASP) and its extension with quantifiers, ASP(Q), for inconsistency-tolerant querying of prioritized data, where a priority relation between conflicting facts is exploited to define three notions of optimal repairs (Pareto-, globally- and completion-optimal). We consider the variants of three well-known semantics (AR, brave and IAR) that use these optimal repairs, and for which query answering is in the first or second level of the polynomial hierarchy for a large class of logical theories. Notably, this paper presents the first implementation of globally-optimal repair-based semantics, as well as the first implementation of the grounded semantics, which is a tractable under-approximation of all these optimal repair-based semantics. Our experimental evaluation sheds light on the feasibility of computing answers under globally-optimal repair semantics and the impact of adopting different semantics, optimizations, and encodings.

ABSTRACT. Answer Set Programming (ASP) is a mature and widely used framework for modeling and solving problems in AI, knowledge representation and reasoning, and combinatorial search. Counting answer sets is of growing importance for analyzing search spaces, navigating ASP programs, and enabling probabilistic reasoning. While Truszczynski established a complete hierarchy for the computational complexity of ASP decision and reasoning problems (skeptical and credulous), a corresponding systematic treatment of counting problems has been missing so far. We close this gap by providing an almost complete characterisation of the counting complexity landscape for ASP. A remaining gap arises between Krom and Horn programs, caused by the minimality of disjunctions in Krom rule heads for guessing. To address this issue, we replace disjunctions with choice rules and introduce a controlled fragment in which choices are allowed and every rule is simultaneously Horn and Krom (Choice-Horn-Krom). We show that this fragment does not admit an polynomial-time approximation scheme (FPRAS) under standard complexity-theoretic assumptions. However, we prove that counting answer sets of an arbitrary ASP program can already be done by counting answer sets of two Choice-Horn-Krom programs. This result demonstrates the expressive power of ASP and yields a conceptually simpler alternative to Valiant's classical reduction from #SAT to #Krom-SAT, which a very well-known result in propositional logic.

ABSTRACT. The ASP(Q) language extends Answer Set Programming (ASP) with Quantifiers that operate over answer sets. Thus, ASP(Q) facilitates a more natural encoding of problems whose complexity exceeds $NP$ within the ASP framework. In this paper we focus on ASP(Q) programs with two quantifiers, i.e., 2-ASP(Q) programs, which can be used to model problems in the second level of the Polynomial Hierarchy. In particular, we propose an approach for evaluating 2-ASP(Q) programs that is inspired by Counterexample Guided Abstraction Refinement (CEGAR). Unlike existing state-of-the-art ASP(Q) solvers, which are typically based on QBF solvers, our new approach leverages ASP solvers, and suffers no overhead due to the effects of translating ASP(Q) in QBF. Experimental results demonstrate that our technique consistently outperforms state-of-the-art ASP(Q) solvers, across benchmark problems located at the second level of the polynomial hierarchy.

ABSTRACT. In this paper, we develop a novel logic-based approach to detecting high-level temporally extended events from timestamped data and background knowledge. Our framework employs logical rules to capture existence and termination conditions for simple temporal events and to combine these into meta-events. In the medical domain, for example, disease episodes and therapies are inferred from timestamped clinical observations, such as diagnoses and drug administrations stored in patient records, and can be further combined into higher-level disease events. As some incorrect events might be inferred, we use constraints to identify incompatible combinations of events and propose a repair mechanism to select preferred consistent sets of events. While reasoning in the full framework is intractable, we identify relevant restrictions that ensure polynomial-time data complexity. Our prototype system implements core components of the approach using answer set programming. An evaluation on a lung cancer use case supports the interest of the approach, both in terms of computational feasibility and positive alignment of our results with medical expert opinions. While strongly motivated by the needs of the healthcare domain, our framework is purposely generic, enabling its reuse in other application areas.

ABSTRACT. Answer Set Programming (ASP) is a declarative formalism widely used in knowledge representation and reasoning for modeling and solving combinatorial problems, yet current Large Language Models (LLMs) often struggle to generate correct programs from natural language specifications. This difficulty stems both from the limited presence of ASP in training corpora and from the strict syntactic and semantic constraints imposed by stable model semantics. We introduce ALM–ASP (Agentic Loop for Modeling in ASP), a multi-agent architecture for automatic ASP modeling grounded in a functional model of language agents equipped with tools and persistent state. ALM–ASP instantiates this model via two interacting agents: a Modeler, which incrementally constructs candidate ASP programs, and a Validator, which assesses their alignment with the original specification and provides feedback for refinement. The agents interact through a shared ASP execution environment backed by the CLINGO engine, yielding an iterative construct–validate loop. An empirical evaluation on a challenging subset of CP–Bench and on problems from recent LP/CP Programming Contests shows that ALM–ASP significantly improves both syntactic validity and end-to-end correctness over general-purpose LLM baselines, and also achieves improved instance coverage compared to the closest agentic alternative, CP–Agent.

ABSTRACT. Model counting (#SAT) is a fundamental yet #P-complete problem central to probabilistic reasoning. In this work, we address incremental model counting, where sequences of structurally similar formulas must be counted. We propose an approach that amortizes computation via a persistent caching mechanism, retaining component data across solver calls to avoid redundant search. Additionally, we investigate branching heuristics adapted for this setting. We focus on the problems of argumentation and soft core, for which incremental model counting is natural. Experiments demonstrate that our method improves performance compared to current model counters, highlighting the capability of structure-aware reuse in dynamic environments.

ABSTRACT. Boolean hedonic games are a class of cooperative games involving multiple agents in which agents aim to form coalitions based on individual agents' preferences. In this work, we provide complexity results and exact algorithms for the task of forming Nash stable coalitions under different membership rights in the dichotomous setting where agents specify preferences for which coalitions they are happy/unhappy to join. The membership rights specify veto rights for coalitions, allowing a coalition to forbid an individual agent from moving (exiting the current coalition or entering another coalition) even if the agent themself would become more happy to move. We establish that various problem variants and their refinements in this setting are often situated on the second level of the polynomial hierarchy, complete for $\Sigma_2^p$. Building on the complexity results, we develop Boolean satisfiability (SAT) based counterexample-guided abstraction refinement algorithms for the $\Sigma_2^p$ problem variants and empirically evaluate a first-of-kind implementation of the approaches.

ABSTRACT. We present BAss (BDD-based ADF symbolic solver), a novel analysis tool for Abstract Dialectical Frameworks (ADFs) based on Binary Decision Diagrams (BDDs). It supports the fully-symbolic computation of all admissible, complete, and preferred interpretations, as well as two-valued and stable models of an ADF. Our approach is inspired by the recently discovered equivalence between Boolean Networks (BNs) and ADFs by Heyninck et al. (2024) and Azpeitia et al. (2024), significantly extending current BDD-based tools bioLQM, aeon, and adf-bdd. We conducted experiments on a large-scale collection of real-world models from both the BN and ADF communities. Our results show that BAss dramatically outperforms previous BDD-based tools and is competitive (even significantly better in some cases) with state-of-the-art SAT/ASP-based methods, particularly in scenarios involving large solution spaces. Notably, BAss is able to enumerate all fixed points or minimal trap spaces of certain biological networks beyond the reach of existing tools, thereby enabling new analysis and case studies in systems biology. These results highlight the practical relevance of symbolic reasoning for complex real-world applications, particularly in systems biology and formal argumentation.

ABSTRACT. Determining the validity of a quantified Boolean formula (QBF) is a PSPACE-complete problem with rich expressive power. Despite interest in efficient solvers, there is, compared to problems in NP, a lack of positive theoretical results, and in the parameterized complexity setting one often has to restrict the quantifier prefix (e.g., bounding alternations) to obtain fixed parameter tractability (FPT). We propose a new parameter: the number of variables in clauses that has to be removed before reaching a tractable class (a clause covering (CC) backdoor). We are then interested in solving QBF in FPT time given a CC-backdoor of size k. We consider the three classical, tractable cases of QBF as base classes: Horn, 2-CNF, and linear equations. We establish W[1]-hardness for Horn but prove FPT for the others, and prove that in a precise, algebraic sense, we are only missing one important case for a full dichotomy. Our algorithms are non-trivial and depend on propagation, and Gaussian elimination, respectively, and are comparably unexplored for QBF.

ABSTRACT. Hierarchical data is common in many domains like life sciences and e-commerce, and its embeddings often play a critical role. While hyperbolic embeddings offer a theoretically grounded approach to representing hierarchies in low-dimensional spaces, current methods often rely on specific geometric constructs as embedding candidates. This reliance limits their generalizability and makes it difficult to integrate with techniques that model semantic relationships beyond pure hierarchies, such as ontology embeddings. In this paper, we present RegD, a flexible Euclidean framework that supports the use of arbitrary geometric regions---such as boxes and balls---as embedding representations. Although RegD operates entirely in Euclidean space, we formally prove that it achieves hyperbolic-like expressiveness by incorporating a depth-based dissimilarity between regions, enabling it to emulate key properties of hyperbolic geometry, including exponential growth. We establish the faithfulness of our approach. Furthermore, extensive empirical evaluations on diverse real-world datasets demonstrate consistent performance improvements over state-of-the-art methods, highlighting RegD’s potential for broader applications, including ontology embedding tasks that extend beyond hierarchical structures.

ABSTRACT. We present a new approach for distilling boosted trees into decision trees, in the objective of generating an ML model offering an acceptable compromise in terms of predictive performance and interpretability. We explain how the correction approach called rectification can be used to implement such a distillation process. We show empirically that this approach provides interesting results, in comparison with an approach to distillation achieved by retraining the model.

ABSTRACT. Knowledge Representation (KR) formalisms provide precise specifications of algorithmic structure, yet it remains unclear whether gradient-trained neural networks implement these specifications even when they are theoretically expressible. Recent formal language theory tells us what Transformers \emph{can} express---masked hard-attention Transformers recognize the star-free regular languages, equivalent to first-order logic with linear order (FO[<]) and linear temporal logic (LTL)---but not what gradient-trained Transformers \emph{will} learn. We ask whether trained networks actually implement the logical circuits that theory predicts, and propose KR-Guided Mechanistic Verification to find out. The idea is to compile a B-RASP specification into a Structural Causal Model whose variables correspond to prescribed logical operations, then use Distributed Alignment Search to obtain quantitative, falsifiable causal evidence for or against each operation's presence in the trained network. We instantiate this framework on binary increment, a task for which B-RASP prescribes an explicit three-stage circuit implementable by a two-layer Transformer with O(poly(n)) parameters---exponentially fewer states than any fixed-precision recurrent or state space baselines require. The answer is affirmative: all three prescribed operations are faithfully encoded in dedicated neural subspaces, with wrong-specification controls at chance; Sparse Autoencoder decomposition independently recovers the same logical structure without supervision. Moreover, this structure is not acquired gradually: it emerges as a sharp phase transition during grokking, providing a specification-aligned progress measure that reveals \emph{what} changes during the generalization transition, not merely \emph{that} something changes. These results demonstrate that KR formalisms can serve not only as prescriptive specifications of what networks should compute, but as falsifiable causal hypotheses that mechanistic interpretability tools can rigorously test---bridging the gap between symbolic KR and neural computation.

ABSTRACT. We introduce a logical language for reasoning about quantized aggregate-combine graph neural networks with global readout (ACR-GNNs). We provide a logical characterization and use it to prove that verification tasks for quantized GNNs with readout are (co)NEXPTIME-complete. This result implies that the verification of quantized GNNs is computationally intractable, prompting substantial research efforts toward ensuring the safety of GNN-based systems. We also experimentally demonstrate that quantized ACR-GNN models are lightweight while maintaining good accuracy and generalization capabilities with respect to non-quantized models.

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 fully automated 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 various planning domains shows that our framework can converge to correct theories.