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

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

November 12, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

Topics

Session Lambda_Free_KBOs

Depends on

Cite

× 
@article{Lambda_Free_KBOs-AFP,
  author  = {Heiko Becker and Jasmin Christian Blanchette and Uwe Waldmann and Daniel Wand},
  title   = {Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2016},
  note    = {\url{https://isa-afp.org/entries/Lambda_Free_KBOs.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: