Improving Rewriting Induction Approach for Proving Ground Confluence

Authors Takahito Aoto, Yoshihito Toyama, Yuta Kimura

Thumbnail PDF


  • Filesize: 1.01 MB
  • 18 pages

Document Identifiers

Author Details

Takahito Aoto
Yoshihito Toyama
Yuta Kimura

Cite AsGet BibTex

Takahito Aoto, Yoshihito Toyama, and Yuta Kimura. Improving Rewriting Induction Approach for Proving Ground Confluence. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


In (Aoto&Toyama, FSCD 2016), a method to prove ground confluence of many-sorted term rewriting systems based on rewriting induction is given. In this paper, we give several methods that add wider flexibility to the rewriting induction approach for proving ground confluence. Firstly, we give a method to deal with the case in which suitable rules are not presented in the input system. Our idea is to construct additional rewrite rules that supplement or replace existing rules in order to obtain a set of rules that is adequate for applying rewriting induction. Secondly, we give a method to deal with non-orientable constructor rules. This is accomplished by extending the inference system of rewriting induction and giving a sufficient criterion for the correctness of the system. Thirdly, we give a method to deal with disproving ground confluence. The presented methods are implemented in our ground confluence prover AGCP and experiments are reported. Our experiments reveal the presented methods are effective to deal with problems for which state-of-the-art ground confluence provers can not handle.
  • Ground Confluence
  • Rewriting Induction
  • Non-Orientable Equations
  • Term Rewriting Systems


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. T. Aoto. Disproving confluence of term rewriting systems by interpretation and ordering. In Proc. of 9th FroCoS, volume 8152 of LNAI, pages 311-326. Springer-Verlag, 2013. Google Scholar
  2. T. Aoto and Y. Toyama. Ground confluence prover based on rewriting induction. In Proc. of 1st FSCD, volume 52 of LIPIcs, pages 33:1-12. Schloss Dagstuhl, 2016. URL:
  3. T. Aoto, Y. Yoshida, and Y. Toyama. Proving confluence of term rewriting systems automatically. In Proc. of 20th RTA, volume 5595 of LNCS, pages 93-102. Springer-Verlag, 2009. Google Scholar
  4. K. Becker. Proving ground confluence and inductive validity in constructor based equational specifications. In Proc. of 4th TAPSOFT, volume 668 of LNCS, pages 46-60. Springer-Verlag, 1993. Google Scholar
  5. A. Bouhoula. Simultaneous checking of completeness and ground conflunce for algebraic specifications. ACM Transactions on Computational Logic, 10(2):20:1-33, 2009. Google Scholar
  6. A. Bouhoula, E. Kounalis, and M. Rusinowitch. Automated mathematical induction. Journal of Logic and Computation, 5(5):631-668, 1995. Google Scholar
  7. N. Dershowitz and U. S. Reddy. Deductive and inductive synthesis of equational programs. Journal of Symbolic Computation, 15:467-494, 1993. Google Scholar
  8. H. Ganzinger. Ground term confluence in parametric conditional equational specifications. In Proc. of 4th STACS, volume 247 of LNCS, pages 286-298. Springer-Verlag, 1987. Google Scholar
  9. R. Göbel. Ground confluence. In Proc. of 2nd RTA, volume 256 of LNCS, pages 156-167. Springer-Verlag, 1987. Google Scholar
  10. D. Kapur, P. Narendran, and H. Zhang. On sufficient-completeness and related properties of term rewriting systems. Acta Informatica, 24(4):395-415, 1987. Google Scholar
  11. A. Lazrek, P. Lescanne, and J. J. Thiel. Tools for proving inductive equalities, relative completeness, and ω-completeness. Information and Computation, 84:47-70, 1990. Google Scholar
  12. F. Rapp and A. Middeldorp. Automating the first-order theory of rewriting for left-linear right-ground rewrite systems. In Proc. of 1st FSCD, volume 52 of LIPIcs, pages 36:1–-12. Schloss Dagstuhl, 2016. Google Scholar
  13. U. S. Reddy. Term rewriting induction. In Proc. of CADE-10, volume 449 of LNAI, pages 162-177. Springer-Verlag, 1990. Google Scholar
  14. S. Shimazu, T. Aoto, and Y. Toyama. Automated lemma generation for rewriting induction with disproof. JSSST Computer Software, 26(2):41-55, 2009. In Japanese. Google Scholar
  15. Terese. Term Rewriting Systems. Cambridge University Press, 2003. Google Scholar
  16. V. van Oostrom. Confluence by decreasing diagrams. Theoretical Computer Science, 126(2):259-280, 1994. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail