論理的問題の等価変換による解法(2) : SLD導出の限界

概要

論文の詳細を見る
Logic programming has successfully solved many problems in terms of inference. Given a logic program P and a query q, Prolog finds substitutions θ such that P|=qθ in terms of inference. The theory of SLD resolution provides Prolog with a theoretical foundation, proving that SLD resolution is a sound and complete procedure for logical problems. It should be pointed out, however, that SLD resolution is not the best way to solve logical problems. For instance, SLD resolution imposes some unneccessary restrictions on the control of computation. These restrictions make the cost of computation control more expensive and, conversely, adoption of low-cost control would make computation less flexible, as can be seen in the Prolog case. This paper adopts a new method of problem solving, where problems are solved by equivalent transformation (ET) of declarative descriptions, preserving their declarative semantics. We prove that the class of SLD resolution can be embeded into the class of ET computation. Thus, we can do away with SLD resolution to solve logical problems, and therefore the unnecessary restrictions of SLD resolution are overcome. The new method, which has more freedom with respect to not only computation rules but also transformation rules, is expected to overcome many of the difficulties that result from the "inference-only" method is logic programming.
1998-11-01