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
}