Termination proving has traditionally been based on the search for (possibly lexicographic) ranking functions. In recent years, however, the discovery of termination proof techniques based on Ramsey's theorem have led to new automation strategies, e.g. size-change, or iterative reductions from termination to safety. In this paper we revisit the decision to use Ramsey-based termination arguments in the iterative approach. We describe a new iterative termination proving procedure that instead searches for lexicographic termination arguments. Using experimental evidence we show that this new method leads to dramatic speedups. © 2013 Springer-Verlag.
CITATION STYLE
Cook, B., See, A., & Zuleger, F. (2013). Ramsey vs. lexicographic termination proving. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7795 LNCS, pp. 47–61). https://doi.org/10.1007/978-3-642-36742-7_4
Mendeley helps you to discover research relevant for your work.