Extensions to the Comprehensive Framework for Saturation Theorem Proving by Jasmin Christian Blanchette 🌐 and Sophie Tourret 🌐 Aug 25
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover by Anders Schlichtkrull 🌐, Jasmin Christian Blanchette 📧 and Dmitriy Traytel 🌐 Nov 23
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover by Anders Schlichtkrull 🌐, Jasmin Christian Blanchette 📧, Dmitriy Traytel 🌐 and Uwe Waldmann 📧 Jan 18
Operations on Bounded Natural Functors by Jasmin Christian Blanchette 📧, Andrei Popescu 🌐 and Dmitriy Traytel 🌐 Dec 19
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals by Jasmin Christian Blanchette 📧, Mathias Fleury 📧 and Dmitriy Traytel 🌐 Nov 12
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
Abstract Completeness by Jasmin Christian Blanchette 🌐, Andrei Popescu 🌐 and Dmitriy Traytel 🌐 Apr 16
Sound and Complete Sort Encodings for First-Order Logic by Jasmin Christian Blanchette 🌐 and Andrei Popescu 🌐 Jun 27