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
Jasmin Christian Blanchette, Uwe Waldmann, Heiko Becker, Daniel Wand
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
