Multi-Completion with Termination Tools

Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara

Journal of Automated Reasoning 50(3), pp. 317 – 354, 2013.


Knuth–Bendix completion is a classical calculus in automated deduction for transforming a set of equations into a confluent and terminating set of directed equations which can be used to decide the induced equational theory. Multi-completion with termination tools constitutes an approach that differs from the classical method in two respects: (1) external termination tools replace the reduction order – a typically critical parameter – as proposed by Wehrman et al. (2006), and (2) multi-completion as introduced by Kurihara and Kondo (1999) is used to keep track of multiple orientations in parallel while exploiting sharing to boost efficiency. In this paper we describe the inference system, give the full proof of its correctness and comment on completeness issues. Critical pair criteria and isomorphisms are presented as refinements together with all proofs. We furthermore describe the implementation of our approach in the tool mkbTT, present extensive experimental results and report on new completions.


  PDF |    doi:10.1007/s10817-012-9249-2  |  © Creative Commons


author = "S.~Winkler and H.~Sato and A.~Middeldorp and M.~Kurihara",
title = "Multi-Completion with Termination Tools",
journal = "Journal of Automated Reasoning",
volume = 50,
number = 3,
pages = "317--354",
year = 2013
Nach oben scrollen