2025/10/21 by Alexander Bentkamp, Bentkamp, Alexander, Jasmin Christian Blanchette +3
Computer Science · #Computability, Logic, AI Algorithms #F.4.1 #FOS: Computer and information sciences #Formal Methods in Verification #I.2.3 #Logic in Computer Science (cs.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2510.18452
openalex publication_date 2025/10/21 · openalex created_date 2025/10/24 · openalex updated_date 2026/07/28
We introduce λKBO and λLPO, two variants of the Knuth-Bendix order (KBO) and the lexicographic path order (LPO) designed for use with the λ-superposition calculus. We establish the desired properties via encodings into the familiar first-order KBO and LPO.