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