3 Search Results for "Hofbauer, Dieter"

Document
DOI: 10.4230/LIPIcs.FSCD.2026.32
New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations

Authors: René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, and Johannes Waldmann

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract
We provide new proofs of two important theorems for proving termination of term rewrite systems (TRSs), including a full formalization in Isabelle/HOL. We first consider Dershowitz' theorem that termination starting from arbitrary terms is equivalent to termination starting from terms in the right-forward closures of right-hand sides, provided that the TRS is right-linear or orthogonal. Our new proof deviates from the original one in that no reorderings of steps in infinite derivations are required, making it more precise in its argumentation. It also subsumes a later result that one can weaken orthogonality to locally confluent overlay TRSs. The second theorem is about matrix interpretations. These were introduced by Hofbauer and Waldmann for proving termination of string rewrite systems (SRSs), internally using the concept of a core. Subsequently, Endrullis, Waldmann and Zantema developed matrix interpretations for TRSs without using the idea of a core. Whereas matrix interpretations for TRSs have already been formalized several times, so far this was not the case for core SRS matrix interpretations. We not only provide such a formalization, but also extend core SRS matrix interpretations to TRSs. These new core matrix interpretations for TRSs generalize previous approaches.
Cite as

René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, and Johannes Waldmann. New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{thiemann_et_al:LIPIcs.FSCD.2026.32,
  author =	{Thiemann, Ren\'{e} and Hofbauer, Dieter and Le Huitouze, Ulysse and Waldmann, Johannes},
  title =	{{New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{32:1--32:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.32},
  URN =		{urn:nbn:de:0030-drops-263825},
  doi =		{10.4230/LIPIcs.FSCD.2026.32},
  annote =	{Keywords: Isabelle/HOL, Matrix Interpretations, Narrowing, Right-Forward Closures, Term Rewriting}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.6
Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems

Authors: Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl, and Joost-Pieter Katoen

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
We present novel semiring semantics for abstract reduction systems (ARSs). More precisely, we provide a weighted version of ARSs, where the reduction steps induce weights from a semiring. Inspired by provenance analysis in database theory and logic, we obtain a formalism that can be used for provenance analysis of arbitrary ARSs. Our semantics handle (possibly unbounded) non-determinism and possibly infinite reductions. Moreover, we develop several techniques to prove upper and lower bounds on the weights resulting from our semantics, and show that in this way one obtains a uniform approach to analyze several different properties like termination, derivational complexity, space complexity, safety, as well as combinations of these properties.
Cite as

Emma Ahrens, Jan-Christoph Kassing, Jürgen Giesl, and Joost-Pieter Katoen. Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.FSCD.2025.6,
  author =	{Ahrens, Emma and Kassing, Jan-Christoph and Giesl, J\"{u}rgen and Katoen, Joost-Pieter},
  title =	{{Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{6:1--6:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  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.FSCD.2025.6},
  URN =		{urn:nbn:de:0030-drops-236215},
  doi =		{10.4230/LIPIcs.FSCD.2025.6},
  annote =	{Keywords: Rewriting, Semirings, Semantics, Termination, Verification}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.21
Sparse Tiling Through Overlap Closures for Termination of String Rewriting

Authors: Alfons Geser, Dieter Hofbauer, and Johannes Waldmann

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
A strictly locally testable language is characterized by its set of admissible factors, prefixes and suffixes, called tiles. We over-approximate reachability sets in string rewriting by languages defined by sparse sets of tiles, containing only those that are reachable in derivations. Using the partial algebra defined by a tiling for semantic labeling, we obtain a transformational method for proving local termination. These algebras can be represented efficiently as finite automata of a certain shape. Using a known result on forward closures, and a new characterisation of overlap closures, we can automatically prove termination and relative termination, respectively. We report on experiments showing the strength of the method.
Cite as

Alfons Geser, Dieter Hofbauer, and Johannes Waldmann. Sparse Tiling Through Overlap Closures for Termination of String Rewriting. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{geser_et_al:LIPIcs.FSCD.2019.21,
  author =	{Geser, Alfons and Hofbauer, Dieter and Waldmann, Johannes},
  title =	{{Sparse Tiling Through Overlap Closures for Termination of String Rewriting}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.21},
  URN =		{urn:nbn:de:0030-drops-105282},
  doi =		{10.4230/LIPIcs.FSCD.2019.21},
  annote =	{Keywords: relative termination, semantic labeling, locally testable language, overlap closure}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 1 2019

  • Refine by Author
  • 2 Hofbauer, Dieter
  • 2 Waldmann, Johannes
  • 1 Ahrens, Emma
  • 1 Geser, Alfons
  • 1 Giesl, Jürgen
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Equational logic and rewriting
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Rewrite systems

  • Refine by Keyword
  • 1 Isabelle/HOL
  • 1 Matrix Interpretations
  • 1 Narrowing
  • 1 Rewriting
  • 1 Right-Forward Closures
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact