Document Open Access Logo

An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems

Authors Dohan Kim, Christopher Lynch

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.19.pdf
  • Filesize: 0.63 MB
  • 17 pages

Document Identifiers

Author Details

Dohan Kim
  • Clarkson University, Potsdam, NY, USA
Christopher Lynch
  • Clarkson University, Potsdam, NY, USA

Cite AsGet BibTex

Dohan Kim and Christopher Lynch. An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 19:1-19:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.19

Abstract

Rewriting modulo equations has been researched for several decades but due to the lack of suitable orderings, there are some limitations to rewriting modulo permutation equations. Given a finite set of permutation equations E, we present a new RPO-based ordering modulo E using (permutation) group actions and their associated orbits. It is an E-compatible reduction ordering on terms with the subterm property and is E-total on ground terms. We also present a completion and ground completion method for rewriting modulo a finite set of permutation equations E using our ordering modulo E. We show that our ground completion modulo E always admits a finite ground convergent (modulo E) rewrite system, which allows us to obtain the decidability of the word problem of ground theories modulo E.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Recursive Path Ordering
  • Permutation Equation
  • Permutation Group
  • Rewrite System
  • Completion
  • Ground Completion

Metrics

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

References

  1. Jürgen Avenhaus. Efficient Algorithms for Computing Modulo Permutation Theories. In David Basin and Michaël Rusinowitch, editors, Automated Reasoning - IJCAR 2004, Cork, Ireland, July 4-8, pages 415-429, Berlin, Heidelberg, 2004. Springer. Google Scholar
  2. Jürgen Avenhaus and David A. Plaisted. General algorithms for permutations in equational inference. Journal of Automated Reasoning, 26(3):223-268, 2001. Google Scholar
  3. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, Cambridge, UK, 1998. Google Scholar
  4. Franz Baader and Wayne Snyder. Unification Theory. In Handbook of Automated Reasoning, Volume I, chapter 8, pages 445-532. Elsevier, Amsterdam, 2001. Google Scholar
  5. Leo Bachmair. Canonical Equational Proofs. Birkhäuser, Boston, 1991. Google Scholar
  6. Leo Bachmair and Nachum Dershowitz. Completion for rewriting modulo a congruence. Theoretical Computer Science, 67(2):173-201, 1989. Google Scholar
  7. Leo Bachmair, Ashish Tiwari, and Laurent Vigneron. Abstract congruence closure. Journal of Automated Reasoning, 31(2):129-168, 2003. Google Scholar
  8. Frédéric Blanqui. Rewriting Modulo in Deduction Modulo. In Robert Nieuwenhuis, editor, Rewriting Techniques and Applications, pages 395-409, Berlin, Heidelberg, 2003. Springer. Google Scholar
  9. Frédéric Blanqui. Termination of rewrite relations on λ-terms based on Girard’s notion of reducibility. Theoretical Computer Science, 611:50-86, 2016. Google Scholar
  10. Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279-301, 1982. Google Scholar
  11. Nachum Dershowitz and David A. Plaisted. Rewriting. In Handbook of Automated Reasoning, Volume I, chapter 9, pages 535-610. Elsevier, Amsterdam, 2001. Google Scholar
  12. GAP Group. Groups, Algorithms, Programming, Version 4.8, 2016. http://www.gap-system.org. Google Scholar
  13. Sumanta Ghosh and Piyush P. Kurur. Permutation Groups and the Graph Isomorphism Problem, pages 183-202. Springer, Cham, 2014. Google Scholar
  14. Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler. Abstract Completion, Formalized. Logical Methods in Computer Science, 15:19:1–19:42, 2019. Google Scholar
  15. Thomas W. Hungerford. Algebra. Springer, New York, NY, 1980. Google Scholar
  16. Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4):1155-1194, 1986. Google Scholar
  17. Deepak Kapur, Paliath Narendran, and G. Sivakumar. A path ordering for proving termination of term rewriting systems. In Hartmut Ehrig, Christiane Floyd, Maurice Nivat, and James Thatcher, editors, Mathematical Foundations of Software Development, pages 173-187, Berlin, Heidelberg, 1985. Springer Berlin Heidelberg. Google Scholar
  18. Deepak Kapur and G. Sivakumar. Proving Associative-Commutative Termination Using RPO-Compatible Orderings. In R. Caferra and Gernot Salzer, editors, Automated Deduction in Classical and Non-Classical Logics, pages 39-61, Berlin, Heidelberg, 2000. Springer. Google Scholar
  19. Dohan Kim and Christopher Lynch. Equational Theorem Proving Modulo. In Automated Deduction - CADE 28: The 28th International Conference on Automated Deduction, Carnegie Mellon University, Pittsburgh, PA (Virtual Conference), July 11-16, to appear. Springer, 2021. Google Scholar
  20. Claude Kirchner and Helene Kirchner. Rewriting, Solving, Proving, 1999. Preliminary version of a book: URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.144.5349.
  21. Donald. E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In Jörg H. Siekmann and Graham Wrightson, editors, Automation of Reasoning: 2: Classical Papers on Computational Logic 1967-1970, pages 342-376. Springer, Berlin, Heidelberg, 1983. Google Scholar
  22. Claude Marché. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253-288, 1996. Google Scholar
  23. Paliath Narendran and Michaël Rusinowitch. Any ground associative-commutative theory has a finite canonical system. In R. V. Book, editor, Rewriting Techniques and Applications, pages 423-434, Berlin, Heidelberg, 1991. Springer. Google Scholar
  24. Robert Nieuwenhuis and Albert Rubio. Paramodulation-based theorem proving. In Handbook of Automated Reasoning, Volume I, chapter 7, pages 371-443. Elsevier, Amsterdam, 2001. Google Scholar
  25. Gerald E Peterson and Mark E Stickel. Complete sets of reductions for some equational theories. Journal of the ACM (JACM), 28(2):233-264, 1981. Google Scholar
  26. Albert Rubio. Theorem Proving modulo Associativity. In H. Kleine Büning, editor, Computer Science Logic, pages 452-467, Berlin, Heidelberg, 1996. Springer. Google Scholar
  27. Albert Rubio. A Fully Syntactic AC-RPO. Inf. Comput., 178(2):515-533, 2002. Google Scholar
  28. Albert Rubio and Robert Nieuwenhuis. A total AC-compatible ordering based on RPO. Theoretical Computer Science, 142(2):209-227, 1995. Google Scholar
  29. Charles C Sims. Computation with finitely presented groups, volume Vol. 48. Cambridge University Press, Cambridge, UK, 1994. Google Scholar
  30. Wayne Snyder. On the complexity of recursive path orderings. Information Processing Letters, 46(5):257-262, 1993. Google Scholar
  31. Joachim Steinbach. On the complexity of simplification orderings. Technical Report Technical Report SR-93-18 (SFB), SEKI University of Kaiserslautern, 1993. Google Scholar
  32. Christian Sternagel and Akihisa Yamada. Reachability analysis for termination and confluence of rewriting. In Tools and Algorithms for the Construction and Analysis of Systems, pages 262-278, Cham, 2019. Springer International Publishing. 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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact