GenAI4ELab/papercli-papers huggingface dataset:
Decidable Multi-agent Epistemic Planning: A Situation Calculus Approach
Authors: Qihui Feng; Gerhard Lakemeyer
Venue: AAAI 2026 (main)

Abstract: Multi-agent epistemic planning (MEP) is the task of generating action sequences that achieve goals specified over both the physical world and agents’ mental states. It plays an important role in research domains such as game theory, computational economics, and cognitive science. While dynamic epistemic logic (DEL) provides an expressive framework for MEP, it requires complete, model-based specifications of the initial state and action effects, and suffers from undecidability due to the unbounded nesting of beliefs.
In this work, we propose a modal variant of the situation calculus that captures much of the expressive power of the DEL approach. Inspired by the cognitive concept Theory of Mind (ToM), we introduce action theories with hierarchical structures, allowing agents to reason about other agents' action theories up to bounded depths. We develop a regression method that reduces reasoning about future states to reasoning about the initial state. By preserving bounded-order ToM throughout the regression process, our approach ensures the decidability of the planning problem. Finally, we propose an algorithm to find the optimal solution, namely, to find the shortest action sequence that achieves the goal.
Computing Syntax Tree-based Minimal Unsatisfiable Cores of LTLf Formulas
Authors: Valeria Fionda; Antonio Ielo; Francesco Ricca
Venue: AAAI 2026 (main)

Abstract: Linear Temporal Logic on Finite Traces (LTLf) is a popular logic to express declarative specifications in Artificial Intelligence (AI). 
The recent call for explainable AI tools has made relevant the problem of computing efficiently minimal unsatisfiable cores (MUCs) and minimal correction sets (MCSes) of LTLf formulas.
Recent work has focused on the extraction of MUCs on formulas in conjunctive form.
In this paper, we present a method that operates on arbitrary formulas and computes a more refined notion of MUCs, as introduced by Schuppan, along with the corresponding notion of MCSes. Experiments show that our system, based on Answer Set Programming, outperforms available tools.
Two Heads Are Better than One: Distilling Large Language Model Features into Small Models with Feature Decomposition and Mixture
Authors: Tianhao Fu; Xinxin Xu; Weichen Xu; Jue Chen; Ruilong Ren; Bowen Deng; Xinyu Zhao; Jian Cao; Xixin Cao
Venue: AAAI 2026 (main)

Abstract: Market making (MM) through Reinforcement Learning (RL) has attracted significant attention in financial trading. With the development of Large Language Models (LLMs), more and more attempts are being made to apply LLMs to financial areas. A simple, direct application of LLM as an agent shows significant performance. Such methods are hindered by their slow inference speed, while most of the current research has not studied LLM distillation for this specific task. To address this, we first propose the normalized fluorescent probe to study the mechanism of the LLM’s feature. Based on the observation found by our investigation, we propose Cooperative Market Making (CMM), a novel framework that decouples LLM features across three orthogonal dimensions: layer, task, and data. Various student models collaboratively learn simple LLM features along with different dimensions, with each model responsible for a distinct feature to achieve knowledge distillation. Furthermore, CMM introduces an Hájek-MoE to integrate the output of the student models by investigating the contribution of different models in a kernel function-generated common feature space. Extensive experimental results on four real-world market datasets demonstrate the superiority of CMM over the current distillation method and RL-based market-making strategies.
Active Learning of Symbolic Automata over Rational Numbers
Authors: Sebastian Hagedorn Gaete; Martín Muñoz; Cristian Riveros; Rodrigo Toro Icarte
Venue: AAAI 2026 (main)

Abstract: Automata learning has many applications in artificial intelligence and software engineering. Central to these applications is the L* algorithm, introduced by Angluin (1987). The L* algorithm learns deterministic finite-state automata (DFAs) in polynomial time when provided with a minimally adequate teacher. Unfortunately, the L* algorithm can only learn DFAs over finite alphabets, which limits its applicability. In this paper, we extend L* to learn symbolic automata whose transitions use predicates over rational numbers, i.e., over infinite and dense alphabets. Our result makes the L* algorithm applicable to new settings like (real) RGX, and time series. Furthermore, our proposed algorithm for learning each predicate is optimal in the sense that it asks a number of queries to the teacher that is at most linear with respect to the size of their representation.
Formal Verification of Diffusion Auctions
Authors: Rustam Galimullin; Munyque Mittelmann; Laurent Perrussel
Venue: AAAI 2026 (main)

