Abstract

In rewriting the Hydra battle refers to a term rewrite system
H proposed by Dershowitz and Jouannaud. To date, H withstands
any attempt to prove its termination automatically. This motivates
our interest in term rewrite systems encoding the Hydra battle,
as a careful study of such systems may prove useful in the design
of automatic termination tools. Moreover it has been an open
problem, whether any termination order compatible with H has to
have the Howard-Bachmann ordinal as its order type, i.e., the proof
theoretic ordinal of the theory of one inductive definition. We
answer this question in the negative, by providing a reduction order
compatible with H, whose order is at most epsilon_0, the proof
theoretic ordinal of Peano arithmetic.

BibTeX

@article{GM-AAECC09,
author      = "Georg Moser",
title       = "The {H}ydra {B}attle and {C}ichon's {P}rinciple",
journal     = "Applicable Algebra in Engineering, Communication and
               Computing",
volume      = 20,
number      = 2,
year        = 2009,
pages       = "133--158"
}