Advertisement
Published in:
2011 | OriginalPaper | Chapter
Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
Authors : Carsten Fuhs, Cynthia Kop
Published in: Frontiers of Combining Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.