A kernel using inference rules in order to compute the three of proves.

Project for CSEEE6863_001_2016_3 - FORMAL VERIF HW SW SYSTEMS

An imperative language, logic parser and simple theorem prover designed to function via a CLI.

Toy theorem prover based on the calculus of constructions

A simple first order logic theorem prover using tableaux

A logic-based library for correct-by-construction process modelling and composition.

HOL-Light Library for Modal Systems

Chad Brown’s Egal, a theorem prover for higher-order Tarski–Grothendieck set theory

A prototypical proof checker and programming language based on illative combinatory logic

Modification to Coq to record intermediate proof states encountered during a proof

Code resources from John Harrison's "Handbook of Practical Logic and Automated Reasoning"

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

A Seamless, Interactive Tactic Learner and Prover for Coq

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.