Dynamic term rewriting calculus and its application to inductive equational reasoning

  • Su Feng
  • Toshiki Sakabe
  • Yasuyoshi Inagaki
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 722)


Dynamic Term Rewriting Calculus (DTRC) is a new computation model proposed by the authors for the purpose of formal description and verification of algorithms treating Term Rewriting Systems (TRSs). The computation of DTRC is basically term rewriting. The characteristic features of DTRC are dynamic change of rewriting rules during computation and hierarchical declaration of not only function symbols and variables but also rewriting rules. These features allow us to program meta-computation of TRSs in DTRC, i.e., we can implement in DTRC in a natural way those algorithms which manipulate TRSs as well as those procedures which verify such algorithms. We show here that we can use DTRC to represent the proof of an inductive theorem of an equational axiom system, i.e., we can translate the statements of base and induction steps in the proof of the inductive theorem into a DTRC term. The translation reduces the proof of the statements into the evaluation of the DTRC term.


Normal Form Function Symbol Operational Semantic Reduction Sequence Structural Induction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Feng S., Sakabe T. and Inagaki Y.: “Dynamic Term Rewriting Calculus and its Application”, IEICE Technical Report, COMP 91-47, pp. 31–40, 1991. (in Japanese)Google Scholar
  2. 2.
    Feng S., Sakabe T. and Inagaki Y.: “Interpretation of Conditional Term Rewriting System by DTRC”, Proc. of 9th Conference of Japan Society for Software Science and Technology, pp. 313–316, September 1992Google Scholar
  3. 3.
    Feng S., Sakabe T. and Inagaki Y.: “Confluence and Termination of Dynamic Term Rewriting Calculus”, to be submitted.Google Scholar
  4. 4.
    Huet G. and Hullot J. M.: “Proofs by Induction in Equational Theories with Constructors”, Rapports de Recherch, INRIA,28(1980).Google Scholar
  5. 5.
    Huet G. and Lang B.: “Proving and applying program transformations expressed with second-order logic”, Acta Informatica, 11, pp. 31–55, 1978.CrossRefGoogle Scholar
  6. 6.
    Huet G. and Oppen D.: “Equations and rewrite rules: A survey”, In R. Book, ed., Formal Language Theory: Perspectives and Open Problems, pp. 349–405, Academic Press, New York, 1980.Google Scholar
  7. 7.
    Jouannaud J. P. and Kounalis E.: “Proof by induction in equational theories without constructors”, Proc. of 1st Symp. on Logic In Computer Science, pp. 358–366, Boston, USA, 1986Google Scholar
  8. 8.
    Klint P.: “A meta-environment for generating programming meta-environments”, In J. A. Bergstra and L. M. G. Feijs, eds., Algebraic Methods II: Theory, Tools, and Applications, pp. 105–124. LNCS 490, 1991.Google Scholar
  9. 9.
    Knuth D. E. and Bendix P.: “Simple word problems in universal algebra”, In J. Leech, ed., Computational Problems in Abstract Algebra, pp. 263–297. Oxford, Pergamon Press, 1970.Google Scholar
  10. 10.
    Kounalis E. and Rusinowitch M., “Mechanizing inductive reasoning”, Proc. Eighth National Conference on Artificial Intelligence, AAAI-90, pp. 240–245, July, 1990Google Scholar
  11. 11.
    Nadathur G. and Miller D.: “An overview of λ Prolog”, In K. Bowen and R. Kowalski,ed., Fifth International Conference and Symposium on Logic Programming, MIT Press, 1988.Google Scholar
  12. 12.
    Reddy U. S., “Term Rewriting Induction”, Proc. 10th International Conference on Automated Deduction, Kaiserslautern, FRG, LNCS 449, pp. 162–177, July 1990.Google Scholar
  13. 13.
    Sakai M., Sakabe T. and Inagaki Y.: “Cover Set Induction for Verifying Algebraic Specifications”, The transactions of the institute of electronics, information and communication engineers, Vol. J75-D-I No. 3, pp. 170–179, March 1992. (in Japanese)Google Scholar
  14. 14.
    Zhang H., Kapur K. and Krishnamoorthy M. S.: “A Mechanizable Induction Principle for Equational Specification”, Proc. of 9th International Conf. on Automated Deduction at Argonne,Illinois, USA, LNCS 310, pp. 162–181, May 1988.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Su Feng
    • 1
  • Toshiki Sakabe
    • 1
  • Yasuyoshi Inagaki
    • 1
  1. 1.Department of Information Engineering, Faculty of EngineeringNagoya UniversityNagoyaJapan

Personalised recommendations