Search Results

Documents authored by Hirokawa, Nao

Document
DOI: 10.4230/LIPIcs.FSCD.2024.13
Simulating Dependency Pairs by Semantic Labeling

Authors: Teppei Saito and Nao Hirokawa

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
We show that termination proofs by a version of the dependency pair method can be simulated by semantic labeling plus multiset path orders. By incorporating a flattening technique into multiset path orders the simulation result can be extended to the dependency pair method for relative termination, introduced by Iborra et al. This result allows us to improve applicability of their dependency pair method.
Cite as

Teppei Saito and Nao Hirokawa. Simulating Dependency Pairs by Semantic Labeling. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 13:1-13:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{saito_et_al:LIPIcs.FSCD.2024.13,
  author =	{Saito, Teppei and Hirokawa, Nao},
  title =	{{Simulating Dependency Pairs by Semantic Labeling}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{13:1--13:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.13},
  URN =		{urn:nbn:de:0030-drops-203423},
  doi =		{10.4230/LIPIcs.FSCD.2024.13},
  annote =	{Keywords: Term rewriting, Relative termination, Semantic labeling, Dependency pairs}
}
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.28
Compositional Confluence Criteria

Authors: Kiraku Shintani and Nao Hirokawa

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

Abstract
We show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of orthogonality, rule labeling, and critical pair systems for term rewriting are recast into composable forms. In addition to them, we prove that Toyama’s parallel closedness result based on parallel critical pairs subsumes his almost parallel closedness theorem.
Cite as

Kiraku Shintani and Nao Hirokawa. Compositional Confluence Criteria. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{shintani_et_al:LIPIcs.FSCD.2022.28,
  author =	{Shintani, Kiraku and Hirokawa, Nao},
  title =	{{Compositional Confluence Criteria}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{28:1--28:19},
  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.28},
  URN =		{urn:nbn:de:0030-drops-163095},
  doi =		{10.4230/LIPIcs.FSCD.2022.28},
  annote =	{Keywords: term rewriting, confluence, decreasing diagrams}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2021.2
Completion and Reduction Orders (Invited Talk)

Authors: Nao Hirokawa

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
We present three techniques for improving the Knuth-Bendix completion procedure and its variants: An order extension by semantic labeling, a new confluence criterion for terminating term rewrite systems, and inter-reduction for maximal completion.
Cite as

Nao Hirokawa. Completion and Reduction Orders (Invited Talk). In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 2:1-2:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{hirokawa:LIPIcs.FSCD.2021.2,
  author =	{Hirokawa, Nao},
  title =	{{Completion and Reduction Orders}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{2:1--2:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.2},
  URN =		{urn:nbn:de:0030-drops-142403},
  doi =		{10.4230/LIPIcs.FSCD.2021.2},
  annote =	{Keywords: term rewriting, completion, reduction order}
}
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.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.2011.71
Maximal Completion

Authors: Dominik Klein and Nao Hirokawa

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
Given an equational system, completion procedures compute an equivalent and complete (terminating and confluent) term rewrite system. We present a very simple and efficient completion procedure, which is based on MaxSAT solving. Experiments show that the procedure is comparable to recent powerful completion tools.
Cite as

Dominik Klein and Nao Hirokawa. Maximal Completion. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 71-80, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{klein_et_al:LIPIcs.RTA.2011.71,
  author =	{Klein, Dominik and Hirokawa, Nao},
  title =	{{Maximal Completion}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{71--80},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.71},
  URN =		{urn:nbn:de:0030-drops-31295},
  doi =		{10.4230/LIPIcs.RTA.2011.71},
  annote =	{Keywords: Term Rewriting, Knuth-Bendix Completion, Multi-completion}
}
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