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.12
URN: urn:nbn:de:0030-drops-179965
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17996/
Hirokawa, Nao ;
Middeldorp, Aart
Hydra Battles and AC Termination
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.
BibTeX - Entry
@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/opus/volltexte/2023/17996},
URN = {urn:nbn:de:0030-drops-179965},
doi = {10.4230/LIPIcs.FSCD.2023.12},
annote = {Keywords: battle of Hercules and Hydra, term rewriting, termination}
}
Keywords: |
|
battle of Hercules and Hydra, term rewriting, termination |
Collection: |
|
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) |
Issue Date: |
|
2023 |
Date of publication: |
|
28.06.2023 |