Formalization of Bachmair and Ganzinger's Ordered Resolution Prover by Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann Jan 18
Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms by Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand Nov 12
Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms by Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand Sep 23