Knuth Bendix Orders

swMATH ID: 28584
Software Authors: Heiko Becker; Jasmin Christian Blanchette; Uwe Waldmann; Daniel Wand
Description: 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.
Homepage: https://www.isa-afp.org/entries/Lambda_Free_KBOs.html
Dependencies: Isabelle
Related Software: Isar; Isabelle/HOL; Nested Multisets; Lambda Free RPOs; Archive Formal Proofs; Sledgehammer; Abstract Completeness; Lifting; Transfer; CoLoR; HOCL; FOL_Harrison; Propositional Resolution; Incredible Proof Machine; Abstract Soundness; Verified Prover; Incompleteness Theorems; FOL Fitting; Paraconsistency; Superposition Calculus
Referenced in: 3 Publications

Referenced in 1 Serial

1 Journal of Automated Reasoning

Referencing Publications by Year