Maximal Completion

Given an equational system, completion procedures compute an equivalent and complete (terminating and confluent) term rewrite system. We present a very simple and efficient completion procedure, which is based on MaxSAT solving. Experiments show that the procedure is comparable to recent powerful completion tools. 1998 ACM Subject Classification F.4.2 Grammars and Other Rewriting Systems Keywords and phrases Term Rewriting, Knuth-Bendix Completion, Multi-completion Digital Object Identifier 10.4230/LIPIcs.xxx.yyy.p Category System Description

• Type: Journal
• Year: 2011
• Where: RTA
• Authors: Dominik Klein, Nao Hirokawa
• Keywords: Completion Procedures, Rewrite System, Rewriting Systems, RTA 2011, Theoretical Computer Science