Logic/General Logic/Mechanization of Proofs

A Naive Prover for First-Order Logic
by Asta Halkjær From

A Sequent Calculus Prover for First-Order Logic with Functions
by Asta Halkjær From and Frederik Krogsdal Jacobsen

Extensions to the Comprehensive Framework for Saturation Theorem Proving
by Jasmin Christian Blanchette and Sophie Tourret

A Comprehensive Framework for Saturation Theorem Proving
by Sophie Tourret

A General Theory of Syntax with Bindings
by Lorenzo Gheri and Andrei Popescu

A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
by Anders Schlichtkrull, Jasmin Christian Blanchette and Dmitriy Traytel

Formalization of Bachmair and Ganzinger's Ordered Resolution Prover
by Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann

First-Order Logic According to Harrison
by Alexander Birch Jensen, Anders Schlichtkrull and Jørgen Villadsen

The Resolution Calculus for First-Order Logic
by Anders Schlichtkrull

Propositional Resolution and Prime Implicates Generation
by Nicolas Peltier

Boolean Expression Checkers
by Tobias Nipkow

Sound and Complete Sort Encodings for First-Order Logic
by Jasmin Christian Blanchette and Andrei Popescu

A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic
by Tom Ridge