2026-07-22T18:34:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17996 2024-03-06T11:00:49Z ddc:004 open_access

Hydra Battles and AC Termination Hirokawa, Nao Middeldorp, Aart battle of Hercules and Hydra term rewriting termination 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nao Hirokawa and Aart Middeldorp 2023 Is Part Of LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2023.12 urn:nbn:de:0030-drops-179965 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.12 eng https://creativecommons.org/licenses/by/4.0/legalcode