Abstract

Showing termination of the Battle of Hercules and Hydra is a challenge.
We present the battle both as a rewrite system and as an arithmetic while
program, provide proofs of their termination, and recall why their
termination cannot be proved within Peano arithmetic.

BibTeX

@inproceedings{DM-JPJ60,
  author      = "Nachum Dershowitz and Georg Moser",
  title       = "The Hydra Battle Revisited",
  booktitle   = "Rewriting, Computation and Proof; Essays Dedicated to
                 Jean-Pierre Jouannaud on the Occasion of his 60th
                 Birthday",
  series      = "Lecture Notes in Computer Science",
  volume      = 4600,
  pages       = "1--27",
  publisher   = "Springer-Verlag",
  year        = 2007
}