Knuth Bendix Orders

MaRDI QIDQ40298swMATHFDO

Official website https://www.isa-afp.org/entries/Lambda_Free_KBOs.html

Cited in

(13)

• Formalization of the resolution calculus for first-order logic
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)
• HOCL
• theoremprover-museum
• Abstract Completeness
• Deriving class
• Abstract Soundness
• Incompleteness Theorems
• Markov Models
• Lambda Free RPOs
• Incredible Proof Machine
• Nested Multisets
• Foundational (co)datatypes and (co)recursion for higher-order logic

This page was built for software: Knuth Bendix Orders