AC Completion with Termination Tools

Sarah Winkler and Aart Middeldorp

Proceedings of the 23rd International Conference on Automated Deduction (CADE 2011), Lecture Notes in Artificial Intelligence 6803, pp. 492 – 498, 2011.


We present mascott, a tool for Knuth-Bendix completion modulo the theory of associative and commutative operators. In contrast to classical completion tools, mascott does not rely on a fixed AC-compatible reduction order. Instead, a suitable order is implicitly constructed during a deduction by collecting all oriented rules in a similar fashion as done in the tool Slothrop. This allows for convergent systems which cannot be completed using standard orders. We outline the underlying inference system and comment on implementation details such as the use of multi-completion, term indexing techniques, and critical pair criteria.


  PDF |    doi:10.1007/978-3-642-22438-6_37  |  © Springer


author = "Sarah Winkler and Aart Middeldorp",
title = "AC Completion with Termination Tools",
booktitle = "Proceedings of the 23rd International Conference on Automated Deduction",
address = "Wroclaw",
series = "Lecture Notes in Artificial Intelligence",
volume = 6803,
pages = "492--498",
year = 2011
Nach oben scrollen