克努特-本迪克斯完备化

克努特-本迪克斯完备化（Knuth-Bendix completion），计算机科学技术名词，由克努特（Knuth）和本迪克斯（Bendix）提出的，将一组等式转换为一个有限终止的具有合流性的项重写系统的方法。是将等式推理问题转化为重写系统中的判定问题的关键步骤。