Skip to content
Conference Open access

Abstracting the Indistinguishable in ASP

Sep 2026 · Proceedings of the Thirty-Fifth International Joint Conference on Artificial Intelligence · pp. 4044-4053 · 1 citation · 55 references

TL;DR

This work examines the computational complexity of existing abstraction techniques based on clustering (faithful and uniform abstractions) and proposes a novel syntactic operator to achieve uniform abstractions, when possible, and explores properties needed to reach abstractions from syntactic symmetry.

Abstract

Answer Set Programming (ASP) is a popular knowledge representation and reasoning framework with countless applications for modeling and solving combinatorial problems. With increasingly large applications, identifying crucial details and collapsing irrelevant or indistinguishable information becomes crucial for a human in the loop. This idea led to the investigation of different notions of abstraction, which relate to forgetting and projection. Very recently, clustering formalisms have been designed that also preserve program dependencies. However, crucial computational properties, such as finding abstractions, remained entirely unexplored to date. In this work, we examine the computational complexity of existing abstraction techniques based on clustering (faithful and uniform abstractions). Besides checking, we tackle the crucial question of constructing abstractions, by also proposing a novel syntactic operator to achieve uniform abstractions, when possible. Moreover, we investigate whether symmetry detection can be used to determine abstractable parts in a program, and give insights on the difference of interchangeability and indistinguishability, by introducing a relaxation of the uniform abstraction condition to capture semantic indistinguishability. We observe that this notion enables us to obtain intuitive faithful abstractions, while symmetry does not. We explore properties needed to reach abstractions from syntactic symmetry.

Read PDF

Similar papers

Sep 2026

Integration of Minimal Reasons in AMOSUM Constraints

This paper proposes and formalizes two new minimization algorithms that guarantee subset-minimal reasons and ensures cardinality-minimal reasons in the AMOSUM constraint and demonstrates that extending the solver wasp with these minimization strategies leads to substantial performance improvements.

Salvatore Fiorentino · 0 citations
Aug 2026

Refining Gelfond’s Rationality Principle: Towards More Comprehensive Foundational Principles for Answer Set Semantics

This work proposes to consider the three refined GAS principles as alternative principles for answer set semantics in general and for answer set and world view construction in particular and analyzes the computational complexity of well-supportedness and the rational answer set and world view semantics.

Yi-Dong Shen, Thomas Eiter · 0 citations
Preprint Sep 2026

Scenes: A Meta-Logical Algebra for Mutable State

Modelling of mutable state spaces and precisely describing how variables are manipulated in a program is a fundamental problem in compositional verification. Though we can make use of the embedded abstract syntax of a program for such analysis, this runs contrary to the shallow-embedding approach, and hampers efficient...

Simon Foster, Carlos Isasa, Christian Pardillo Laursen · 0 citations
#machine learning Preprint Aug 2026

ClosureBench: A Constructive Benchmark for Compositional Graph Reasoning

ClosureBench is introduced, a constructive benchmark for compositional graph-relational reasoning with programmatically verified ground truth with programmatically verified ground truth: each task's reference answer is computed by executing a program in the Ein tensor-logic language, ensuring machine-verified correctne...

S. Goria · 0 citations
Preprint Sep 2026

A Deeper Look at Depth: Stable Generation Accounting for Quantifier Reasoning

SMT solvers make automated verification convenient. At the same time, solvers suffer from instability, whereby seemingly inconsequential changes to the input may cause a previously quickly produced proof to fail or time out. This paper addresses a common cause of outcome instability (i.e., unsat/unknown fluctuations) i...

Can Cebeci, Nikolaj S. Bjørner, George Candea et al. · 0 citations

Crimps: Indexical Separation Logics for Order-Invariant Specifications

Crimp is introduced, a generic higher-order function formalised over a non-standard separation algebra that can be instantiated to capture diverse order-invariant properties of varied imperative data structures and gives rise to a natural separation logic, indexical separation logic, for localising and reflecting state...

Unknown authors · 0 citations

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.