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
Secondary volumes: Selected Papers of the 8th International Conference on Formal Structures and Deduction (FSCD 2023)
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 1122 times.
This article's PDF has been downloaded 222 times.