A Satisfiability Encoding of Dependency Pair Techniques for Maximal Completion
Authors: Haruhiko Sato and Sarah Winkler
Paper Information
| Title: | A Satisfiability Encoding of Dependency Pair Techniques for Maximal Completion |
| Authors: | Haruhiko Sato and Sarah Winkler |
| Proceedings: | WST 2014 Informal Proceedings |
| Editor: | Carsten Fuhs |
| Keywords: | dependency pair framework, Knuth-Bendix completion, maximal completion, SAT encoding |
| Abstract: | ABSTRACT. We present a general approach to encode termination in the dependency pair framework as a satisfiability problem, and include encodings of dependency graph and reduction pair processors. We use our encodings to increase the power of the completion tool Maxcomp. |
| Pages: | 5 |
| Talk: | Jul 18 11:15 |
| Paper: |  |