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.
翻译:我们提出一种方法,用以对特定回答设置程序(ASP)规则的查询提供可能的证明,该规则是使用一种诱拐过程,即只根据输入规则自动建造可复制的空间。鉴于一组用户(可能是空的)提供了事实,我们的方法推断出任何可能为引起查询而需要的其他事实,然后又输出这些额外事实,而用户不需要明确具体说明所有可复制的空间。我们还提出一种方法,用来产生一套与查询理由图表相对应的定向边缘。此外,通过不同形式的隐含术语替代,我们的方法可以考虑到用户提供的事实,并适当修改绑架解决办法。过去关于绑架问题的工作主要基于目标定向方法,但是这些方法可以产生并非真正具有宣示性的解决者。在像Clingo ASP求解者这样的下层解决者中实现绑架问题的工作要少得多。我们描述了可以在Clingo直接运行的新型ASP程序,以产生绑架解决办法和定向边缘装置,而无需修改基本解决引擎。