License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2023.4
URN: urn:nbn:de:0030-drops-179882
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17988/
Go to the corresponding LIPIcs Volume Portal

Yamada, Akihisa

Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk)

pdf-format:
LIPIcs-FSCD-2023-4.pdf (0.6 MB)

Abstract

Automated termination analysis is a central topic in the research of term rewriting. In this talk, I will first review the theoretical foundation of termination of term rewriting, leading to the recently established tuple interpretation method. Then I will present an Isabelle/HOL formalization of the theory. Although the formalization is based on the existing library IsaFoR (Isabelle Formalization of Rewriting), the present work takes another approach of representing relations (predicates rather than sets) so that the notation is more human friendly. Then I will present a unified implementation of the termination analysis techniques via SMT encoding, leading to the termination prover NaTT. Many tools have been developed for termination analysis and have been competing annually in termCOMP (Termination Competition) for two decades. At the end of the talk, I will share my experience in organizing termCOMP in the last five years.

BibTeX - Entry

@InProceedings{yamada:LIPIcs.FSCD.2023.4,
  author =	{Yamada, Akihisa},
  title =	{{Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{4:1--4:5},
  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/opus/volltexte/2023/17988},
  URN =		{urn:nbn:de:0030-drops-179882},
  doi =		{10.4230/LIPIcs.FSCD.2023.4},
  annote =	{Keywords: Term rewriting, Termination, Isabelle/HOL, Competition}
}

Keywords: Term rewriting, Termination, Isabelle/HOL, Competition
Collection: 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Issue Date: 2023
Date of publication: 28.06.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI