A transfinite Knuth-Bendix order for lambda-free higher-order terms
From MaRDI portal
Publication:2405268
DOI10.1007/978-3-319-63046-5_27zbMath1496.03037MaRDI 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
03B10: Classical first-order logic
03B35: Mechanization of proofs and logical operations
03B16: Higher-order logic
Related Items
Unnamed Item, Unnamed Item, The CADE-26 automated theorem proving system competition – CASC-26, Superposition with lambdas, Formalization of the resolution calculus for first-order logic, A Knuth-Bendix-like ordering for orienting combinator equations, Set of support, demodulation, paramodulation: a historical perspective, Certified equational reasoning via ordered completion