THEORETICAL BASIS FOR MAKING EQUIV ALENT TRANSFORMATION RULES FROM LOGICAL EQUIV ALENCES FOR PROGRAM SYNTHESIS
Katsunori Miura, Kiyoshi Akama, Hiroshi Mabuchi, Hidekatsu Koike, K Miura · Institutional Repositories DataBase (IRDB) · 2013
To propose methods for making Equivalent Transformation (ET) rules is important for generating correct and sufficiently efficient programs from a specification which is a set of logical formulas. An ET rule is a procedure for replacing a clause set with another one while preserving declarative meaning. This paper proposes a new method for making ET rules via a Logical Equivalence (LE) from a specification. An LE describes an equivalence relationship between two logical formulas under some specified preconditions. We newly formulate an LE and define the correctness of LEs with respect to a specification. It is guaranteed by the method of this paper that an ET rule can be made from a correct LE. The method is useful for the generation of various programs. Many ET rules included in programs which solve constraint satisfaction problems, can be made by the method.