Abstract

This paper describes two advancements of SAT-based Knuth-Bendix completion as implemented in Maxcomp. (1) Termination techniques using the dependency pair framework are encoded as satisfiability problems, including dependency graph and reduction pair processors. (2) Instead of relying on pure maximal completion, different SAT-encoded control strategies are exploited.

Experiments show that these developments let Maxcomp improve over other automatic completion tools, and produce novel complete systems.

BibTeX

@inproceedings{HSSW-CADE15,
  author    = "Haruhiko Sato and Sarah Winkler",
  title     = "Encoding Dependency Pair Techniques and Control Strategies
               for Maximal Completion",
  booktitle = "Proceedings of the 25th International Conference on
               Automated Deduction (CADE-25)",
  editor    = "Amy Felty and Aart Middeldorp",
  series    = "Lecture Notes in Artificial Intelligence",
  volume    = 9195,
  pages     = "152--162",
  year      = 2015,
  doi       = "10.1007/978-3-319-21401-6_10"
}