A Sequent Calculus Prover for First-Order Logic with Functions by Asta Halkjær From and Frederik Krogsdal Jacobsen Jan 31
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
First-Order Logic According to Harrison by Alexander Birch Jensen, Anders Schlichtkrull and Jørgen Villadsen Jan 01
Sound and Complete Sort Encodings for First-Order Logic by Jasmin Christian Blanchette and Andrei Popescu Jun 27
A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic by Tom Ridge Sep 28