Rule-Based Abduction for Logic Programming

Ph.D.ThesisIn order to capture the nature of inference, a philosopher Peirce classified inference into three fundamental kinds: deduction, induction, and abduction. In this classification, which based on the form of syllogisms, abduction is characterized as the inference of a case A from a rule $ A \rightarrow C $ and a result C. Furthermore, he also placed these three kinds of inference at each stage of scientific inquiry. According to him, every scientific inquiry begins with an observation of a surprising fact. The first stage, abduction, of scientific inquiry proposes a hypothesis to explain why the fact arises. The second stage, deduction, derives new conclusions from the hypothesis. The third stage, induction, tests empirically or corroborates the hypothesis and the conclusions. Hence, abduction is not only a kind of inference, but also a method of scientific discovery. The inference schema of abduction as the first stage of scientific inquiry is described in the following three steps: 1. A surprising fact C is observed. 2. If A were true, then C would be a matter of course. 3. Hence, there is reason to suspect that A is true. In computer science, the second stage, deduction, has been developed from viewpoints of automated theorem proving and logic programming. The third stage, induction, has been studied from viewpoints of inductive inference and machine learning. For the first stage, abduction, there are also many researches in various fields. In order to systematically understand them and clearly discuss abduction, first we classify abduction into five types: rule-selecting abduction, rule-finding abduction, rule-generating abduction, theory-selecting abduction, and theory-generating abduction. In this thesis, we examine such various researches on abduction so far developed, and show that most of them can be placed in our classification. Furthermore, we investigate the first three types of abduction, which we call together rule-based abduction, for logic programming. The rule-selecting abduction for logic programming is abduction which selects a rule in a program and proposes a hypothesis to explain a surprising fact. From the philosophical viewpoint we mentioned above, we should consider the process of abduction which terminates. Hence, it is a main purpose in this thesis to identify the class of logic programs for which the process of abduction terminates. We first introduce the concept of head-reducing programs. Then, we show that all the derivations for a head-reducing program and a surprising fact are finite. Hence, all the processes of rule-selecting abduction for a head-reducing program are finite. In general, abduction is closely related to nonmonotonic reasoning. Thus, in this thesis, we compare rule-selecting abduction with default logic. In order to formulate the rule-selecting abduction for default logic, we define a surprising fact and a hypothesis in the default logic. We show that, if there exists a hypothesis which explains a surprising fact, then there also exists an extension of a given default theory, which includes the surprising fact. This extension is corresponding to the least Herbrand model of the definite program obtaining from the default theory. Furthermore, we extend the concept of head-reducingness to that of breadth-first head-reducing programs, and the rule-selecting abduction to the breadth-first ruleselecting abduction. We also show that there exists a finite derivation for a breadthfirst head-reducing program and a surprising fact. Hence, the process of breadth-first rule-selecting abduction for a breadth-first head-reducing program is finite. The rule-finding abduction for logic programming is abduction which finds a rule in a program in the set of programs and proposes a hypothesis to explain a surprising fact. In rule-finding abduction, we are interested in how to choose programs from the set of programs. Then, we pay our attention to choosing programs for which the process of rule-finding abduction terminates. We introduce two concepts of loop-pair and loop-elimination. The loop-pair syntactically determines whether or not there exists an infinite process of rule-finding abduction for the choice of programs. We show that, if a loop-pair appears in a derivation, then the derivation becomes infinite. On the other hand, the loop-elimination is a transformation of programs. By using loop-elimination, we can choose the programs for which rule-finding abduction terminates. We also show that, for given two programs, if we transform one program by loop-elimination, then all the derivations for union of the transformed program and the rest are finite. In other words, by loop-elimination, we can choose the programs whose proof trees have no infinite branches. In this thesis, we also discuss analogical reasoning from the viewpoint of abduction. In this thesis, we adopt the formulation of analogical reasoning by Haraguchi and Arikawa. In their formulation, the main problem is how to detect an analogy. In order to solve this problem, we also adopt the concept of partial isomorphic generalizations. By using these concepts, we introduce the concept of deducible hypotheses, and formulate rule-finding abduction with analogy. We show that a deducible hypothesis is correct in the sense of analogical reasoning, and show that it is polynomial time computable with respect to the length of a surprising fact and the size of a proof tree. We design an algorithm of rule-finding abduction with analogy, and realize it as a Prolog program. The rule-generating abduction for logic programming is abduction which generates a rule and proposes a hypothesis to explain a surprising fact. In rule-generating abduction, only one surprising fact is given. In order to generate a rule and propose a hypothesis, we need to generalize the surprising fact. When we deal with generalizations, we should avoid overgeneralization. It should be determined whether or not a generalization is overgeneral by an intended model. However, it is hard to give in advance such an intended model in our rule-generating abduction. Hence, we introduce a syntactical generalization of one atom, called a safe generalization. In general, an atom is regarded as a relation between its arguments. Then, for safe generalizations, common ground terms are replaced by common variables. If the class of definite programs is not restricted to some subclass, there may be infinitely many meaningless hypotheses. Hence, we introduce the subclass of headreducing programs, called weakly 2-reducing programs. However, without any heuristic, the number of weakly 2-reducing rules for rule-generating abduction also increases in exponential order with respect to the length of a surprising fact. On the other hand, safe generalizations in this class are characterized by only two types of substitutions. Hence, by using two types of safe generalizations, we design an efficient algorithm of rule-generating abduction for weakly 2-reducing programs. The number of rules and hypotheses obtained by this algorithm is at most the number of the arguments in a surprising fact. We show that this algorithm generates rules and proposes hypotheses in polynomial time with respect to the length of a surprising fact. Furthermore, we show that the selected common list in some argument of a surprising fact appears in the same argument of the hypothesis proposed by this algorithm