GenAI4ELab/papercli-papers huggingface dataset:
LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments
Authors: Till Hofmann; Jens Claßen
Venue: AAAI 2025 (main)

Abstract: We investigate the synthesis of policies for high-level agent programs expressed in Golog, a language based on situation calculus that incorporates nondeterministic programming constructs. Unlike traditional approaches for program realization that assume full agent control or rely on incremental search, we address scenarios where environmental nondeterminism significantly influences program outcomes. Our synthesis problem involves deriving a policy that successfully realizes a given Golog program while ensuring the satisfaction of a temporal specification, expressed in Linear Temporal Logic on finite traces (LTLf), across all possible environmental behaviors. By leveraging an expressive class of first-order action theories, we construct a finite game arena that encapsulates program executions and tracks the satisfaction of the temporal goal. A game-theoretic approach is employed to derive such a policy. Experimental results demonstrate this approach's feasibility in domains with unbounded objects and non-local effects. This work bridges agent programming and temporal logic synthesis, providing a framework for robust agent behavior in nondeterministic environments.
New Compilation Languages Based on Restricted Weak Decomposability
Authors: Petr Illner
Venue: AAAI 2025 (main)

Abstract: This paper introduces two new compilation languages restricting weak decomposable negation normal form (wDNNF) circuits and integrates them into the knowledge compilation map. Positive (resp. negative) wDNNF circuits restrict wDNNF circuits so that each variable shared among the inputs of a conjunction node can only have positive (resp. negative) occurrences in that subcircuit. Unlike wDNNF circuits, pwDNNF (resp. nwDNNF) circuits satisfy the maximum (resp. minimum) cardinality query. We present a compiler for converting CNF formulae into pwDNNF and nwDNNF circuits by extending Bella - the state-of-the-art compiler for wDNNF circuits. We introduce a new caching scheme, called Cara, that exploits isomorphism. Using that scheme, we show a new compilation method based on copying subcircuits, which may significantly speed up compilations at the expense of increasing circuit sizes. Our experiments demonstrate that nwDNNF circuits are suitable for computing most probable explanations (MPEs) in two-layer Bayesian networks (BNs) with large domains.
Hybrid Reasoning About Relative Position and Orientation of Objects and Navigating Agents Using Answer Set Programming
Authors: Yusuf Izmirlioglu
Venue: AAAI 2025 (main)

Abstract: We study reasoning about relative position, orientation and distance of moving objects in 2D space. We first construct a new hybrid calculus HOPA by augmenting qualitative distance and quantitative constraints into Oriented Point Relation Algebra (OPRA). Then we develop a framework for consistency checking and reasoning with HOPA using Answer Set Programming. This framework can also explain the source of inconsistency, infer new knowledge and generate a layout of objects and their orientation in the discrete space. The framework is capable of reasoning with (un)certain, heterogenous and presumed information. We evaluate efficiency and scalability of our method by computational experiments, and illustrate its applications with sample scenarios from robotic perception and marine navigation.
APKGC: Noise-enhanced Multi-Modal Knowledge Graph Completion with Attention Penalty
Authors: Yue Jian; Xiangyu Luo; Zhifei Li; Miao Zhang; Yan Zhang; Kui Xiao; Xiaoju Hou
Venue: AAAI 2025 (main)

Abstract: Multimodal knowledge graphs (MMKG) store structured world knowledge enriched with multimodal descriptive information. However, MMKG often faces the challenge of incompleteness. The primary objective of multimodal knowledge graph completion (MMKGC) is to predict missing entities within MMKG. Current MMKGC methods struggle with addressing the issue of over-trust attention and how to enhance the robustness of the model. To overcome these problems, we introduce APKGC, a noise-enhanced multimodal method for knowledge graph completion with attention penalty. APKGC effectively adjusts the attention scores in the language model and alleviates over-trust attention through a specifically designed attention penalty module. Additionally, an adaptive noise sampling module is proposed to supplement the entity's multimodal information, thereby enhancing the model's robustness. Experimental evaluation demonstrates that APKGC excels in overcoming these challenges. Compared to the existing state-of-the-art MMKGC model, APKGC improves Hit@1 by 3.3% on the DB15K dataset and by 3.4% on the MKG-W dataset.
A Modal Logic for Joint Abilities of Structured Strategies with Bounded Complexity
Authors: Ruiqi Jin; Yongmei Liu; Liping Xiong
Venue: AAAI 2025 (main)

