User Guided Abductive Proof Generation for Answer Set Programming Queries

We present a method for calculating 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 inputed facts, our method is able to infer any additional facts that may be needed for the entailment of a query and output a set of directed edges representing  a justification tree, all without the user needing to explicitly specify the space of abducibles. Furthermore our method is able to take user supplied facts into account and adapt the proofs accordingly. Past work in implementing abductive reasoning systems has been primarily based on top-down execution methods with prolog as the underlying engine. Recently sCASP has been proposed as a goal directed ASP engine which is able to incorporate abduction but it too uses a top-down execution mechanism which can sometimes suffer from issues like a lack of true declaritivity. Furthermore, there maybe use cases where one wants to know all the resulting consequences of an abductive solution to a query with respect to a rule-set. Much less work has been done on realizing abduction purely in a bottom up ASP solver like Clingo. After describing and explaining our encodings, we establish the appropriate proof search completeness and finiteness results. Central to our methods is the use of Clingo ASP's choice rules and weak constraints features.  

Estimated publication date: September 2022.