cl-banner

Ordinals and Knuth-Bendix Orders

Sarah Winkler, Harald Zankl, and Aart Middeldorp

Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18), Lecture Notes in Artificial Intelligence (Advanced Research in Computing and Software Science) 7180, pp. 420 – 434, 2012.

Abstract

In this paper we consider a hierarchy of three versions of Knuth-Bendix orders. (1) We show that the standard definition can be (slightly) simplified without affecting the ordering relation. (2) For the extension of transfinite Knuth-Bendix orders we show that transfinite ordinals are not needed as weights, as far as termination of finite rewrite systems is concerned. (3) Nevertheless termination proving benefits from transfinite ordinals when used in the setting of general Knuth-Bendix orders defined over a weakly monotone algebra. We investigate the relationship to polynomial interpretations and present experimental results for both termination analysis and ordered completion. For the latter it is essential that the order is totalizable on ground terms.

 

  PDF |    doi:10.1007/978-3-642-28717-6_33  |  © Springer

BibTeX 

@inproceedings{SWHZAM-LPAR18,
author = "Sarah Winkler and Harald Zankl and Aart Middeldorp",
title = "Ordinals and {Knuth-Bendix} Orders",
booktitle = "Proceedings of the 18th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning",
series = "Lecture Notes in Computer Science (Advanced Research in
Computing and Software Science)",
volume = 7180,
pages = "420--434",
year = 2012
}
Nach oben scrollen