Abstract

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.

BibTeX Entry

@inproceedings{WM-CADE11,
 author    = "Sarah Winkler and Aart Middeldorp",
 title     = "{AC} Completion with Termination Tools",
 booktitle = "Proceedings of the 23rd International Conference on Automated
              Deduction",
 series    = "Lecture Notes in Artificial Intelligence",
 volume    = 6803,
 pages     = "492--498",
 year      = 2011,
 doi       = "10.1007/978-3-642-22438-6\_37"
}