prover

An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

Cicada Language (solo version)

An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logtk, a supporting library for manipulating terms, formulas, clauses, etc.

Zero-Knowledge Proofs "for (not too much 😉 ) dummies"

Resolution theorem proving for predicate logic in pure Python.

Cicada Language

[research] A modular SMT solver in OCaml, based on mcSAT

A modular library for CDCL(T) SMT solvers, with [wip] proof generation.

Python Symbolic Information Theoretic Inequality Prover

Geometer's Sandbox project repo

[frozen] Scheduling and running jobs on a shared computer, then analyse their output

Haskell interface to automated theorem provers

Python-based theorem prover

An implementation of a propositional logic resolution prover in Rust.

A neural parser for typelogical grammars based on Sinkhorn networks and Linear Logic Proof Nets.

Prover Engine

A graph based prover.

State of project before the move from Ant to Gradle

A experimental prover written in Common Lisp, based on clause resolution and Knuth-Bendix completion algorithm.