Search Results

Documents authored by Winkler, Sarah

Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2019.3
Extending Maximal Completion (Invited Talk)

Authors: Sarah Winkler

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

Abstract
Maximal completion (Klein and Hirokawa 2011) is an elegantly simple yet powerful variant of Knuth-Bendix completion. This paper extends the approach to ordered completion and theorem proving as well as normalized completion. An implementation of the different procedures is described, and its practicality is demonstrated by various examples.
Cite as

Sarah Winkler. Extending Maximal Completion (Invited Talk). In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{winkler:LIPIcs.FSCD.2019.3,
  author =	{Winkler, Sarah},
  title =	{{Extending Maximal Completion}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{3:1--3:15},
  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.3},
  URN =		{urn:nbn:de:0030-drops-105102},
  doi =		{10.4230/LIPIcs.FSCD.2019.3},
  annote =	{Keywords: automated reasoning, completion, theorem proving}
}
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
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.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}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.373
Optimizing mkbTT

Authors: Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
We describe performance enhancements that have been added to mkbTT, a modern completion tool combining multi-completion with the use of termination tools.
Cite as

Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara. Optimizing mkbTT. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 373-384, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{winkler_et_al:LIPIcs.RTA.2010.373,
  author =	{Winkler, Sarah and Sato, Haruhiko and Middeldorp, Aart and Kurihara, Masahito},
  title =	{{Optimizing mkbTT}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{373--384},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.373},
  URN =		{urn:nbn:de:0030-drops-26643},
  doi =		{10.4230/LIPIcs.RTA.2010.373},
  annote =	{Keywords: Knuth-Bendix completion, termination prover, automated deduction}
}
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