Nao Hirokawa ; Aart Middeldorp - Hydra Battles and AC Termination

lmcs:13184 - Logical Methods in Computer Science, June 27, 2025, Volume 21, Issue 2 - https://doi.org/10.46298/lmcs-21(2:29)2025
Hydra Battles and AC TerminationArticle

Authors: Nao Hirokawa ; Aart Middeldorp

    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.


    Volume: Volume 21, Issue 2
    Published on: June 27, 2025
    Accepted on: April 3, 2025
    Submitted on: March 6, 2024
    Keywords: Logic in Computer Science

    Consultation statistics

    This page has been seen 161 times.
    This article's PDF has been downloaded 41 times.