Abstract: Coordination and joint ability are important topics in representation and reasoning about multi-agent systems. The modal logic JAADL proposed by Liu et al. extends ATL with joint abilities, which enables reasoning about whether a coalition of agents can coordinate and achieve a goal without communication. However, like ATL, strategic abilities in JAADL are defined in terms of combinatorial strategies, which are functions from histories or states to actions. On the other hand, there has been research on reasoning about natural strategic abilities, where a natural strategy is formalized as a sequence of condition-action pairs, making it more human-friendly than combinatorial strategy. In this work, we propose SJAADL, a variation of JAADL where strategic abilities are defined in terms of structured strategies represented with LDL (linear dynamic logic) formulas, with bounded complexity. We use nondeterministic strategies since they are more expressive, natural and succinct than determinstic ones. We present syntax and semantics of SJAADL. We show that model checking SJAADL can be done in time quasi-polynomial with the model size, exponential with the formula size,  and with the complexity bound of structured strategies, exponential in the memoryless case and double exponential in the memoryful case. Finally, we introduce the problem of synthesizing norms to achieve joint abilities, and give two algorithms for it.
Reasoning About Actual Causes in Nondeterministic Domains
Authors: Shakil M. Khan; Yves Lespérance; Maryam Rostamigiv
Venue: AAAI 2025 (main)

Abstract: Reasoning about the causes behind observations is crucial to the formalization of rationality. While extensive research has been conducted on root cause analysis, most studies have predominantly focused on deterministic settings. In this paper, we investigate causation in more realistic nondeterministic domains, where the agent does not have any control on and may not know the choices that are made by the environment. We build on recent preliminary work on actual causation in the nondeterministic situation calculus to formalize more sophisticated forms of reasoning about actual causes in such domains. We investigate the notions of “Certainly Causes” and “Possibly Causes” that enable the representation of actual cause for agent actions in these domains. We then show how regression in the situation calculus can be extended to reason about such notions of actual causes.
An Alternative Theory of Stable Revision for Nondeterministic Approximation Fixpoint Theory and the Relationships
Authors: Spencer Killen; Jia-Huai You; Jesse Heyninck
Venue: AAAI 2025 (main)

Abstract: Approximation fixpoint theory (AFT) is a robust and popular mathematical framework that characterizes many nonmonotonic semantics,  where the construction of stable fixpoints, called stable revision, play a central role.  Nondeterministic AFT is a recent development that redefines AFT for a nondeterministic setting to capture disjunctive semantics. This theory departs from traditional AFT by introducing distinct definitions, thus raising the question of whether deterministic AFT can be adopted directly to define nondeterministic stable revision. This work proposes such an alternate theory and creates a new way to study disjunctive semantics in terms of normal (non-disjunctive) knowledge bases. To demonstrate the viability of our framework, we show how to capture stable and partial stable models for disjunctive logic programs. We then study the relationships between this alternative theory and the state-of-the-art nondeterministic AFT.
On Action Theories with Iterable First-Order Progression
Authors: Daxin Liu; Jens Claßen
Venue: AAAI 2025 (main)

