License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2021.19
URN: urn:nbn:de:0030-drops-142572
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14257/
Go to the corresponding LIPIcs Volume Portal

Kim, Dohan ; Lynch, Christopher

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

pdf-format:
LIPIcs-FSCD-2021-19.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{kim_et_al:LIPIcs.FSCD.2021.19,
  author =	{Kim, Dohan and Lynch, Christopher},
  title =	{{An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{19:1--19:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14257},
  URN =		{urn:nbn:de:0030-drops-142572},
  doi =		{10.4230/LIPIcs.FSCD.2021.19},
  annote =	{Keywords: Recursive Path Ordering, Permutation Equation, Permutation Group, Rewrite System, Completion, Ground Completion}
}

Keywords: Recursive Path Ordering, Permutation Equation, Permutation Group, Rewrite System, Completion, Ground Completion
Collection: 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
Issue Date: 2021
Date of publication: 06.07.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI