Document Open Access Logo

Ground Confluence Prover based on Rewriting Induction

Authors Takahito Aoto, Yoshihito Toyama

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.33.pdf
  • Filesize: 0.52 MB
  • 12 pages

Document Identifiers

Author Details

Takahito Aoto
Yoshihito Toyama

Cite As Get BibTex

Takahito Aoto and Yoshihito Toyama. Ground Confluence Prover based on Rewriting Induction. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 33:1-33:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSCD.2016.33

Abstract

Ground confluence of term rewriting systems guarantees that all ground
terms are confluent. Recently, interests in proving confluence of
term rewriting systems automatically has grown, and confluence provers
have been developed. But they mainly focus on confluence and not
ground confluence. In fact, little interest has been paid to
developing tools for proving ground confluence automatically. We
report an implementation of a ground confluence prover based on
rewriting induction, which is a method originally developed for
proving inductive theorems.

Subject Classification

Keywords
  • Ground Confluence
  • Rewriting Induction
  • Non-Orientable Equations
  • Term Rewriting Systems

Metrics

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

References

  1. T. Aoto. Dealing with non-orientable equations in rewriting induction. In Proc. of 17th RTA, volume 4098 of LNCS, pages 242-256. Springer-Verlag, 2006. Google Scholar
  2. T. Aoto. Designing a rewriting induction prover with an increased capability of non-orientable equations. In Proc. of 1st SCSS, RISC Technical Report, pages 1-15, 2008. Google Scholar
  3. T. Aoto. Sound lemma generation for proving inductive validity of equations. In Proc. of 28th FSTTCS, volume 2 of LIPIcs, pages 13-24. Schloss Dagstuhl, 2008. Google Scholar
  4. T. Aoto and S. Stratulat. Decision procedures for proving inductive theorems without induction. In Proc. of 16th PPDP, pages 237-248. ACM Press, 2014. Google Scholar
  5. T. Aoto and Y. Toyama. Persistency of confluence. Journal of Universal Computer Science, 3(11):1134-1147, 1997. Google Scholar
  6. 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
  7. 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
  8. 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
  9. A. Bouhoula and F. Jacquemard. Verifying regular trace properties of secuirty protocols with explicit destructors and implicit induction. In Proc. of FCS-ARSPA, pages 27-44, 2007. Google Scholar
  10. A. Bouhoula, E. Kounalis, and M. Rusinowitch. Automated mathematical induction. Journal of Logic and Computation, 5(5):631-668, 1995. Google Scholar
  11. Y. Chiba, T. Aoto, and Y. Toyama. Program transformation by templates based on term rewriting. In Proc. of 7th PPDP, pages 59-69. ACM Press, 2005. Google Scholar
  12. M. Codish, V. Lagoon, and P. J. Stuckey. Solving partial order constraints for LPO termination. In Proc. of 17th RTA, volume 4098 of LNCS, pages 4-18. Springer-Verlag, 2006. Google Scholar
  13. N. Dershowitz and U. S. Reddy. Deductive and inductive synthesis of equational programs. Journal of Symbolic Computation, 15:467-494, 1993. Google Scholar
  14. L. Fribourg. A strong restriction of the inductive completion procedure. Journal of Symbolic Computation, 8:253-276, 1989. Google Scholar
  15. H. Ganzinger. Ground term confluence in parametric conditional equational specifications. In Proc. of 4th STACS, volume 247 of LNCS, pages 286-298, 1987. Google Scholar
  16. R. Göbel. Ground confluence. In Proc. of 2nd RTA, volume 256 of LNCS, pages 156-167, 1987. Google Scholar
  17. N. Hirokawa and D. Klein. Saigawa: A confluence tool. In Proc. of 1st IWC, page 49, 2012. Google Scholar
  18. D. Kapur, P. Narendran, and F. Otto. On ground-confluence of term rewriting systems. Information and Computation, 86:14-31, 1990. Google Scholar
  19. 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
  20. D. Kapur, P. Narendran, and H. Zhang. Automating inductionless induction using test sets. Journal of Symbolic Computation, 11(1-2):81-111, 1991. Google Scholar
  21. K. Sato, K. Kikuchi, T. Aoto, and Y. Toyama. Correctness of context-moving transformations for term rewriting systems. In Proc. of 25th LOPSTR, volume 9527 of LNCS, pages 331-345. Springer-Verlag, 2015. Google Scholar
  22. 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
  23. T. Sternagel and A. Middeldorp. Conditional confluence (system description). In Proc. of Joint 25th RTA and 12th TLCA, pages 456-465. Springer-Verlag, 2014. Google Scholar
  24. Terese. Term Rewriting Systems. Cambridge University Press, 2003. Google Scholar
  25. T. Walsh. A divergence critic for inductive proof. Journal of Artificial Intelligence Research, 4:209-235, 1996. Google Scholar
  26. F. Winkler and B. Buchberger. A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. In Proc. of the Colloq. on Algebra, Combinatorics and Logic in Computer Science, Vol. II, pages 849-869. Springer-Verlag, 1985. Google Scholar
  27. H. Zankl, B. Felgenhauer, and A. Middeldorp. CSI - A confluence tool. In Proc. of 23rd CADE, volume 6803 of LNAI, pages 499-505. Springer-Verlag, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact