Solving logical problems by equivalent transformation

In logic programming, computation is regarded as inference. In this paper, we propose a new method to solve logical problems by equivalent transformation and develop a theoretical foundation for the correctness of the method. Given a logic program P and a query q, A logical problem < P, q > is formalized as finding the set L(P, q) of all ground instances g of q such that P satisfies= g. The set L(P, q) is represented by the declarative semantics of a logic program P' that is produced from P and q. The logical problem < P, q > is solved by transforming P' equivalently into a simpler form, preserving its declarative semantics and utilizing many transformation rules. Inferential (resolution-based) problem solving can be regarded as a special case of the proposed method.