proof-automation
There are 12 repositories under proof-automation topic.
leanprover-community/mathlib3
Lean 3's obsolete mathematical components library: please use mathlib4
TOTBWF/refinery
⛏️ A refinement proof framework for haskell
uwplse/PUMPKIN-PATCH
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
wenkokke/AutoInAgda
Proof automation – for Agda, in Agda.
proof-tree-builder/proof-tree-builder.github.io
A web-based graphical proof assistant for LK and Hoare logic.
math-comp/algebra-tactics
Ring, field, lra, nra, and psatz tactics for Mathematical Components
math-comp/mczify
Micromega tactics for Mathematical Components
owings1/pytableaux
multi-logic proof generator
wenkokke/swillprover
a linear logic prover based on Naoyuki Tamura's llprover that works under SWI Prolog
dtumad/lean-crypto-formalization
Library for formalizing cryptography proofs in Lean 3 (Deprecated)
joe-lynch/ODPE
The Open Deduction Proof Editor allows proof theorists (or anyone) to deconstruction proofs step by step. It currently supports deep inference formalisms, namely Open Deduction and naturally the Calculus of Structures. The front end of the application is written in Java, while the back end is written in Maude. There is also an implementation of proof search both with and without proof variables.