Termination Tools in Ordered Completion
Sarah Winkler and Aart MiddeldorpProceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Lecture Notes in Artificial Intelligence 6173, pp. 518 – 532, 2010.
Abstract
Ordered completion is one of the most frequently used calculi in
equational theorem proving. The performance of an ordered completion
run strongly depends on the reduction order supplied as input.
This paper describes how termination tools can replace fixed
reduction orders in ordered completion procedures, thus allowing for a
novel degree of automation. Our method can be combined with the
multi-completion approach proposed by Kondo and Kurihara. We present
experimental results obtained with our ordered completion tool
oMKBtt for both ordered completion and equational theorem proving.
BibTeX
@inproceedings{SWAM-IJCAR10, author = "Sarah Winkler and Aart Middeldorp", title = "Termination Tools in Ordered Completion", booktitle = "Proceedings of the 5th International Joint Conference on Automated Reasoning", series = "Lecture Notes in Artificial Intelligence", volume = 6173, pages = "518--532", publisher = "Springer-Verlag", year = 2010 }