---
title: "Witnesses for Answer Sets of Basic Logic Programs"
authors:
  - "Yisong Wang"
  - "Xianglong Wang"
  - "Zhongtao Xie"
  - "Thomas Eiter"
doi: "10.24963/ijcai.2025/523"
url: "https://ijcai.org/proceedings/2025/523"
pdf: "https://ijcai.org/proceedings/2025/0523.pdf"
venue: "Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence"
year: 2025
pages: "4696-4705"
track: "Main Track"
keywords:
  - "AI Ethics, Trust, Fairness: ETF: Explainability and interpretability"
  - "Knowledge Representation and Reasoning: KRR: Logic programming"
---

# Witnesses for Answer Sets of Basic Logic Programs

Yisong Wang, Xianglong Wang, Zhongtao Xie, Thomas Eiter

*Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence*, pages 4696-4705. DOI: [10.24963/ijcai.2025/523](https://doi.org/10.24963/ijcai.2025/523)

## Abstract

Explanation plays an important role in the decisions of both symbolic and neural network-based AI systems.  Logic programs under answer set semantics (ASP) have been a typical declarative reasoning and problem-solving paradigm that has extensive applications in various AI domains. In this paper, we consider the issue of explanation for logic programs  with abstract constraint atoms (c-atoms) under SPT-answer set semantics. Such c-atoms are general  enough to capture complex constructors of logic programs, including aggregates, and the SPT-answer sets exclude circular justifications that other semantics  have. We propose a minimal reduct for logic programs with c-atoms that yields a new semantic characterization of SPT-answer sets, and then introduce  an extension of resolution for clauses with c-atoms. As we show, every atom in an SPT-answer set enjoys an extended resolution proof from the minimal reduct of its logic program. Finally, we present minimal sufficient subsets of logic programs
(witnesses) to structure such an extended resolution proof for an atom in an SPT-answer set. Our results  contribute to the justification of answer sets and provide a basis for explainability of ASP-based applications.