Abstract: In diffusion auctions, sellers can leverage an underlying social network to broaden participation, thereby increasing their potential revenue. Specifically, sellers can incentivise participants in their auction to diffuse information about the auction through the network. While numerous variants of such auctions have been recently studied in the literature, the formal verification and strategic reasoning perspectives have not been investigated yet.   

Our contribution is threefold. First, we introduce a logical formalism that captures the dynamics of diffusion and its strategic dimension. Second, for such a logic, we provide model-checking procedures that allow one to verify properties like the Nash equilibrium, and that pave the way towards checking the existence of sellers' strategies. Third, we establish computational complexity results for the presented algorithms.
Matrix Editing Meets Fair Clustering: Parameterized Algorithms and Complexity
Authors: Robert Ganian; Hung P. Hoang; Simon Wietheger
Venue: AAAI 2026 (main)

Abstract: We study the computational problem of computing a fair means clustering of discrete vectors, which admits an equivalent formulation as editing a colored matrix into one with few distinct color-balanced rows by changing at most k values. While NP-hard in both the fairness-oblivious and the fair settings, the problem is well-known to admit a fixed-parameter algorithm in the former "vanilla" setting. As our first contribution, we exclude an analogous algorithm even for highly restricted fair means clustering instances. We then proceed to obtain a full complexity landscape of the problem, and establish tractability results which capture three means of circumventing our obtained lower bound: placing additional constraints on the problem instances, fixed-parameter approximation, or using an alternative parameterization targeting tree-like matrices.
Heterogeneous Graph Neural Networks for Assumption-Based Argumentation
Authors: Preesha Gehlot; Anna Rapberger; Fabrizio Russo; Francesca Toni
Venue: AAAI 2026 (main)

Abstract: Assumption‐Based Argumentation (ABA) is a powerful structured argumentation formalism, but exact computation of extensions under stable semantics is intractable for large frameworks.  We present the first Graph Neural Network (GNN) approach to approximate credulous acceptance in ABA. To leverage GNNs, we model ABA frameworks via a dependency graph representation encoding assumptions, claims and rules as nodes, with heterogeneous edge labels distinguishing support, derive and attack relations. We propose two GNN architectures—ABAGCN and ABAGAT—that stack residual heterogeneous convolution or attention layers, respectively, to learn node embeddings. Our models are trained on the ICCMA 2023 benchmark, augmented with synthetic ABAFs, with hyperparameters optimised via Bayesian search.  Empirically, both ABAGCN and ABAGAT outperform a state‐of‐the‐art GNN baseline that we adapt from the abstract argumentation iterature, achieving a node‐level F1 score of up to 0.71 on the ICCMA instances. Finally, we develop a sound polynomial time extension‐reconstruction algorithm driven by our predictor: it reconstructs stable extensions with F1 above 0.85 on small ABAFs and maintains an F1 of about 0.58 on large frameworks. Our work opens new avenues for scalable approximate reasoning in structured argumentation.
Non-Monotonic S4F Standpoint Logic
Authors: Piotr Gorczyca; Hannes Strass
Venue: AAAI 2026 (main)

Abstract: Standpoint logics offer unified modal logic-based formalisms for representing multiple heterogeneous viewpoints. At the same time, many non-monotonic reasoning frameworks can be naturally captured using modal logics — in particular using the modal logic S4F. In this work, we propose a novel formalism called S4F Standpoint Logic, which generalises both S4F and standpoint propositional logic and is therefore capable of expressing multi-viewpoint, non-monotonic semantic commitments. We define its syntax and semantics and analyze its computational complexity, obtaining the result that S4F Standpoint Logic is not computationally harder than its constituent logics, whether in monotonic or non-monotonic form. We also outline mechanisms for credulous and sceptical acceptance and illustrate the framework with an example.
The Correspondence Between Bounded Graph Neural Networks and Fragments of First-Order Logic
Authors: Bernardo Cuenca Grau; Eva Feng; Przemysław Andrzej Wałęga
Venue: AAAI 2026 (main)

