@article{oai:barrel.repo.nii.ac.jp:00005215,
 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 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.},
 pages = {2635--2650},
 title = {THEORETICAL BASIS FOR MAKING EQUIVALENT TRANSFORMATION RULES FROM LOGICAL EQUIVALENCES FOR PROGRAM SYNTHESIS},
 volume = {9},
 year = {2013}
}