Knuth Bendix Orders

Lambda Free KBOs: Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms. 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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 3 articles )

Showing results 1 to 3 of 3.
Sorted by year (citations)

  1. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
  2. Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy: Foundational (co)datatypes and (co)recursion for higher-order logic (2017)
  3. Blanchette, Jasmin Christian; Fleury, Mathias; Traytel, Dmitriy: Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL (2017)