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{NHAM-FSCD23,
 author    = "Nao Hirokawa and Aart Middeldorp",
 title     = "Hydra Battles and {AC} Termination",
 booktitle = "Proceedings of the 8th International Conference on Formal
              Structures for Computation and Deduction",
 editor    = "Marco Gaboardi and Femke van Raamsdonk",
 series    = "Leibniz International Proceedings in Informatics",
 volume    = 260,
 pages     = "12:1--12:16",
 year      = 2023,
 doi       = "10.4230/LIPIcs.FSCD.2023.12"
}