Generating Speq Rules based on Automatic Proof of Logical Equivalence
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.
[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.
[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.
@article{"International Journal of Information, Control and Computer Sciences:64047", author = "Katsunori Miura and Kiyoshi Akama and Hiroshi Mabuchi", title = "Generating Speq Rules based on Automatic Proof of Logical Equivalence", 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", volume = "2", number = "9", pages = "3243-9", }
