Termination Tools in Ordered Completion

Sarah Winkler and Aart Middeldorp

Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Lecture Notes in Artificial Intelligence 6173, pp. 518 – 532, 2010.


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 tooloMKBtt for both ordered completion and equational theorem proving.


  PDF |    doi:10.1007/978-3-642-14203-1_43  |  ©  Springer


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
Nach oben scrollen