DROPS

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

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}
}

Search Results

Documents authored by Kohl, Christina

Formalizing Almost Development Closed Critical Pairs (Short Paper)

Abstract

Cite as

ProTeM: A Proof Term Manipulator (System Description)

Abstract

Cite as

Thanks for your feedback!

Could not send message