21 Search Results for "Middeldorp, Aart"

Document
DOI: 10.4230/LIPIcs.ITP.2024.8
The Directed Van Kampen Theorem in Lean

Authors: Henning Basold, Peter Bruin, and Dominique Lawson

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Directed topology augments the concept of a topological space with a notion of directed paths. This leads to a category of directed spaces, in which the morphisms are continuous maps respecting directed paths. Directed topology thereby enables an accurate representation of computation paths in concurrent systems that usually cannot be reversed. Even though ideas from algebraic topology have analogues in directed topology, the directedness drastically changes how spaces can be characterised. For instance, while an important homotopy invariant of a topological space is its fundamental groupoid, for directed spaces this has to be replaced by the fundamental category because directed paths are not necessarily reversible. In this paper, we present a Lean 4 formalisation of directed spaces and of a Van Kampen theorem for them, which allows the fundamental category of a directed space to be computed in terms of the fundamental categories of subspaces. Part of this formalisation is also a significant theory of directed spaces, directed homotopy theory and path coverings, which can serve as basis for future formalisations of directed topology. The formalisation in Lean can also be used in computer-assisted reasoning about the behaviour of concurrent systems that have been represented as directed spaces.
Cite as

Henning Basold, Peter Bruin, and Dominique Lawson. The Directed Van Kampen Theorem in Lean. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{basold_et_al:LIPIcs.ITP.2024.8,
  author =	{Basold, Henning and Bruin, Peter and Lawson, Dominique},
  title =	{{The Directed Van Kampen Theorem in Lean}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.8},
  URN =		{urn:nbn:de:0030-drops-207368},
  doi =		{10.4230/LIPIcs.ITP.2024.8},
  annote =	{Keywords: Lean, Directed Topology, Van Kampen Theorem, Directed Homotopy Theory, Formalised Mathematics}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.35
Formal Verification of the Empty Hexagon Number

Authors: Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
A recent breakthrough in computer-assisted mathematics showed that every set of 30 points in the plane in general position (i.e., no three points on a common line) contains an empty convex hexagon. Heule and Scheucher solved this problem with a combination of geometric insights and automated reasoning techniques by constructing CNF formulas ϕ_n, with O(n⁴) clauses, such that if ϕ_n is unsatisfiable then every set of n points in general position must contain an empty convex hexagon. An unsatisfiability proof for n = 30 was then found with a SAT solver using 17 300 CPU hours of parallel computation. In this paper, we formalize and verify this result in the Lean theorem prover. Our formalization covers ideas in discrete computational geometry and SAT encoding techniques by introducing a framework that connects geometric objects to propositional assignments. We see this as a key step towards the formal verification of other SAT-based results in geometry, since the abstractions we use have been successfully applied to similar problems. Overall, we hope that our work sets a new standard for the verification of geometry problems relying on extensive computation, and that it increases the trust the mathematical community places in computer-assisted proofs.
Cite as

Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule. Formal Verification of the Empty Hexagon Number. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{subercaseaux_et_al:LIPIcs.ITP.2024.35,
  author =	{Subercaseaux, Bernardo and Nawrocki, Wojciech and Gallicchio, James and Codel, Cayden and Carneiro, Mario and Heule, Marijn J. H.},
  title =	{{Formal Verification of the Empty Hexagon Number}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{35:1--35:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.35},
  URN =		{urn:nbn:de:0030-drops-207633},
  doi =		{10.4230/LIPIcs.ITP.2024.35},
  annote =	{Keywords: Empty Hexagon Number, Discrete Computational Geometry, Erd\H{o}s-Szekeres}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2023.38
Formalizing Almost Development Closed Critical Pairs (Short Paper)

Authors: Christina Kohl and Aart Middeldorp

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
We report on the first formalization of the almost-development closedness criterion for confluence of left-linear term rewrite systems and illustrate a problem we encountered while trying to formalize the original paper proof by van Oostrom.
Cite as

Christina Kohl and Aart Middeldorp. Formalizing Almost Development Closed Critical Pairs (Short Paper). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 38:1-38:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kohl_et_al:LIPIcs.ITP.2023.38,
  author =	{Kohl, Christina and Middeldorp, Aart},
  title =	{{Formalizing Almost Development Closed Critical Pairs}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{38:1--38:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.38},
  URN =		{urn:nbn:de:0030-drops-184130},
  doi =		{10.4230/LIPIcs.ITP.2023.38},
  annote =	{Keywords: Term rewriting, confluence, certification}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.12
Hydra Battles and AC Termination

Authors: Nao Hirokawa and Aart Middeldorp

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Hercules to beat Hydra. To prove the termination of our encoding, we employ type introduction in connection with many-sorted semantic labeling for AC rewriting and AC-RPO.
Cite as

Nao Hirokawa and Aart Middeldorp. Hydra Battles and AC Termination. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{hirokawa_et_al:LIPIcs.FSCD.2023.12,
  author =	{Hirokawa, Nao and Middeldorp, Aart},
  title =	{{Hydra Battles and AC Termination}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and 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.FSCD.2023.12},
  URN =		{urn:nbn:de:0030-drops-179965},
  doi =		{10.4230/LIPIcs.FSCD.2023.12},
  annote =	{Keywords: battle of Hercules and Hydra, term rewriting, termination}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.27
Polynomial Termination Over ℕ Is Undecidable

Authors: Fabian Mitterwallner and Aart Middeldorp

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
In this paper we prove via a reduction from Hilbert’s 10th problem that the problem whether the termination of a given rewrite system can be shown by a polynomial interpretation in the natural numbers is undecidable, even for rewrite systems that are incrementally polynomially terminating. We also prove that incremental polynomial termination is an undecidable property of terminating rewrite systems.
Cite as

Fabian Mitterwallner and Aart Middeldorp. Polynomial Termination Over ℕ Is Undecidable. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{mitterwallner_et_al:LIPIcs.FSCD.2022.27,
  author =	{Mitterwallner, Fabian and Middeldorp, Aart},
  title =	{{Polynomial Termination Over \mathbb{N} Is Undecidable}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.27},
  URN =		{urn:nbn:de:0030-drops-163081},
  doi =		{10.4230/LIPIcs.FSCD.2022.27},
  annote =	{Keywords: Term Rewriting, Polynomial Termination, Undecidability}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.30
Completion for Logically Constrained Rewriting

Authors: Sarah Winkler and Aart Middeldorp

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We propose an abstract completion procedure for logically constrained term rewrite systems (LCTRSs). This procedure can be instantiated to both standard Knuth-Bendix completion and ordered completion for LCTRSs, and we present a succinct and uniform correctness proof. A prototype implementation illustrates the viability of the new completion approach.
Cite as

Sarah Winkler and Aart Middeldorp. Completion for Logically Constrained Rewriting. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{winkler_et_al:LIPIcs.FSCD.2018.30,
  author =	{Winkler, Sarah and Middeldorp, Aart},
  title =	{{Completion for Logically Constrained Rewriting}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{30:1--30:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.30},
  URN =		{urn:nbn:de:0030-drops-92001},
  doi =		{10.4230/LIPIcs.FSCD.2018.30},
  annote =	{Keywords: Constrained rewriting, completion, automation, theorem proving}
}
Document
System Description
DOI: 10.4230/LIPIcs.FSCD.2018.31
ProTeM: A Proof Term Manipulator (System Description)

Authors: Christina Kohl and Aart Middeldorp

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
Proof terms are a useful concept for reasoning about computations in term rewriting. Human calculation with proof terms is tedious and error-prone. We present ProTeM, a new tool that offers support for manipulating proof terms that represent multisteps in left-linear rewrite systems.
Cite as

Christina Kohl and Aart Middeldorp. ProTeM: A Proof Term Manipulator (System Description). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 31:1-31:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kohl_et_al:LIPIcs.FSCD.2018.31,
  author =	{Kohl, Christina and Middeldorp, Aart},
  title =	{{ProTeM: A Proof Term Manipulator}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{31:1--31:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.31},
  URN =		{urn:nbn:de:0030-drops-92013},
  doi =		{10.4230/LIPIcs.FSCD.2018.31},
  annote =	{Keywords: Proof terms, term rewriting, interactive tool}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.32
Confluence Competition 2018

Authors: Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We report on the 2018 edition of the Confluence Competition, a competition of software tools that aim to (dis)prove confluence and related properties of rewrite systems automatically.
Cite as

Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl. Confluence Competition 2018. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 32:1-32:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{aoto_et_al:LIPIcs.FSCD.2018.32,
  author =	{Aoto, Takahito and Hamana, Makoto and Hirokawa, Nao and Middeldorp, Aart and Nagele, Julian and Nishida, Naoki and Shintani, Kiraku and Zankl, Harald},
  title =	{{Confluence Competition 2018}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{32:1--32:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.32},
  URN =		{urn:nbn:de:0030-drops-92023},
  doi =		{10.4230/LIPIcs.FSCD.2018.32},
  annote =	{Keywords: Confluence, competition, rewrite systems}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.19
Infinite Runs in Abstract Completion

Authors: Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
Completion is one of the first and most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In an earlier paper we presented a new and formalized correctness proof of abstract completion for finite runs. In this paper we extend our analysis and our formalization to infinite runs, resulting in a new proof that fair infinite runs produce complete presentations of the initial equations. We further consider ordered completion - an important extension of completion that aims to produce ground-complete presentations of the initial equations. Moreover, we revisit and extend results of Métivier concerning canonicity of rewrite systems. All proofs presented in the paper have been formalized in Isabelle/HOL.
Cite as

Nao Hirokawa, Aart Middeldorp, Christian Sternagel, and Sarah Winkler. Infinite Runs in Abstract Completion. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 19:1-19:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{hirokawa_et_al:LIPIcs.FSCD.2017.19,
  author =	{Hirokawa, Nao and Middeldorp, Aart and Sternagel, Christian and Winkler, Sarah},
  title =	{{Infinite Runs in Abstract Completion}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{19:1--19:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.19},
  URN =		{urn:nbn:de:0030-drops-77252},
  doi =		{10.4230/LIPIcs.FSCD.2017.19},
  annote =	{Keywords: term rewriting, abstract completion, ordered completion, canonicity, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.36
Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems

Authors: Franziska Rapp and Aart Middeldorp

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
The first-order theory of rewriting is decidable for finite left-linear right-ground rewrite systems. We present a new tool that implements the decision procedure for this theory. It is based on tree automata techniques. The tool offers the possibility to synthesize rewrite systems that satisfy properties that are expressible in the first-order theory of rewriting.
Cite as

Franziska Rapp and Aart Middeldorp. Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 36:1-36:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{rapp_et_al:LIPIcs.FSCD.2016.36,
  author =	{Rapp, Franziska and Middeldorp, Aart},
  title =	{{Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{36:1--36:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.36},
  URN =		{urn:nbn:de:0030-drops-60018},
  doi =		{10.4230/LIPIcs.FSCD.2016.36},
  annote =	{Keywords: first-order theory, ground rewrite systems, automation, synthesis}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.209
Leftmost Outermost Revisited

Authors: Nao Hirokawa, Aart Middeldorp, and Georg Moser

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

Abstract
We present an elementary proof of the classical result that the leftmost outermost strategy is normalizing for left-normal orthogonal rewrite systems. Our proof is local and extends to hyper-normalization and weakly orthogonal systems. Based on the new proof, we study basic normalization, i.e., we study normalization if the set of considered starting terms is restricted to basic terms. This allows us to weaken the left-normality restriction. We show that the leftmost outermost strategy is hyper-normalizing for basically left-normal orthogonal rewrite systems. This shift of focus greatly extends the applicability of the classical result, as evidenced by the experimental data provided.
Cite as

Nao Hirokawa, Aart Middeldorp, and Georg Moser. Leftmost Outermost Revisited. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 209-222, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{hirokawa_et_al:LIPIcs.RTA.2015.209,
  author =	{Hirokawa, Nao and Middeldorp, Aart and Moser, Georg},
  title =	{{Leftmost Outermost Revisited}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{209--222},
  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.209},
  URN =		{urn:nbn:de:0030-drops-51986},
  doi =		{10.4230/LIPIcs.RTA.2015.209},
  annote =	{Keywords: term rewriting, strategies, normalization}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.223
Conditional Complexity

Authors: Cynthia Kop, Aart Middeldorp, and Thomas Sternagel

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

Abstract
We propose a notion of complexity for oriented conditional term rewrite systems. This notion is realistic in the sense that it measures not only successful computations but also partial computations that result in a failed rule application. A transformation to unconditional context-sensitive rewrite systems is presented which reflects this complexity notion, as well as a technique to derive runtime and derivational complexity bounds for the latter.
Cite as

Cynthia Kop, Aart Middeldorp, and Thomas Sternagel. Conditional Complexity. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 223-240, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kop_et_al:LIPIcs.RTA.2015.223,
  author =	{Kop, Cynthia and Middeldorp, Aart and Sternagel, Thomas},
  title =	{{Conditional Complexity}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{223--240},
  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.223},
  URN =		{urn:nbn:de:0030-drops-51999},
  doi =		{10.4230/LIPIcs.RTA.2015.223},
  annote =	{Keywords: conditional term rewriting, complexity}
}
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.319
Normalized Completion Revisited

Authors: Sarah Winkler and Aart Middeldorp

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

Abstract
Normalized completion (Marché 1996) is a widely applicable and efficient technique for com- pletion modulo theories. If successful, a normalized completion procedure computes a rewrite system that allows to decide the validity problem using normalized rewriting. In this paper we consider a slightly simplified inference system for finite normalized completion runs. We prove correctness, show faithfulness of critical pair criteria in our setting, and propose a different notion of normalizing pairs. We then show how normalized completion procedures can benefit from AC- termination tools instead of relying on a fixed AC-compatible reduction order. We outline our implementation of this approach in the completion tool mkbtt and present experimental results, including new completions.
Cite as

Sarah Winkler and Aart Middeldorp. Normalized Completion Revisited. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 319-334, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{winkler_et_al:LIPIcs.RTA.2013.319,
  author =	{Winkler, Sarah and Middeldorp, Aart},
  title =	{{Normalized Completion Revisited}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{319--334},
  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.319},
  URN =		{urn:nbn:de:0030-drops-40702},
  doi =		{10.4230/LIPIcs.RTA.2013.319},
  annote =	{Keywords: term rewriting, completion}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.335
Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence

Authors: Sarah Winkler, Harald Zankl, and Aart Middeldorp

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

Abstract
Kirby and Paris (1982) proved in a celebrated paper that a theorem of Goodstein (1944) cannot be established in Peano (1889) arithmetic. We present an encoding of Goodstein's theorem as a termination problem of a finite rewrite system. Using a novel implementation of ordinal interpretations, we are able to automatically prove termination of this system, resulting in the first automatic termination proof for a system whose derivational complexity is not multiple recursive. Our method can also cope with the encoding by Touzet (1998) of the battle of Hercules and Hydra, yet another system which has been out of reach for automated tools, until now.
Cite as

Sarah Winkler, Harald Zankl, and Aart Middeldorp. Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 335-351, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{winkler_et_al:LIPIcs.RTA.2013.335,
  author =	{Winkler, Sarah and Zankl, Harald and Middeldorp, Aart},
  title =	{{Beyond Peano Arithmetic – Automatically Proving Termination of the Goodstein Sequence}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{335--351},
  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.335},
  URN =		{urn:nbn:de:0030-drops-40718},
  doi =		{10.4230/LIPIcs.RTA.2013.335},
  annote =	{Keywords: term rewriting, termination, automation, ordinals}
}
  • Refine by Author
  • 19 Middeldorp, Aart
  • 5 Winkler, Sarah
  • 5 Zankl, Harald
  • 4 Hirokawa, Nao
  • 3 Felgenhauer, Bertram
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 9 term rewriting
  • 4 automation
  • 4 termination
  • 3 Term rewriting
  • 3 confluence
  • Show More...

  • Refine by Type
  • 21 document

  • Refine by Publication Year
  • 3 2011
  • 3 2015
  • 3 2018
  • 2 2010
  • 2 2013
  • Show More...

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 About DROPS Imprint Privacy Contact