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

@inproceedings{SWAM-CADE11,
  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
}