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.

• Type: Journal
• Year: 2015
• Where: CADE
• Authors: Haruhiko Sato, Sarah Winkler
• Keywords: CADE 2015, Logical Reasoning