Creation of ET Rules via Logical Equivalence

摘要

A correct program can be created by accumulating rules (ET rules) that transform definite clauses equivalently by replacing some atom in a clause with conjunction of atoms. A method for creating ET rules is very important. How- ever, such techniques for human programmers have never been established. In this paper, we propose a method for creating ET rules based on logical equivalence for correct- ness of rules, and on simplification patterns for assurance of simpler result. It is expected that an effective method of algorithm construction will be given by using the proposed method together with the squeeze method, i.e., by successive accumulation of ET rules created by the proposed method.