@article{oai:kitami-it.repo.nii.ac.jp:00007951,
 author = {Miura, Katsunori and Akama, Kiyoshi and Mabuchi, Hiroshi and Koike, Hidekatsu},
 issue = {6},
 journal = {International Journal of Innovative Computing, Information and Control},
 month = {Jun},
 note = {To propose methods for making Equivalent Transformation (ET) rules is
important for generating correct and sufficiently efficient programs from a speci cation
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 speci cation. An LE
describes an equivalence relationship between two logical formulas under some speci ed
preconditions. We newly formulate an LE and de ne the correctness of LEs with respect
to a speci cation. 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.},
 pages = {2635--2650},
 title = {THEORETICAL BASIS FOR MAKING EQUIVALENT TRANSFORMATION RULES FROM LOGICAL EQUIVALENCES FOR PROGRAM SYNTHESIS},
 volume = {9},
 year = {2013}
}