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
• Foundational (co)datatypes and (co)recursion for higher-order logic
• HOCL
• theoremprover-museum
• Markov Models
• Abstract Completeness
• Deriving class
• Incompleteness Theorems
• Lambda Free RPOs
• Abstract Soundness
• Incredible Proof Machine
• Nested Multisets
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)

This page was built for software: Knuth Bendix Orders