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-MPO, a new AC
compatible reduction order that can be seen as a much weakened version of
AC-RPO.

BibTeX

@article{NHAM-LMCS21,
 author    = "Nao Hirokawa and Aart Middeldorp",
 title     = "Hydra Battles and {AC} Termination",
 journal   = "Logical Methods in Computer Science",
 volume    = 21,
 number    = 2,
 pages     = "29:1--29:22",
 year      = 2025,
 doi       = "10.46298/lmcs-21(2:29)2025"
}