An Introduction to Knuth Bendix Completion

In this series of videos, I will go through the paper by A. J. Dick in 1991 on “An Introduction to Knuth-Bendix Completion”. This paper aims to provide an informal and intuitive introduction to many of the concepts essential to a clear understanding of Knuth-Bendix Completion.

• Slides with animation (PPT format)
• Slides without animation (PDF format)

Part 1: Introduction

Part 2: Order of Complexity

Part 3: Superposition of Critical Term

Part 4: Confluence of Rewrite Rules

Part 5: KBC Algorithm