2024-03-28T16:42:22Z
https://kitami-it.repo.nii.ac.jp/oai
oai:kitami-it.repo.nii.ac.jp:00007951
2022-12-13T02:21:24Z
1:87
THEORETICAL BASIS FOR MAKING EQUIVALENT TRANSFORMATION RULES FROM LOGICAL EQUIVALENCES FOR PROGRAM SYNTHESIS
Miura, Katsunori
Akama, Kiyoshi
Mabuchi, Hiroshi
Koike, Hidekatsu
Equivalent transformation (ET) rule
Logical equivalence (LE)
Equivalence relationship of clause sets
Rule generation mapping (RGM)
LE in Class S
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.
journal article
ICIC International
2013-06
application/pdf
International Journal of Innovative Computing, Information and Control
6
9
2635
2650
https://kitami-it.repo.nii.ac.jp/record/7951/files/2013.06_Theoretical Basis for making Equivalent Transformation Rules from Logical Equivalences for Program Synthesis.pdf
eng
c 2013 ICIC International
open access