Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms

MaRDI QIDQ7361192FDO

Authors Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand

Publication date 23 September 2016

Cited in

(6)

• A Comprehensive Framework for Saturation Theorem Proving
• Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
• Substitutions for Lambda-Free Higher-Order Terms
• Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms
• A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
• An Algebra for Higher-Order Terms

This page was built for software: Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms