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
Abstract Soundness by Jasmin Christian Blanchette π§, Andrei Popescu π and Dmitriy Traytel π Feb 10
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