Abstract: Graph Neural Networks (GNNs) address two key challenges in applying deep learning to graph-structured data: they handle varying size input graphs and ensure invariance under graph isomorphism. While GNNs have demonstrated broad applicability, understanding their expressive power remains an important question. 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. To establish these results, we apply methods from finite model theory of first-order and modal logics to the domain of graph representation learning. Our results provide a unifying framework for understanding the logical expressiveness of GNNs within FO.
Extending Description Logics with Generic Concepts – the Case of Terminologies
Authors: Joshua Hirschbrunn; Yevgeny Kazakov
Venue: AAAI 2026 (main)

Abstract: We propose an extension of Description Logics (DLs) with generic concepts
and conditional axioms. Inspired by object-oriented languages, generic
concepts allow a compact definition of concepts with similar structures.
For example, one can define a generic concept Owner[X] to describe objects
that own another object from X, and later use a specific replacement of the
parameter X, such as Owner[Pet] representing pet owners. Conditional axioms
can be used to set bounds on the values that replace the generic parameters.
For example, we could restrict replacements of X in a concept Keeper[X] to
only subconcepts of Pet. As the set of possible parameter replacements can
be infinite and even uncountable, the generic extensions are, in general,
undecidable. To identify decidable generic DLs, we focus on the case of
terminologies, requiring that variables are only used in definitions of
generic concepts. We formulate restrictions that allow a reduction
of generic entailment to classical entailment and further conditions that
ensure decidability.
Revisiting Conjunctive Query Entailment for S
Authors: Yazmín Ibáñez-García; Jean Christoph Jung; Vincent Michielini; Filip Murlak
Venue: AAAI 2026 (main)

Abstract: We clarify the complexity of answering unions of conjunctive queries over knowledge bases formulated in the description logic S, the extension of ALC with transitive roles. Contrary to what existing partial results suggested, we show that the problem is, in fact, 2ExpTime-complete; hardness already holds in the presence of two transitive roles and for Boolean conjunctive queries. We complement this result by showing that the problem remains in coNExpTime when the input query is rooted or is restricted to use at most one transitive role (but may use arbitrarily many non-transitive roles).
Enumerating Minimal Unsatisfiable Cores of LTLf Formulae
Authors: Antonio Ielo; Giuseppe Mazzotta; Rafael Peñaloza; Francesco Ricca
Venue: AAAI 2026 (main)

Abstract: Linear Temporal Logic over finite traces (LTLf) is a widely used formalism with applications in AI, process mining, model checking, and more. 
The primary reasoning task for LTLf is satisfiability checking; yet, the recent focus on explainable AI has increased interest in analyzing inconsistent formulae, making the enumeration of minimal explanations for unsatisfiability a relevant task also for LTLf. 
We introduce a novel technique for enumerating minimal unsatisfiable cores (MUCs) of an LTLf specification. 
The main idea is to encode an LTLf formula into an Answer Set Programming (ASP) specification, such that the minimal unsatisfiable subsets (MUSes) of the ASP program directly correspond to the MUCs of the original LTLf specification.
Leveraging recent advancements in ASP solving yields an MUC enumerator achieving good performance in experiments conducted on established benchmarks from the literature.
Enhancing Strategy Logic with Procedural Rationality
Authors: Ruiqi Jin; Shuyi Li; Yongmei Liu
Venue: AAAI 2026 (main)

Abstract: ATL and Strategy Logic (SL) are important languages for representation and reasoning about strategic abilities of coalitions in multi-agent systems. In analyzing strategies of agents in multi-agent systems, an important concept to consider is rationality. Strategy Logic can express rationality concepts such as Nash Equilibrium (NE). Recently, there has been work on logics for joint abilities incorporating rationality concepts based on iterated elimination of dominated strategies (IEDS). Each of NE and IEDS has its strengths and limitations.  However, when the payoff is binary, e.g., whether a goal is satisfied, IEDS has more distinguishing power than NE. In this work, we propose Strategy Logic with IEDS (SL_{IEDS}), an extension of Strategy Logic with an IEDS operator, where we can reason about rational strategies that survive IEDS. We prove that SL_{IEDS} is strictly more expressive than SL. Finally, we prove that model checking memoryless SL_{IEDS} is EXPTIME-complete.
Causal, Strategic, and Combined Responsibility Attribution in Situation Calculus Concurrent Game Structures
Authors: MohammadHossein Karimian; Shakil M Khan; Yves Lesperance
Venue: AAAI 2026 (main)

