Document Open Access Logo

Confluence of Conditional Rewriting in Logic Form

Authors Raúl Gutiérrez , Salvador Lucas , Miguel Vítores

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2021.44.pdf
  • Filesize: 0.88 MB
  • 18 pages

Document Identifiers

Author Details

Raúl Gutiérrez
  • Universidad Politécnica de Madrid, Spain
Salvador Lucas
  • DSIC & VRAIN, Universitat Politècnica de València, Spain
Miguel Vítores
  • VRAIN, Universitat Politècnica de València, Spain

Funding

Partially supported by grant RTI2018-094403-B-C32 funded by MCIN/AEI/10.13039/501100011033 and by "ERDF A way of making Europe", and PROMETEO/2019/098.

Cite AsGet BibTex

Raúl Gutiérrez, Salvador Lucas, and Miguel Vítores. Confluence of Conditional Rewriting in Logic Form. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 44:1-44:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSTTCS.2021.44

Abstract

We characterize conditional rewriting as satisfiability in a Herbrand-like model of terms where variables are also included as fresh constant symbols extending the original signature. Confluence of conditional rewriting and joinability of conditional critical pairs is characterized similarly. Joinability of critical pairs is then translated into combinations of (in)feasibility problems which can be efficiently handled by a number of automatic tools. This permits a more efficient use of standard results for proving confluence of conditional term rewriting systems, most of them relying on auxiliary proofs of joinability of conditional critical pairs, perhaps with additional syntactical and (operational) termination requirements on the system. Our approach has been implemented in a new system: CONFident . Its ability to (dis)prove confluence of conditional term rewriting systems is witnessed by means of some benchmarks comparing our tool with existing tools for similar purposes.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Logic and verification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Confluence
  • Program analysis
  • Rewriting-based systems

Metrics

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

Supplementary Materials

References

  1. Takahito Aoto, Junichi Yoshida, and Yoshihito Toyama. Proving confluence of term rewriting systems automatically. In Ralf Treinen, editor, Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009, Proceedings, volume 5595 of Lecture Notes in Computer Science, pages 93-102. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02348-4_7.
  2. Jürgen Avenhaus and Carlos Loría-Sáenz. On conditional rewrite systems with extra variables and deterministic logic programs. In Frank Pfenning, editor, Logic Programming and Automated Reasoning, 5th International Conference, LPAR'94, Kiev, Ukraine, July 16-22, 1994, Proceedings, volume 822 of Lecture Notes in Computer Science, pages 215-229. Springer, 1994. URL: https://doi.org/10.1007/3-540-58216-9_40.
  3. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. Google Scholar
  4. Jan A. Bergstra and Jan Willem Klop. Conditional rewrite rules: Confluence and termination. J. Comput. Syst. Sci., 32(3):323-362, 1986. URL: https://doi.org/10.1016/0022-0000(86)90033-4.
  5. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71999-1.
  6. Max Dauchet and Sophie Tison. The theory of ground rewrite systems is decidable. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), Philadelphia, Pennsylvania, USA, June 4-7, 1990, pages 242-248. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/LICS.1990.113750.
  7. Nachum Dershowitz, Mitsuhiro Okada, and G. Sivakumar. Confluence of conditional rewrite systems. In Stéphane Kaplan and Jean-Pierre Jouannaud, editors, Conditional Term Rewriting Systems, 1st International Workshop, Orsay, France, July 8-10, 1987, Proceedings, volume 308 of Lecture Notes in Computer Science, pages 31-44. Springer, 1987. URL: https://doi.org/10.1007/3-540-19242-5_3.
  8. Francisco Durán and José Meseguer. On the church-rosser and coherence properties of conditional order-sorted rewrite theories. J. Log. Algebraic Methods Program., 81(7-8):816-850, 2012. URL: https://doi.org/10.1016/j.jlap.2011.12.004.
  9. Joseph A. Goguen and José Meseguer. Models and equality for logical programming. In Hartmut Ehrig, Robert A. Kowalski, Giorgio Levi, and Ugo Montanari, editors, TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, March 23-27, 1987, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Functional and Logic Programming and Specifications (CFLP), volume 250 of Lecture Notes in Computer Science, pages 1-22. Springer, 1987. URL: https://doi.org/10.1007/BFb0014969.
  10. Bernhard Gramlich and Claus-Peter Wirth. Confluence of terminating conditional rewrite systems revisited. In Harald Ganzinger, editor, Rewriting Techniques and Applications, 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, Proceedings, volume 1103 of Lecture Notes in Computer Science, pages 245-259. Springer, 1996. URL: https://doi.org/10.1007/3-540-61464-8_56.
  11. Raúl Gutiérrez and Salvador Lucas. Automatically proving and disproving feasibility conditions. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science, pages 416-435. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_27.
  12. Raúl Gutiérrez and Salvador Lucas. mu-term : Verify termination properties automatically (system description). In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science, pages 436-447. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_28.
  13. Nao Hirokawa, Julian Nagele, and Aart Middeldorp. Cops and CoCoWeb: Infrastructure for Confluence Tools. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, volume 10900 of Lecture Notes in Computer Science, pages 346-353. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94205-6_23.
  14. Salvador Lucas. Proving semantic properties as first-order satisfiability. Artif. Intell., 277, 2019. URL: https://doi.org/10.1016/j.artint.2019.103174.
  15. Salvador Lucas. Applications and extensions of context-sensitive rewriting. Journal of Logical and Algebraic Methods in Programming, 121:100680, 2021. URL: https://doi.org/10.1016/j.jlamp.2021.100680.
  16. Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Inf. Process. Lett., 95(4):446-453, 2005. URL: https://doi.org/10.1016/j.ipl.2005.05.002.
  17. Salvador Lucas and José Meseguer. Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebr. Meth. Program., 86(1):236-268, 2017. URL: https://doi.org/10.1016/j.jlamp.2016.03.003.
  18. Salvador Lucas, José Meseguer, and Raúl Gutiérrez. The 2D Dependency Pair Framework for conditional rewrite systems. Part I: Definition and basic processors. J. Comput. Syst. Sci., 96:74-106, 2018. URL: https://doi.org/10.1016/j.jcss.2018.04.002.
  19. William McCune. Prover9 & Mace4. Technical report, University of New Mexico, 2005-2010. URL: http://www.cs.unm.edu/~mccune/prover9/.
  20. Elliott Mendelson. Introduction to mathematical logic (4. ed.). Chapman and Hall, 1997. Google Scholar
  21. A. Middeldorp, J. Nagele, and K. Shintani. CoCo 2019: report on the eight confluence competition. J.International Journal on Software Tools for Technology Transfer, to appear, 2021. URL: https://doi.org/10.1007/s10009-021-00620-4.
  22. Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner. On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation. In 3rd International Workshop on Confluence, IWC 2014, July 13, 2014, Vienna, Austria, page 42, 2014. Google Scholar
  23. Enno Ohlebusch. Advanced topics in term rewriting. Springer, 2002. Google Scholar
  24. David A. Plaisted. A logic for conditional term rewriting systems. In Stéphane Kaplan and Jean-Pierre Jouannaud, editors, Conditional Term Rewriting Systems, 1st International Workshop, Orsay, France, July 8-10, 1987, Proceedings, volume 308 of Lecture Notes in Computer Science, pages 212-227. Springer, 1987. URL: https://doi.org/10.1007/3-540-19242-5_16.
  25. Franziska Rapp and Aart Middeldorp. Automating the first-order theory of rewriting for left-linear right-ground rewrite systems. In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal, volume 52 of LIPIcs, pages 36:1-36:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.36.
  26. Taro Suzuki, Aart Middeldorp, and Tetsuo Ida. Level-confluence of conditional rewrite systems with extra variables in right-hand sides. In Jieh Hsiang, editor, Rewriting Techniques and Applications, 6th International Conference, RTA-95, Kaiserslautern, Germany, April 5-7, 1995, Proceedings, volume 914 of Lecture Notes in Computer Science, pages 179-193. Springer, 1995. URL: https://doi.org/10.1007/3-540-59200-8_56.
  27. Ralf Treinen. The first-order theory of linear one-step rewriting is undecidable. Theor. Comput. Sci., 208(1-2):179-190, 1998. URL: https://doi.org/10.1016/S0304-3975(98)00083-8.
  28. Miguel Vítores. CONFident: a tool for confluence analysis of rewriting systems. PhD thesis, Departamento de Sistemas Informáticos y Computación. Universitat Politècnica de València, December 2021. 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 Imprint Privacy Contact