Sciweavers

Share
CADE
2015
Springer

Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion

4 years 3 months ago
Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion
Abstract. This paper describes two advancements of SAT-based KnuthBendix 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.
Haruhiko Sato, Sarah Winkler
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CADE
Authors Haruhiko Sato, Sarah Winkler
Comments (0)
books