Abstract: Responsibility is a central concept in accountable decision making for multiagent systems. As modern AI systems grow in complexity and autonomy, there is a growing demand for them to address issues in AI ethics, prompting researchers to formalize responsibility from diverse perspectives, including strategic responsibility. However, causal responsibility, i.e. responsibility due to actual causal contribution, has received much less attention. In this paper, we study variants of responsibility attribution from both strategic and causal perspectives within a synchronous game-theoretic logic framework that allows concurrent moves by multiple agents. Our formalization is based on Situation Calculus Synchronous Game Structures (SCSGS). We show that by combining these perspectives, one can obtain novel forms of responsibility attribution that are grounded on actual causation. While doing this, we propose an account of actual causation in SCSGS. We prove that our formalization handles the issues associated with preemption and over-determination well. We also study some key properties of responsibility and demonstrate that causal, strategic, and combined notions of responsibility are extensionally distinct.
Can You Tell the Difference? Contrastive Explanations for ABox Entailments
Authors: Patrick Koopmann; Yasir Mahmood; Axel-Cyrille Ngonga Ngomo; Balram Tiwari
Venue: AAAI 2026 (main)

Abstract: We introduce the notion of contrastive ABox explanations to answer questions of the type “Why is a an instance of C, but b is not?”. While there are various approaches for explaining positive entailments (why is C(a) entailed by the knowledge base) as well as missing entailments (why is C(b) not entailed) in isolation, contrastive explanations consider both at the same time, which allows them to focus on the relevant commonalities and differences between a and b. We develop an appropriate notion of contrastive explanations for the special case of ABox reasoning with description logic ontologies, and analyze the computational complexity for different variants under different optimality criteria, considering lightweight as well as more expressive description logics. We
implemented a first method for computing one variant of contrastive explanations, and evaluated it on generated problems for realistic knowledge bases.
Tractable Weighted First-Order Model Counting with Bounded Treewidth Binary Evidence
Authors: Václav Kůla; Qipeng Kuang; Yuyi Wang; Yuanhong Wang; Ondřej Kuželka
Venue: AAAI 2026 (main)

Abstract: The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. Conditioning WFOMC on evidence—fixing the truth values of a set of ground literals—has been shown impossible in time polynomial in the domain size (unless ♯P ⊆ FP) even for fragments of logic that are otherwise tractable for WFOMC without evidence. In this work, we address the barrier by restricting the binary evidence to the case where the underlying Gaifman graph has bounded treewidth. We present a polynomial-time algorithm in the domain size for computing WFOMC for the two-variable fragments ??² and ?² conditioned on such binary evidence. Furthermore, we show the applicability of our algorithm in combinatorial problems by solving the stable seating arrangement problem on bounded-treewidth graphs of bounded degree, which was an open problem. We also conducted experiments to show the scalability of our algorithm compared to the existing model counting solvers.
Robust Lazy Conflict Detection via Multi-Conflict Extraction and Genetic Diversity Control
Authors: Viet-Man Le; Lukas André Feldgrill; Alexander Felfernig
Venue: AAAI 2026 (main)

Abstract: Detecting minimal conflict sets is essential for providing meaningful feedback in knowledge-based configuration. While lazy conflict detection addresses runtime efficiency by predetermining conflict sets offline using a genetic algorithm, it suffers from low conflict coverage, stagnation, and instability. We propose a robust enhancement that integrates multi-conflict extraction and genetic diversity control to overcome these limitations. Our method extends conflict discovery per evaluation and introduces three diversity mechanisms: full population reproduction, weighted genetic operators, and adaptive extinction. Empirical evaluations on five real-world configuration knowledge bases show that our approach recovers up to 85% of conflict sets, reduces solver calls by up to 73%, and achieves higher result stability. These improvements demonstrate the scalability and reliability of enhanced lazy conflict detection for interactive configuration systems.
Consistency-based Abductive Reasoning over Perceptual Errors of Multiple Pre-trained Models in Novel Environments
Authors: Mario Leiva; Noel Ngu; Joshua Shay Kricheli; Aditya Taparia; Ransalu Senanayake; Paulo Shakarian; Nathaniel D. Bastian; John Corcoran; Gerardo Simari
Venue: AAAI 2026 (main)

