Research on Inverse Entailment in Nonmonotonic Logic Programming

在这项研究中，我们提出了实现非单调逻辑编程归纳的技术。我们首先介绍了一个算法，通过反转蕴涵来推导假设。接下来，我们介绍了一种方法计算归纳假设使用答案集在非单调逻辑编程。进一步的细节解释如下。逆蕴涵是归纳法的一种基本技术，它在小句逻辑程序中演绎地构造归纳假设。当背景理论是一个非单调逻辑程序，然而，目前的IE技术不能使用。主要原因是IE是基于一阶逻辑中的演绎定理，而这在一般的非单调逻辑中并不成立。为了解决这个问题，我们在非单调逻辑程序中建立了一个新的蕴涵定理。我们构造了非单调ILP中的IE理论，并给出了从正反例学习非单调逻辑程序的归纳算法.回答集程序设计（ASP）是近年来备受关注的一种新的逻辑程序设计范式. ASP将程序看作是一组约束条件，每个解都必须满足这些约束条件，然后从程序的答案集合中抽取出解。在这项研究中，我们展示了一种方法，构建归纳假设使用答案集。在这种情况下，背景理论和例子的工作作为约束条件的归纳假设应满足的，和非单调逻辑程序的归纳是通过计算程序的答案集。结果表明，基于逆蕴涵的归纳是可计算的证明程序的答案集规划的非单调逻辑规划。

In this research, we propose techniques for realizing induction in nonmonotonic logic programming. We first introduce an algorithm to induce hypotheses by inverting entailment. Next, we introduce a method for computing inductive hypotheses using answer sets in nonmonotonic logic programming. Further details are explained as follows.1. Inverse entailment (IE) is known as a basic technique for induction, which deductively constructs inductive hypotheses in clausal logic programs. When a background theory is a nonmonotonic logic program, however, the present IE technique cannot be used. The primary reason is that IE is based on the deduction theorem in first-order logic, which does not hold in nonmonotonic logics in general. To solve the problem, we establish a new entailment theorem in nonmonotonic logic programs. We construct a theory of IE in nonmonotonic ILP and present an induction algorithm to learn nonmonotonic logic programs from positive and negative examples.2. Answer set programming (ASP) is a new paradigm of logic programming which attracts much attention recently. ASP views a program as a set of constraints which every solution should satisfy, then extracts solutions from the collection of answer sets of the program. In this research we show a method of constructing inductive hypotheses using answer sets. In this setting, the background theory and examples work as constraints which inductive hypotheses should satisfy, and induction in nonmonotonic logic programs is realized by computing answer sets of a program. The result implies that induction based on inverse entailment is computable by proof procedures for answer set programming in nonmonotonic logic programming.