Harnessing First Order Termination Provers Using Higher Order Dependency Pairs

C. Fuhs, C.L.M. Kop

Research output: Contribution to JournalArticleAcademicpeer-review


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. © 2011 Springer-Verlag.
Original languageEnglish
Pages (from-to)147-162
JournalLecture Notes in Computer Science
Publication statusPublished - 2011
EventFrontiers of Combining Systems -
Duration: 1 Jan 20111 Jan 2011

Bibliographical note

Proceedings title: Proc. 8th Symposium on Frontiers of Combining Systems - FroCoS'11
Publisher: Springer
ISBN: 978-3-642-24363-9
Editors: C. Tinelli, V. Sofronie-Stokkermans


Dive into the research topics of 'Harnessing First Order Termination Provers Using Higher Order Dependency Pairs'. Together they form a unique fingerprint.

Cite this