Abstract: The deployment of pre-trained perception models in novel environments often leads to performance degradation due to distributional shifts. Although recent artificial intelligence approaches for metacognition use logical rules to characterize and filter model errors, improving precision often comes at the cost of reduced recall. This paper addresses the hypothesis that leveraging multiple pre-trained models can mitigate this recall reduction. We formulate the challenge of identifying and managing conflicting predictions from various models as a consistency-based abduction problem, building on the idea of abductive learning (ABL) but applying it to test-time instead of training. The input predictions and the learned error detection rules derived from each model are encoded in a logic program. We then seek an abductive explanation—a subset of model predictions—that maximizes prediction coverage while ensuring the rate of logical inconsistencies (derived from domain constraints) remains below a specified threshold. We propose two algorithms for this knowledge representation task: an exact method based on Integer Programming (IP) and an efficient Heuristic Search (HS). Through extensive experiments on a simulated aerial imagery dataset featuring controlled, complex distributional shifts, we demonstrate that our abduction-based framework outperforms individual models and standard ensemble baselines, achieving, for instance, average relative improvements of approximately 13.6% in F1-score and 16.6% in accuracy across 15 diverse test datasets when compared to the best individual model. Our results validate the use of consistency-based abduction as an effective mechanism to robustly integrate knowledge from multiple imperfect models in challenging, novel scenarios.
SITA: A Framework for Structure-to-Instance Theorem Autoformalization
Authors: Chenyi Li; Wanli Ma; Zichen Wang; Zaiwen Wen
Venue: AAAI 2026 (main)

Abstract: While large language models (LLMs) have shown progress in mathematical reasoning, they still face challenges in formalizing theorems that arise from instantiating abstract structures in concrete settings. With the goal of auto-formalizing mathematical results at the research level, we develop a framework for structure-to-instance theorem autoformalization (SITA), which systematically bridges the gap between abstract mathematical theories and their concrete applications in Lean proof assistant. Formalized abstract structures are treated as modular templates that contain definitions, assumptions, operations, and theorems. These templates serve as reusable guides for the formalization of concrete instances. Given a specific instantiation, we generate corresponding Lean definitions and instance declarations, integrate them using Lean’s typeclass mechanism, and construct verified theorems by checking structural assumptions. We incorporate LLM-based generation with feedback-guided refinement to ensure both automation and formal correctness. Experiments on a dataset of optimization problems demonstrate that SITA effectively formalizes diverse instances grounded in abstract structures.
Discovering Latent Facts from Context to Construct Richer Open Knowledge Graphs
Authors: Jinpeng Li; Hang Yu; Ziqi Ma; Peng Qi
Venue: AAAI 2026 (main)

Abstract: Knowledge graph construction (KGC) aims to extract valuable information from text and organize it into structured knowledge graphs (KGs). Recent methods have leveraged the strong generative capabilities of large language models (LLMs) to improve the generalization and reduce the labor costs. However, constrained by the input length of LLMs, existing methods mainly focus on extracting knowledge within individual texts and lack the capability to discover latent knowledge across texts. To fill this gap, we propose a novel method for open knowledge graph construction, termed KG-DLF. The core idea of this method is to enhance the knowledge graph construction process by discovering new facts that are consistent with the underlying contextual logic. Specifically, we first design a knowledge extractor to extract knowledge from the text. Then, a knowledge normalizer performs schema alignment on the extracted knowledge. Next, we explore a knowledge discoverer based on a clue search strategy, which leverages the logical consistency of context to mine latent facts. Finally, we design a counterfactual-based knowledge corrector, enabling the model to purify knowledge and reduce factual errors. Experimental results show that KG-DLF is capable of extracting comprehensive knowledge in open-world scenarios across three KGC benchmarks.