User Guided Abductive Proof Generation for Answer Set Programming Queries (Extended Version)

TL;DR

This paper introduces a novel method for abductive proof generation in Answer Set Programming that automatically constructs abducibles from rules, incorporates user facts, and generates justification graphs using ASP programs in Clingo.

Contribution

It presents a new bottom-up abductive approach for ASP that does not require modifying the solver, enabling automatic abducible construction and justification graph generation.

Findings

Automatically constructs abducibles from rules

Integrates user-provided facts into abductive reasoning

Produces justification graphs using ASP programs in Clingo

Abstract

We present a method for generating possible proofs of a query with respect to a given Answer Set Programming (ASP) rule set using an abductive process where the space of abducibles is automatically constructed just from the input rules alone. Given a (possibly empty) set of user provided facts, our method infers any additional facts that may be needed for the entailment of a query and then outputs these extra facts, without the user needing to explicitly specify the space of all abducibles. We also present a method to generate a set of directed edges corresponding to the justification graph for the query. Furthermore, through different forms of implicit term substitution, our method can take user provided facts into account and suitably modify the abductive solutions. Past work on abduction has been primarily based on goal directed methods. However these methods can result in solvers that are not truly declarative. Much less work has been done on realizing abduction in a bottom up solver like the Clingo ASP solver. We describe novel ASP programs which can be run directly in Clingo to yield the abductive solutions and directed edge sets without needing to modify the underlying solving engine.