Knuth-Bendix completion

This page provides an online implementation of Knuth-Bendix completion algorithm.

Theory

Symbols

Please enter function names (lowercase letters only) with arities separated by commas. First symbols have higher weight (we currently use lexicographic path order).

i:1, m:2, e:0

Rules

Please enter the rules.

m(m(x,y),z) = m(x,m(y,z)) m(i(x),x) = e m(e,x) = x

Results

Knuth-Bendix completion

Squier completion