论文标题
目标指导的约束答案集编程的理由
Justifications for Goal-Directed Constraint Answer Set Programming
论文作者
论文摘要
道德和法律问题使得可能直接影响人们的生活(例如,法律或健康咨询)的计划,以人为理解的术语来证明其建议。答案集编程具有丰富的语义,使得非常简洁的表达复杂的知识成为可能。但是,证明为什么答案是ASP程序的结果可能是不平凡的 - 甚至当用户是给定域中的专家时,但不一定在ASP中知识渊博的时候。大多数ASP系统使用SAT解决程序在基本规则上产生答案,这些程序与人类感知推理的看法不符。我们建议使用S(CASP),这是一个与谓语ASP的查询驱动的,自上而下的执行模型,该模型具有约束,以生成(约束)答案集的理由树。 S(CASP)的操作语义依赖于向后的链接,这是直观的,它可以跟随并借此生成更容易转化为自然语言的解释。我们展示了S(CASP)如何为文献中提出的相关示例提供最小的理由,包括搜索树,但更重要的是,作为自然语言的解释。我们通过实际的ASP应用程序验证了设计,并评估生成S(CASP)依据树的成本。
Ethical and legal concerns make it necessary for programs that may directly influence the life of people (via, e.g., legal or health counseling) to justify in human-understandable terms the advice given. Answer Set Programming has a rich semantics that makes it possible to very concisely express complex knowledge. However, justifying why an answer is a consequence from an ASP program may be non-trivial -- even more so when the user is an expert in a given domain, but not necessarily knowledgeable in ASP. Most ASP systems generate answers using SAT-solving procedures on ground rules that do not match how humans perceive reasoning. We propose using s(CASP), a query-driven, top-down execution model for predicate ASP with constraints to generate justification trees of (constrained) answer sets. The operational semantics of s(CASP) relies on backward chaining, which is intuitive to follow and lends itself to generating explanations that are easier to translate into natural language. We show how s(CASP) provides minimal justifications for, among others, relevant examples proposed in the literature, both as search trees but, more importantly, as explanations in natural language. We validate our design with real ASP applications and evaluate the cost of generating s(CASP) justification trees.