MOVES Seminar 30 Sept, 2011, 11:00

Harnessing First Order Termination Provers Using Higher Order Dependency
Pairs


Many functional programs and higher order term rewrite systems contain, besides higher order rules, also a significant first order part. We discuss how an automatic termination prover can split a rewrite system into a first order and a higher order part. The results are applicable to all common styles of higher order rewriting with simple types, although some dependency pair approach is needed to use them.