Analogical logic program synthesis algorithm that can refute inappropriate similarities

Abstract

This paper presents an algorithmic learning theory for analogical synthesis of logic programs from their examples. An analogical synthesizer is defined as a kind of inductive inference machine that uses analogy. More precisely speaking, it synthesizes target programs from their examples, given a source program to which the target programs should be similar. One of the difficulties in realizing an efficient analogical synthesizer is to distinguish useless and inappropriate similarities from the other. A similarity is inappropriate if every similar program with respect to the similarity is not correct. If our synthesizer cannot refute such similarities then it would waste computational resources without succeeding to find a desired program.

To cope with this hard problem on analogical synthesis, this paper first applies the notion of refutably inferable class of linear programs, and obtains a basic synthesizer. It has a function of refuting inappropriate similarities. Secondly this paper investigates another method of refuting inappropriate similarities, using an analogous technique that has been employed for theorem proving with abstraction. Incorporating this method into the basic synthesizer, we obtain a more efficient one. All the synthesizers presented in this paper are proved to identify a similar correct program in the limit, given a source program.