5 Search Results for "Yamada, Akihisa"

Document
DOI: 10.4230/LIPIcs.ITP.2023.34
Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)

Authors: Akihisa Yamada and Jérémy Dubut

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

Abstract
Directed sets are of fundamental interest in domain theory and topology. In this paper, we formalize some results on directed sets in Isabelle/HOL, most notably: under the axiom of choice, a poset has a supremum for every directed set if and only if it does so for every chain; and a function between such posets preserves suprema of directed sets if and only if it preserves suprema of chains. The known pen-and-paper proofs of these results crucially use uncountable transfinite sequences, which are not directly implementable in Isabelle/HOL. We show how to emulate such proofs by utilizing Isabelle/HOL’s ordinal and cardinal library. Thanks to the formalization, we relax some conditions for the above results.
Cite as

Akihisa Yamada and Jérémy Dubut. Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 34:1-34:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{yamada_et_al:LIPIcs.ITP.2023.34,
  author =	{Yamada, Akihisa and Dubut, J\'{e}r\'{e}my},
  title =	{{Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{34:1--34:13},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.34},
  URN =		{urn:nbn:de:0030-drops-184092},
  doi =		{10.4230/LIPIcs.ITP.2023.34},
  annote =	{Keywords: Directed Sets, Completeness, Scott Continuous Functions, Ordinals, Isabelle/HOL}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2023.4
Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk)

Authors: Akihisa Yamada

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

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.
Cite as

Akihisa Yamada. Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 4:1-4:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.4},
  URN =		{urn:nbn:de:0030-drops-179882},
  doi =		{10.4230/LIPIcs.FSCD.2023.4},
  annote =	{Keywords: Term rewriting, Termination, Isabelle/HOL, Competition}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2020.4
Certifying the Weighted Path Order (Invited Talk)

Authors: René Thiemann, Jonas Schöpf, Christian Sternagel, and Akihisa Yamada

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
The weighted path order (WPO) unifies and extends several termination proving techniques that are known in term rewriting. Consequently, the first tool implementing WPO could prove termination of rewrite systems for which all previous tools failed. However, we should not blindly trust such results, since there might be problems with the implementation or the paper proof of WPO. In this work, we increase the reliability of these automatically generated proofs. To this end, we first formally prove the properties of WPO in Isabelle/HOL, and then develop a verified algorithm to certify termination proofs that are generated by tools using WPO. We also include support for max-polynomial interpretations, an important ingredient in WPO. Here we establish a connection to an existing verified SMT solver. Moreover, we extend the termination tools NaTT and TTT2, so that they can now generate certifiable WPO proofs.
Cite as

René Thiemann, Jonas Schöpf, Christian Sternagel, and Akihisa Yamada. Certifying the Weighted Path Order (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{thiemann_et_al:LIPIcs.FSCD.2020.4,
  author =	{Thiemann, Ren\'{e} and Sch\"{o}pf, Jonas and Sternagel, Christian and Yamada, Akihisa},
  title =	{{Certifying the Weighted Path Order}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{4:1--4:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.4},
  URN =		{urn:nbn:de:0030-drops-123263},
  doi =		{10.4230/LIPIcs.FSCD.2020.4},
  annote =	{Keywords: certification, Isabelle/HOL, reduction order, termination analysis}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.30
Complete Non-Orders and Fixed Points

Authors: Akihisa Yamada and Jérémy Dubut

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
In this paper, we develop an Isabelle/HOL library of order-theoretic concepts, such as various completeness conditions and fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often without any property of ordering, thus complete non-orders. In particular, we generalize the Knaster - Tarski theorem so that we ensure the existence of a quasi-fixed point of monotone maps over complete non-orders, and show that the set of quasi-fixed points is complete under a mild condition - attractivity - which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene’s fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene’s fixed points are least quasi-fixed points.
Cite as

Akihisa Yamada and Jérémy Dubut. Complete Non-Orders and Fixed Points. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{yamada_et_al:LIPIcs.ITP.2019.30,
  author =	{Yamada, Akihisa and Dubut, J\'{e}r\'{e}my},
  title =	{{Complete Non-Orders and Fixed Points}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.30},
  URN =		{urn:nbn:de:0030-drops-110852},
  doi =		{10.4230/LIPIcs.ITP.2019.30},
  annote =	{Keywords: Order Theory, Lattice Theory, Fixed-Points, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.8
AC Dependency Pairs Revisited

Authors: Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
Rewriting modulo AC, i.e., associativity and/or commutativity of certain symbols, is among the most frequently used extensions of term rewriting by equational theories. In this paper we present a generalization of the dependency pair framework for termination analysis to rewriting modulo AC. It subsumes existing variants of AC dependency pairs, admits standard dependency graph analyses, and in particular enjoys the minimality property in the standard sense. As a direct benefit, important termination techniques are easily extended; we describe usable rules and the subterm criterion for AC termination, which properly generalize the non-AC versions. We also perform these extensions within IsaFoR - the Isabelle formalization of rewriting - and thereby provide the first formalization of AC dependency pairs. Consequently, our certifier CeTA now supports checking proofs of AC termination.
Cite as

Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari. AC Dependency Pairs Revisited. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{yamada_et_al:LIPIcs.CSL.2016.8,
  author =	{Yamada, Akihisa and Sternagel, Christian and Thiemann, Ren\'{e} and Kusakari, Keiichirou},
  title =	{{AC Dependency Pairs Revisited}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{8:1--8:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.8},
  URN =		{urn:nbn:de:0030-drops-65488},
  doi =		{10.4230/LIPIcs.CSL.2016.8},
  annote =	{Keywords: Equational Rewriting, Termination, Dependency Pairs, Certification}
}
  • Refine by Author
  • 5 Yamada, Akihisa
  • 2 Dubut, Jérémy
  • 2 Sternagel, Christian
  • 2 Thiemann, René
  • 1 Kusakari, Keiichirou
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Automated reasoning
  • 1 Theory of computation → Denotational semantics
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Interactive proof systems
  • 1 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 4 Isabelle/HOL
  • 2 Termination
  • 1 Certification
  • 1 Competition
  • 1 Completeness
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2023
  • 1 2016
  • 1 2019
  • 1 2020

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