@article{(Open Science Index):https://publications.waset.org/pdf/15050, title = {Generating Speq Rules based on Automatic Proof of Logical Equivalence}, author = {Katsunori Miura and Kiyoshi Akama and Hiroshi Mabuchi}, country = {}, institution = {}, abstract = {In the Equivalent Transformation (ET) computation model, a program is constructed by the successive accumulation of ET rules. A method by meta-computation by which a correct ET rule is generated has been proposed. Although the method covers a broad range in the generation of ET rules, all important ET rules are not necessarily generated. Generation of more ET rules can be achieved by supplementing generation methods which are specialized for important ET rules. A Specialization-by-Equation (Speq) rule is one of those important rules. A Speq rule describes a procedure in which two variables included in an atom conjunction are equalized due to predicate constraints. In this paper, we propose an algorithm that systematically and recursively generate Speq rules and discuss its effectiveness in the synthesis of ET programs. A Speq rule is generated based on proof of a logical formula consisting of given atom set and dis-equality. The proof is carried out by utilizing some ET rules and the ultimately obtained rules in generating Speq rules.}, journal = {International Journal of Computer and Information Engineering}, volume = {2}, number = {9}, year = {2008}, pages = {3097 - 3105}, ee = {https://publications.waset.org/pdf/15050}, url = {https://publications.waset.org/vol/21}, bibsource = {https://publications.waset.org/}, issn = {eISSN: 1307-6892}, publisher = {World Academy of Science, Engineering and Technology}, index = {Open Science Index 21, 2008}, }