Search Results

Documents authored by Felgenhauer, Bertram

Document
DOI: 10.4230/LIPIcs.RTA.2015.257
Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules

Authors: Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
We describe how to utilize redundant rewrite rules, i.e., rules that can be simulated by other rules, when (dis)proving confluence of term rewrite systems. We demonstrate how automatic confluence provers benefit from the addition as well as the removal of redundant rules. Due to their simplicity, our transformations were easy to formalize in a proof assistant and are thus amenable to certification. Experimental results show the surprising gain in power.
Cite as

Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp. Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 257-268, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{nagele_et_al:LIPIcs.RTA.2015.257,
  author =	{Nagele, Julian and Felgenhauer, Bertram and Middeldorp, Aart},
  title =	{{Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{257--268},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.257},
  URN =		{urn:nbn:de:0030-drops-52010},
  doi =		{10.4230/LIPIcs.RTA.2015.257},
  annote =	{Keywords: term rewriting, confluence, automation, transformation}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.174
Proof Orders for Decreasing Diagrams

Authors: Bertram Felgenhauer and Vincent van Oostrom

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
We present and compare some well-founded proof orders for decreasing diagrams. These proof orders order a conversion above another conversion if the latter is obtained by filling any peak in the former by a (locally) decreasing diagram. Therefore each such proof order entails the decreasing diagrams technique for proving confluence. The proof orders differ with respect to monotonicity and complexity. Our results are developed in the setting of involutive monoids. We extend these results to obtain a decreasing diagrams technique for confluence modulo.
Cite as

Bertram Felgenhauer and Vincent van Oostrom. Proof Orders for Decreasing Diagrams. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 174-189, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{felgenhauer_et_al:LIPIcs.RTA.2013.174,
  author =	{Felgenhauer, Bertram and van Oostrom, Vincent},
  title =	{{Proof Orders for Decreasing Diagrams}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{174--189},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.174},
  URN =		{urn:nbn:de:0030-drops-40616},
  doi =		{10.4230/LIPIcs.RTA.2013.174},
  annote =	{Keywords: involutive monoid, confluence modulo, decreasing diagram, proof order}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.165
Deciding Confluence of Ground Term Rewrite Systems in Cubic Time

Authors: Bertram Felgenhauer

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
It is well known that the confluence property of ground term rewrite systems (ground TRSs) is decidable in polynomial time. For an efficient implementation, the degree of this polynomial is of great interest. The best complexity bound in the literature is given by Comon, Godoy and Nieuwenhuis (2001), who describe an O(n^5) algorithm, where n is the size of the ground TRS. In this paper we improve this bound to O(n^3). The algorithm has been implemented in the confluence tool CSI.
Cite as

Bertram Felgenhauer. Deciding Confluence of Ground Term Rewrite Systems in Cubic Time. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 165-175, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{felgenhauer:LIPIcs.RTA.2012.165,
  author =	{Felgenhauer, Bertram},
  title =	{{Deciding Confluence of Ground Term Rewrite Systems in Cubic Time}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{165--175},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.165},
  URN =		{urn:nbn:de:0030-drops-34918},
  doi =		{10.4230/LIPIcs.RTA.2012.165},
  annote =	{Keywords: confluence, ground rewrite systems, decidability, polynomial time}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.288
Layer Systems for Proving Confluence

Authors: Bertram Felgenhauer, Harald Zankl, and Aart Middeldorp

Published in: LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)

Abstract
We introduce layer systems for proving generalizations of the modularity of confluence for first-order rewrite systems. Layer systems specify how terms can be divided into layers. We establish structural conditions on those systems that imply confluence. Our abstract framework covers known results like many-sorted persistence, layer-preservation and currying. We present a counterexample to an extension of the former to order-sorted rewriting and derive new sufficient conditions for the extension to hold.
Cite as

Bertram Felgenhauer, Harald Zankl, and Aart Middeldorp. Layer Systems for Proving Confluence. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 288-299, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{felgenhauer_et_al:LIPIcs.FSTTCS.2011.288,
  author =	{Felgenhauer, Bertram and Zankl, Harald and Middeldorp, Aart},
  title =	{{Layer Systems for Proving Confluence}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{288--299},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.288},
  URN =		{urn:nbn:de:0030-drops-33265},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.288},
  annote =	{Keywords: Term rewriting, Confluence, Modularity, Persistence}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.377
Labelings for Decreasing Diagrams

Authors: Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
This paper is concerned with automating the decreasing diagrams technique of van Oostrom for establishing confluence of term rewrite systems. We study abstract criteria that allow to lexicographically combine labelings to show local diagrams decreasing. This approach has two immediate benefits. First, it allows to use labelings for linear rewrite systems also for left-linear ones, provided some mild conditions are satisfied. Second, it admits an incremental method for proving confluence which subsumes recent developments in automating decreasing diagrams. The techniques proposed in the paper have been implemented and experimental results demonstrate how, e.g., the rule labeling benefits from our contributions.
Cite as

Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp. Labelings for Decreasing Diagrams. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 377-392, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{zankl_et_al:LIPIcs.RTA.2011.377,
  author =	{Zankl, Harald and Felgenhauer, Bertram and Middeldorp, Aart},
  title =	{{Labelings for Decreasing Diagrams}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{377--392},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.377},
  URN =		{urn:nbn:de:0030-drops-31378},
  doi =		{10.4230/LIPIcs.RTA.2011.377},
  annote =	{Keywords: term rewriting, confluence, decreasing diagrams, labeling}
}
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