A transfinite Knuth-Bendix order for lambda-free higher-order terms

DOI10.1007/978-3-319-63046-5_27zbMath1496.03037OpenAlexW2735771386MaRDI QIDQ2405268

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

Publication date: 22 September 2017

Full work available at URL: https://doi.org/10.1007/978-3-319-63046-5_27

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Higher-order logic (03B16)

Related Items (8)

Formalization of the resolution calculus for first-order logic ⋮ Unnamed Item ⋮ The CADE-26 automated theorem proving system competition – CASC-26 ⋮ Superposition with lambdas ⋮ Unnamed Item ⋮ Certified equational reasoning via ordered completion ⋮ A Knuth-Bendix-like ordering for orienting combinator equations ⋮ Set of support, demodulation, paramodulation: a historical perspective

This page was built for publication: A transfinite Knuth-Bendix order for lambda-free higher-order terms