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

@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"
}