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 Entry

@inproceedings{WM-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",
 year      = 2010,
 doi       = "10.1007/978-3-642-14203-1\_43"
}