論理的問題の等価変換による解法(1) : その理論的基礎

概要

論文の詳細を見る
In logic programming, computation is regarded as inference. Given a logic program P and a query q, Prolog finds substitutions θsuch that P|=qθ in terms of inference. It is widely believed that inference is the unique and best way to solve logical problems. Many extensions of logic programming based on logical inference have also been developed. However, it has never been proved that logical inference is the best way to solve logical problems. In this paper, we propose a new method to solve logical problems, without relying on inferential methods. Firstly, a logical problem is reformulated to find the set L(P, q) of all ground instances g of q such that P|=g. Secondly, it is proved that the set L(P, q) can be transformed into another form f(M(P')), i.e., it is represented by declarative semantics of a program P' determined by P and q. Finally, equivalent transformation (ET) is proposed as a new method for solving logical problems. In the new method, P' is transformed equivalently to a simpler form, preserving its declarative semantics and utilizing many transformation rules. This theory provides a theoretical foundation for a more general class of problem solving than the logical inference in logic programming.
社団法人人工知能学会の論文
1998-11-01