A Technique for Prolog Program Synthesis by Doing without Most General Atoms

神奈川県茅ヶ崎市 E.Y. Shapiro proved that any Prolog-program is constructed by means of an iteration of the following four operations: (1) An addition of an atom to a head of a Horn clause (2) A unification of two variables (3) A unification of a variable and a function (4) An addition of the most general agom to a body. It is indeterminate to obtain the most general atom needed in the operation (4). Therefore in this investigation the inductive model-inference algorithm proposed by Shapiro has been implemented with C-language without using the most general atom. It is easy to control the program-synthesis in this method, but a space of hypotheses increases explosively in the size. We shall show that the contradiction-backtracing is reduced to the inverse application—order of the resolution principle