Document Open Access Logo

Confluence of Conditional Rewriting Modulo

Author Salvador Lucas

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2024.37.pdf
  • Filesize: 0.99 MB
  • 21 pages

Document Identifiers

Subject Classification

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

Metrics

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

Abstract

We investigate confluence of rewriting with Equational Generalized Term Rewriting Systems R, consisting of Horn clauses, some of them defining conditional equations s = t ⇐ c and rewriting rules 𝓁 → r ⇐ c. In both cases, c is a sequence of atoms, possibly defined by using additional Horn clauses. Such systems include Equational Term Rewriting Systems and (join, oriented, and semi-equational) Conditional Term Rewriting Systems. A set of equations E defines an equivalence =_E and quotient set T(F,X)/=_E of terms, where reductions s →_{R/E}t using rules in R occur. For such systems, we obtain a finite set of conditional pairs π, which can be viewed as logical sentences, to prove and disprove confluence of →_{R/E} by (dis)proving joinability of such conditional pairs π.

Cite As Get BibTex

Salvador Lucas. Confluence of Conditional Rewriting Modulo. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 37:1-37:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CSL.2024.37

Author Details

Salvador Lucas
  • DSIC & VRAIN, Universitat Politècnica de València, Spain

Funding

  • Lucas, Salvador: Supported by project PID2021-122830OB-C42 funded by MCIN/AEI/ 10.13039/501100011033 and by "ERDF A way of making Europe" and by the grant CIPROM/2022/6 funded by Generalitat Valenciana.

Acknowledgements

I thank the anonymous referees for their helpful remarks.

References

  1. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: https://doi.org/10.1017/CBO9781139172752.
  2. Franz Baader and Wayne Snyder. Unification theory. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 445-532. Elsevier and MIT Press, 2001. URL: https://doi.org/10.1016/b978-044450813-3/50010-2.
  3. Gilles Dowek. Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory. CoRR, abs/2306.00498, 2023. URL: https://doi.org/10.48550/ARXIV.2306.00498.
  4. 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.
  5. Melvin Fitting. First-Order Logic and Automated Theorem Proving, Second Edition. Graduate Texts in Computer Science. Springer, 1996. URL: https://doi.org/10.1007/978-1-4612-2360-3.
  6. Raúl Gutiérrez and Salvador Lucas. Automatic Generation of Logical Models with AGES. In Pascal Fontaine, editor, Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Proceedings, volume 11716 of Lecture Notes in Computer Science, pages 287-299. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29436-6_17.
  7. 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, 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.
  8. Raúl Gutiérrez, Miguel Vítores, and Salvador Lucas. Confluence Framework: Proving Confluence with CONFident. In Alicia Villanueva, editor, Logic-Based Program Synthesis and Transformation - 32nd International Symposium, LOPSTR 2022, Proceedings, volume 13474 of Lecture Notes in Computer Science, pages 24-43. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-16767-6_2.
  9. Gérard P. Huet. Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. J. ACM, 27(4):797-821, 1980. URL: https://doi.org/10.1145/322217.322230.
  10. Jean-Pierre Jouannaud. Confluent and coherent equational term rewriting systems: Application to proofs in abstract data types. In Giorgio Ausiello and Marco Protasi, editors, CAAP'83, Trees in Algebra and Programming, 8th Colloquium, Proceedings, volume 159 of Lecture Notes in Computer Science, pages 269-283. Springer, 1983. URL: https://doi.org/10.1007/3-540-12727-5_16.
  11. Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. SIAM J. Comput., 15(4):1155-1194, 1986. URL: https://doi.org/10.1137/0215084.
  12. Stephen Cole Kleene. Mathematical Logic. Dover Publications, 2002. Originally published by John Wiley & Sons, 1967. Google Scholar
  13. Donald E. Knuth and Peter E. Bendix. Simple Word Problems in Universal Algebra. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263-297. Pergamon Press, 1970. Google Scholar
  14. Salvador Lucas. Context-sensitive Rewriting. ACM Comput. Surv., 53(4):78:1-78:36, 2020. URL: https://doi.org/10.1145/3397677.
  15. Salvador Lucas. Local confluence of conditional and generalized term rewriting systems. Journal of Logical and Algebraic Methods in Programming, 136:paper 100926, pages 1-23, 2024. URL: https://doi.org/10.1016/j.jlamp.2023.100926.
  16. Salvador Lucas, Miguel Vítores, and Raúl Gutiérrez. Proving and disproving confluence of context-sensitive rewriting. Journal of Logical and Algebraic Methods in Programming, 126:100749, 2022. URL: https://doi.org/10.1016/j.jlamp.2022.100749.
  17. William McCune. Prover9 & Mace4. Technical report, University of New Mexico, 2005-2010. URL: http://www.cs.unm.edu/~mccune/prover9/.
  18. Elliott Mendelson. Introduction to mathematical logic (4. ed.). Chapman and Hall, 1997. Google Scholar
  19. Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002. URL: https://doi.org/10.1007/978-1-4757-3661-8.
  20. Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. J. ACM, 28(2):233-264, 1981. URL: https://doi.org/10.1145/322248.322251.
  21. 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, 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.
  22. Gordon D. Plotkin. Building-in equational theories. Machine Intelligence, 7:73-90, 1972. Google Scholar
  23. John Alan Robinson. A review of automatic theorem proving. In J.T. Schwartz, editor, Mathematical Aspects of Computer Science, volume XIX of Proceedings of Simposia in Applied Mathematics, pages 1-18, 1967. URL: https://doi.org/10.1090/psapm/019.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact