Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms

Heiko Becker 📧, Jasmin Christian Blanchette 📧, Uwe Waldmann 📧 and Daniel Wand 📧

November 12, 2016

Abstract

This Isabelle/HOL formalization defines Knuth–Bendix orders for higher-order terms without lambda-abstraction and proves many useful properties about them. The main order fully coincides with the standard transfinite KBO with subterm coefficients on first-order terms. It appears promising as the basis of a higher-order superposition calculus.
BSD License

Topics

Theories of Lambda_Free_KBOs