Generating Speq Rules based on Automatic Proof of Logical Equivalence

Authors: Katsunori Miura, Kiyoshi Akama, Hiroshi Mabuchi

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.

Keywords: Equivalent transformation, ET rule, Equation of two variables, Rule generation, Specialization-by-Equation rule

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1084292

References:

[1] Akama,K. , Y.Shigeta and E.Miyamoto, Solving logical problems by equivalent transformation - a theoretical foundation, Journal of the Japanese Society for Artificial Intelligence (in Japanese), vol.13, pp.928-935, 1998.
[2] Akama, K., E.Nantajeewarawat and H.Koike, Program generation in the equivalent transformation computation model using the squeeze method, Proc. of PSI2006, LNCS4378, Springer-Verlag Berlin Heidelberg, pp.41-54, 2007.
[3] Harada,M., T.Mizuno and S.Hamada, Executable C++ Program Generation form the Structured Object-oriented Design Diagrams, Transactions of Information Processing Society of Japan (in Japanese), vol.40, no.7, pp.2988-3000, 1999.
[4] Higashino,T, M.Mori, T.Sugiyama, K.Taniguchi and T.Kasami, An algebraic specification of HDLC procedures and its verification, The IEICE Transactions on Information and Systems (in Japanese), vol.SE- 10, no.6, pp.825-836, 1984.
[5] Hopkins,J., Component primer, Communications of the ACM, vol.43, no.10 pp.27-30, 2000.
[6] IBM San Francisce, Concepts and facilities, IBM Corporation, 1977 Project, Software Development, vol.6, no.2, 1998.
[7] Ikeda,M., T.Nakamura, Y.Takata and H.Seki, Algebraic Specification of User Interface and Its Automatic Implementation, The Special Interest Group Notes of IPSJ (in Japanese), vol.2001, no.114, pp.9-16, 2001.
[8] Jaffar,J. and M.Maher, Constraint logic programming, A survey, Journal of Logic Programming, vol.19/20, pp.503-581, 1994.
[9] Koike,H. , K.Akama and E.Boyd, Program synthesis by generating equivalent transformation rules, Proc. of the 2nd International Conference on Intelligent Technologies, Bangkok, Thailand, pp.250-259, 2001.
[10] Lloyd,J.W., Foundations of Logic Programming, 2nd Edition, Springer- Verlag, 1987.
[11] Lu,Yiguang, H.Awaya, H.Seki, M.Fujii and K.Ninomiya, On a Translation from Algebraic Specifications of Abstract Sequential Machines into Programs, The IEICE Transactions on Information and Systems (in Japanese), vol.J73-D-I, no.2, pp.201-213, 1990.
[12] Mabuchi,H. , K.Akama and T.Wakatsuki, Equivalent transformation rules as components of programs, International Journal of Innovative Computing, Information & Control, vol.3, no.3, pp.685-696, 2007.
[13] Miura,K. , K.Akama and H.Mabuchi, Creation of ET Rules from Logical Formulas Representing Equivalent Relations, International Journal of Innovative Computing, Information & Control, vol.5, (no.4 or no.5), 2009 (to appear).
[14] Nishida,Y. , K.Akama and H.Koike, An experimental programgeneration system based on meta-computation, Technical report of the Institute of Electronics, Information and Communication Engineers (in Japanese), Matsue, Japan, pp.31-36, 2007.
[15] Sterling,L. and E.shapiro, The Art of Prolog: Advanced Programming Techniques, MIT Press, second edition,
[16] Szyperski,C., Component software: Beyond object-oriented programming, Addison-Wesley, 1999.
[17] van Hentenryck,P., Constraint logic programming, The Knowledge Engineering Review, vol.6, no.3, pp.151-194, 1991.
[18] Wakatsuki,T., K.Akama and H.Mabuchi, A Framework for Synthesizing low-level Imperative Programs From Deterministic Abstract Programs, Technical report of the Institute of Electronics, Information and Communication Engineers (in Japanese), vol.107, no.392, pp.37- 42, 2007.