Abstract: We study the first-order definability of progression for situation calculus action theories with a focus on the iterability of progression. Progression, the task of updating a knowledge base according to actions' effects so that proper information is retained, is notoriously challenging as it in general requires second-order logic. Exceptions where progression is first-order like local-effect actions and normal actions impose certain syntax constraints on action theories to eliminate second-order quantifiers in the progressed knowledge base. Unfortunately, the progressed result might not satisfy the constraints again, making it impossible to apply first-order progression iteratively. In this paper, we first lift the existing result on first-order progression for normal actions by allowing disjunctions in the knowledge base. As a result, we obtain an action theory whose type is called disjunctive normal, which is iteratively first-order progressable. Second, we propose a new class of action theories, called PANACK, that strictly subsumes the disjunctive normal ones, and we show that it remains iteratively first-order progressable as well.
Scalable Knowledge Refactoring Using Constrained Optimisation
Authors: Minghao Liu; David M. Cerna; Filipe Gouveia; Andrew Cropper
Venue: AAAI 2025 (main)

Abstract: Knowledge refactoring compresses logic programs by replacing them with new rules. Current approaches struggle to scale to large programs. To overcome this limitation, we introduce a constrained optimisation refactoring approach. Our first key idea is to encode the problem with decision variables based on literals rather than rules. Our second key idea is to focus on linear invented rules. Our empirical results on multiple domains show that our approach can refactor programs quicker and with more compression than the previous state-of-the-art approach, sometimes by 60%.
Dung’s Argumentation Framework: Unveiling the Expressive Power with Inconsistent Databases
Authors: Yasir Mahmood; Markus Hecher; Axel-Cyrille Ngonga Ngomo
Venue: AAAI 2025 (main)

Abstract: The connection between inconsistent databases and Dung’s abstract argumentation framework has recently drawn growing interest. Specifically, an inconsistent database, involving certain types of integrity constraints such as functional and inclusion dependencies, can be viewed as an argumentation framework in Dung’s setting. Nevertheless, no prior work has explored the exact expressive power of Dung’s theory of argumentation when compared to inconsistent databases and integrity constraints. In this paper, we close this gap by arguing that an argumentation framework can also be viewed as an inconsistent database. We first establish a connection between subset-repairs for databases and extensions for AFs considering conflict-free, naive, admissible, and preferred semantics. Further, we define a new family of attribute-based repairs based on the principle of maximal content preservation. The effectiveness of these repairs is then highlighted by connecting them to stable, semi-stable, and stage semantics. Our main contributions include translating an argumentation framework into a database together with integrity constraints. Moreover, this translation can be achieved in polynomial time, which is essential in transferring complexity results between the two formalisms.
Spectra of Cardinality Queries over Description Logic Knowledge Bases
Authors: Quentin Manière; Marcin Przybyłko
Venue: AAAI 2025 (main)

Abstract: Recent works have explored the use of counting queries coupled with Description Logic ontologies. The answer to such a query in a model of a knowledge base is either an integer or infinity, and its spectrum is the set of its answers over all models. While it is unclear how to compute and manipulate such a set in general, we identify a class of counting queries whose spectra can be effectively represented. Focusing on atomic counting queries, we pinpoint the possible shapes of a spectrum over ALCIF ontologies: they are essentially the subsets of N and infinity closed under addition. For most sublogics of ALCIF, we show that possible spectra enjoy simpler shapes, being [ m, infinity ] or variations thereof. To obtain our results, we refine constructions used for finite model reasoning and notably rely on a cycle-reversion technique for the Horn fragment of ALCIF. We also study the data complexity of computing the proposed effective representation and establish the FP^NP[log]-completeness of this task under several settings.
Temporal Specification Optimisation for the Event Calculus
Authors: Periklis Mantenoglou; Alexander Artikis
Venue: AAAI 2025 (main)

