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 omkb TT for both ordered completion and equational theorem proving. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Winkler, S., & Middeldorp, A. (2010). Termination tools in ordered completion. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6173 LNAI, pp. 518–532). https://doi.org/10.1007/978-3-642-14203-1_43
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
