2022-01-20T08:30:37Zhttps://kitami-it.repo.nii.ac.jp/oaioai:kitami-it.repo.nii.ac.jp:000079512021-09-07T05:07:56Z1THEORETICAL BASIS FOR MAKING EQUIVALENT TRANSFORMATION RULES FROM LOGICAL EQUIVALENCES FOR PROGRAM SYNTHESISMiura, KatsunoriAkama, KiyoshiMabuchi, HiroshiKoike, Hidekatsuc 2013 ICIC InternationalEquivalent transformation (ET) ruleLogical equivalence (LE)Equivalence relationship of clause setsRule generation mapping (RGM)LE in Class STo propose methods for making Equivalent Transformation (ET) rules is\nimportant for generating correct and sufficiently efficient programs from a speci cation\nwhich is a set of logical formulas. An ET rule is a procedure for replacing a clause\nset with another one while preserving declarative meaning. This paper proposes a new\nmethod for making ET rules via a Logical Equivalence (LE) from a speci cation. An LE\ndescribes an equivalence relationship between two logical formulas under some speci ed\npreconditions. We newly formulate an LE and de ne the correctness of LEs with respect\nto a speci cation. It is guaranteed by the method of this paper that an ET rule can be\nmade from a correct LE. The method is useful for the generation of various programs.\nMany ET rules included in programs which solve constraint satisfaction problems, can be\nmade by the method.ICIC International2013-06engjournal articlehttps://kitami-it.repo.nii.ac.jp/records/7951International Journal of Innovative Computing, Information and Control9626352650https://kitami-it.repo.nii.ac.jp/record/7951/files/2013.06_Theoretical Basis for making Equivalent Transformation Rules from Logical Equivalences for Program Synthesis.pdfapplication/pdf229.5 kB2016-11-22