论文标题
用户指导的绑架式证明生成答案集编程查询（扩展版本）
User Guided Abductive Proof Generation for Answer Set Programming Queries (Extended Version)
论文作者
论文摘要
我们提出了一种使用绑架过程，仅根据输入规则自动构造出依从物的空间，以生成有关给定答案集编程（ASP）规则集的可能查询证明的方法。给定一组（可能是空的）用户提供的事实，我们的方法渗透了需要查询可能需要的任何其他事实，然后输出这些额外的事实，而无需用户需要明确指定所有占有不利的空间。我们还提出了一种生成与查询的理由图相对应的有向边的方法。此外，通过不同形式的隐式术语替换，我们的方法可以考虑用户提供的事实，并适当修改绑架解决方案。过去的绑架工作主要基于目标定向方法。但是，这些方法可能会导致并非真正声明的求解器。关于实现绑架者（如Clingo ASP求解器）进行绑架的工作要少得多。我们描述了可以直接在Clingo中运行的新型ASP程序，以产生绑架解决方案和定向边缘集，而无需修改基础求解引擎。
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.
