Document Open Access Logo

Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion

Authors Christian Sternagel, Thomas Sternagel

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.29.pdf
  • Filesize: 0.61 MB
  • 16 pages

Document Identifiers

Author Details

Christian Sternagel
Thomas Sternagel

Cite As Get BibTex

Christian Sternagel and Thomas Sternagel. Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSCD.2016.29

Abstract

Suzuki et al. showed that properly oriented, right-stable, orthogonal, and oriented conditional term rewrite systems with extra variables in right-hand sides are confluent. We present our Isabelle/HOL formalization of this result, including two generalizations. On the one hand, we relax proper orientedness and orthogonality to extended proper orientedness and almost orthogonality modulo infeasibility, as suggested by Suzuki et al. On the other hand, we further loosen the requirements of the latter, enabling more powerful methods for proving infeasibility of conditional critical pairs. Furthermore, we formalized a construction by Jacquemard that employs exact tree automata completion for non-reachability analysis and apply it to certify infeasibility of conditional critical pairs. Combining these two results and extending the conditional confluence checker ConCon accordingly, we are able to automatically prove and certify confluence of an important class of conditional term rewrite systems.

Subject Classification

Keywords
  • certification
  • conditional term rewriting
  • confluence
  • infeasible critical pairs
  • non-reachability

Metrics

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

References

  1. Jürgen Avenhaus and Carlos Loría-Sáenz. On conditional rewrite systems with extra variables and deterministic logic programs. In Proceedings of the 5th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, volume 822 of Lecture Notes in Computer Science, pages 215-229. Springer, 1994. \doi10.1007/3-540-58216-9_40. Google Scholar
  2. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  3. Bertram Felgenhauer and René Thiemann. Reachability analysis with state-compatible automata. In Proceedings of the 8th International Conference on Language and Automata Theory and Applications, volume 8370 of Lecture Notes in Computer Science, pages 347-359. Springer, 2014. \doi10.1007/978-3-319-04921-2_28. Google Scholar
  4. Thomas Genet. Decidable approximations of sets of descendants and sets of normal forms. In Proceedings of the 9th International Conference on Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, pages 151-165. Springer, 1998. \doi10.1007/BFb0052368. Google Scholar
  5. Thomas Genet and Valerié Viet Triem Tong. Reachability analysis of term rewriting systems with timbuk. In Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, volume 2250 of Lecture Notes in Computer Science, pages 695-706. Springer, 2001. \doi10.1007/3-540-45653-8_48. Google Scholar
  6. Jürgen Giesl, René Thiemann, and Peter Schneider-Kamp. Proving and disproving termination of higher-order functions. In Proceedings of the 5th International Workshop on Frontiers of Combining Systems, volume 3717 of Lecture Notes in Computer Science, pages 216-231. Springer, 2005. \doi10.1007/11559306_12. Google Scholar
  7. Michael Hanus. On extra variables in (equational) logic programming. In Proceedings of the 12th International Conference on Logic Programming, pages 665-679. MIT Press, 1995. Google Scholar
  8. Florent Jacquemard. Decidable approximations of term rewriting systems. In Proceedings of the 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 362-376. Springer, 1996. \doi10.1007/3-540-61464-8_65. Google Scholar
  9. Tobias Nipkow, Lawrence Charles Paulson, and Makarius Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. \doi10.1007/3-540-45949-9. Google Scholar
  10. Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002. Google Scholar
  11. Christian Sternagel and Aart Middeldorp. Root-labeling. In Proceedings of the 19th International Conference on Rewriting Techniques and Applications, volume 5117 of Lecture Notes in Computer Science, pages 336-350. Springer, 2008. \doi10.1007/978-3-540-70590-1_23. Google Scholar
  12. Christian Sternagel and Thomas Sternagel. Level-confluence of 3-CTRSs in Isabelle/HOL. In Tiwari and Aoto [18]. URL: http://www.csl.sri.com/users/tiwari/iwc2015/iwc2015.pdf.
  13. Christian Sternagel and René Thiemann. Signature extensions preserve termination - an alternative proof via dependency pairs. In Proceedings of the 19h EACSL Annual Conference on Computer Science Logic, volume 6247 of Lecture Notes in Computer Science, pages 514-528. Springer, 2010. \doi10.1007/978-3-642-15205-4_39. Google Scholar
  14. Christian Sternagel and René Thiemann. The Certification Problem Format. In Proceedings of the 11th Workshop on User Interfaces for Theorem Provers, pages 61-72, 2014. \doi10.4204/EPTCS.167.8. Google Scholar
  15. Thomas Sternagel and Aart Middeldorp. Conditional confluence (system description). In Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications, volume 8560 of Lecture Notes in Computer Science, pages 456-465. Springer, 2014. \doi10.1007/978-3-319-08918-8_31. Google Scholar
  16. Taro Suzuki, Aart Middeldorp, and Tetsuo Ida. Level-confluence of conditional rewrite systems with extra variables in right-hand sides. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science, pages 179-193. Springer, 1995. \doi10.1007/3-540-59200-8_56. Google Scholar
  17. René Thiemann and Christian Sternagel. Certification of termination proofs using Cęrn-0.2exeęrn-0.5exTęrn-0.5exA. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pages 452-468. Springer, 2009. \doi10.1007/978-3-642-03359-9_31. Google Scholar
  18. Ashish Tiwari and Takahito Aoto, editors. Proceedings of the 4th International Workshop on Confluence, 2015. URL: http://www.csl.sri.com/users/tiwari/iwc2015/iwc2015.pdf.
  19. Makarius Wenzel. System description: Isabelle/jEdit in 2014. In Proceedings of the 11th Workshop on User Interfaces for Theorem Provers, pages 84-94, 2014. \doi10.4204/EPTCS.167.10. Google Scholar
  20. Sarah Winkler and René Thiemann. Formalizing soundness and completeness of unravelings. In Proceedings of the 10th International Workshop on Frontiers of Combining Systems, volume 9322 of Lecture Notes in Computer Science, pages 239-255. Springer, 2015. \doi10.1007/978-3-319-24246-0_15. 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