Abstract: Temporal pattern matching tasks require the detection of situations of interest based on streams of symbolic events. The Run-Time Event Calculus (RTEC) is a formal framework that represents situations of interest as time-varying properties called 'fluents'. Temporal patterns often express 'Boolean combinations' of situations; RTEC features two types of fluents that may model such patterns: 'simple' and 'statically determined'. A simple fluent representation, however, is exponentially larger and more expensive to reason with than the corresponding statically determined fluent one. We formally identify the class of simple fluent definitions that can be translated into statically determined fluent definitions. Moreover, we present a compiler for the translation, and a reproducible empirical evaluation on real applications.
Consistent Query Answering over Existential Rules with Open and Closed Predicates
Authors: Lorenzo Marconi; Riccardo Rosati
Venue: AAAI 2025 (main)

Abstract: We study Consistent Query Answering (CQA) over knowledge bases with existential rules. Specifically, we propose a novel framework for CQA that combines previous approaches, allowing for the simultaneous presence of both open and closed predicates, i.e. predicates interpreted under open- and closed-world assumption, respectively. We establish the data complexity of answering unions of conjunctive queries in such a new framework under the so-called AR semantics and for different classes of existential rules. We also provide new complexity results for the standard (i.e. non-inconsistency tolerant) query answering in the presence of both open and closed predicates. Our results show that, for certain classes of rules, the complexity of CQA matches that of non-inconsistency-tolerant query answering.
Probabilistic Strategy Logic with Degrees of Observability
Authors: Chunyan Mu; Nima Motamed; Natasha Alechina; Brian Logan
Venue: AAAI 2025 (main)

Abstract: There has been considerable work on reasoning about the strategic ability of agents under imperfect information. However, existing logics such as Probabilistic Strategy Logic are unable to express properties relating to information transparency. Information transparency concerns the extent to which agents' behaviours and actions are observable by other agents. Reasoning about information transparency is useful in many domains including security, privacy, and decision-making. In this paper, we present a formal framework for reasoning about information transparency properties in stochastic multi-agent systems.  We extend Probabilistic Strategy Logic with new observability operators that capture the degree of observability of temporal properties by agents. We show that the model checking problem for the resulting logic is decidable.
An And-Sum Circuit with Signed Edges That Is More Succinct than SDD
Authors: Ryoma Onaka; Kengo Nakamura; Masaaki Nishino; Norihito Yasuda
Venue: AAAI 2025 (main)

Abstract: Knowledge compilation is a method of transforming knowledge into a compressed and tractable form for permitting more efficient operations. For Boolean functions, numerous representations have been proposed that enhance succinctness and tractability. In this paper, we introduce a new representation named structured Decomposable And-Sum Circuit (st-DASC), which employs AND and SUM nodes with signed edges, in place of the standard AND and OR nodes with unsigned edges. Notably, incorporating negative signs permits polytime logical negation. By following a knowledge compilation map, we show that st-DASCs are more succinct than Sentential Decision Diagrams (SDDs) while maintaining support for every operation on the knowledge compilation map that SDD supports. Furthermore, st-DASCs are even more succinct than structured d-DNNFs (st-d-DNNFs), which are more succinct than SDDs although they support fewer operations than SDDs. Accordingly, st-DASCs break the traditional trade-off between succinctness and tractability over SDDs and st-d-DNNFs.
Tensor Decomposition Meets Knowledge Compilation: A Study Comparing Tensor Trains with OBDDs
Authors: Ryoma Onaka; Kengo Nakamura; Masaaki Nishino; Norihito Yasuda
Venue: AAAI 2025 (main)

Abstract: A knowledge compilation map analyzes tractable operations in Boolean function representations and compares their succinctness. This enables the selection of appropriate representations for different applications. In the knowledge compilation map, all representation classes are subsets of the negation normal form (NNF). However, Boolean functions may be better expressed by a representation that is different from that of the NNF subsets. In this study, we treat tensor trains as Boolean function representations and analyze their succinctness and tractability. Our study is the first to evaluate the expressiveness of a tensor decomposition method using criteria from knowledge compilation literature. Our main results demonstrate that tensor trains are more succinct than ordered binary decision diagrams (OBDDs) and support the same polytime operations as OBDDs. Our study broadens their application by providing a theoretical link between tensor decomposition and existing NNF subsets.
A Logical Analysis of Hanabi
Authors: Elise Perrotin
Venue: AAAI 2025 (main)

Abstract: The card game Hanabi has recently gained popularity as a benchmark for handling epistemic reasoning in AI systems. However it has until now mostly been approached through the lens of machine learning rather than formal logical analysis. This is mostly due to the fact that modeling Hanabi in the standard epistemic logic DEL is untractable. In this paper we take a different approach to formalizing Hanabi, using the simple epistemic logic EL-O as a starting point. We generalize common knowledge in EL-O to arbitrary groups of agents and show how to overcome some of the limitations EL-O places on agent reasoning by introducing a special reasoning action. Analyzing our formalization of Hanabi finally leads us to introduce an alternative semantics for our generalization of EL-O in which models are finite and satisfiability checking is NP-complete, and which is enough to fully describe the evolution of knowledge in a game of Hanabi.
Checking Consistency of CP-Theory Preferences in Polynomial Time
Authors: Erik Rauer; Samik Basu; Vasant Honavar
Venue: AAAI 2025 (main)

Abstract: We investigate the problem of checking the consistency of qualitative preferences expressed in CP-theory. This problem is PSPACE-Complete even when the preferences are locally consistent or the preference variables have binary domain. We present a new sufficient condition for consistency of preferences and show that the condition can be checked in polynomial time in settings of practical relevance (locally consistent or binary domain preference variables). We further show how the resulting sufficient condition can be used to efficiently identify a subset of outcomes that are non-dominated with respect to a set of qualitative preferences.
Shield Synthesis for LTL Modulo Theories
Authors: Andoni Rodríguez; Guy Amir; Davide Corsi; César Sánchez; Guy Katz
Venue: AAAI 2025 (main)

Abstract: In recent years, Machine Learning (ML) models have achieved remarkable success in various domains. However, these models also tend to demonstrate unsafe behaviors, precluding their deployment in safety-critical systems. To cope with this issue, ample research focuses on developing methods that guarantee the safe behaviour of a given ML model. A prominent example is shielding which incorporates an ex- ternal component (a “shield”) that blocks unwanted behavior. Despite significant progress, shielding suffers from a main setback: it is currently geared towards properties encoded solely in propositional logics (e.g., LTL) and is unsuitable for richer logics. This, in turn, limits the widespread applicability of shielding in many real-world systems. In this work, we address this gap, and extend shielding to LTL modulo theories, by building upon recent advances in reactive synthesis modulo theories. This allowed us to develop a novel approach for generating shields conforming to complex safety specifications in these more expressive, logics. We evaluated our shields and demonstrate their ability to handle rich data with temporal dynamics. To the best of our knowledge, this is the first approach for synthesizing shields for such expressivity.
A Variable Occurrence-Centric Framework for Inconsistency Handling
Authors: Yakoub Salhi
Venue: AAAI 2025 (main)

Abstract: In this paper, we introduce  a syntactic framework  for analyzing and handling inconsistencies in propositional bases. Our approach focuses on examining  the  relationships between variable occurrences within conflicts. We propose two dual concepts: Minimal Inconsistency Relation (MIR) and Maximal Consistency Relation (MCR). Each MIR is a minimal equivalence relation on variable occurrences that results in inconsistency, while each MCR is a maximal equivalence relation designed to prevent inconsistency. Notably, MIRs capture  conflicts overlooked  by  minimal inconsistent subsets. Using MCRs, we develop a series of non-explosive inference relations. The main strategy involves restoring consistency by modifying the propositional base according to each MCR, followed by employing the classical inference relation to derive conclusions.  Additionally, we propose  an unusual semantics that assigns truth values to variable occurrences instead of the variables themselves. The associated inference relations are established through Boolean interpretations compatible with the occurrence-based models.