22Automation, Solvers & Tactics
22 entries
Tactics and solver integrations that are useful when proving properties of programs.
- grindBuilt-in SMT-style tactic combining congruence closure, E-matching and arithmetic.
- bv_decideBuilt-in bit-blasting decision procedure for
BitVecgoals, backed by a verified SAT proof checker (LeanSAT).leanprover/lean4 - AesopWhite-box, rule-based proof search.leanprover-community/aesop
- lean-smtDischarge goals to SMT solvers with proof reconstruction.ufmg-smite/lean-smt
- lean-cvc5FFI bindings to the cvc5 SMT solver.abdoo8080/lean-cvc5
- lean-autoInterface between Lean and automated theorem provers.leanprover-community/lean-auto
- DuperSuperposition-based automatic prover.leanprover-community/duper
- LeanHammerHammer combining premise selection, ATPs and proof reconstruction.JOSHCLUNE/LeanHammer
- CanonicalExhaustive term search in dependent type theory.chasenorman/CanonicalLean
- LeanwuzlaConnects
bv_decideto SMT-LIB.hargoniX/Leanwuzla - BlasterSMT-based reasoning core.input-output-hk/Lean-blaster
- eggEquality saturation tactic based on egg (deprecated).marcusrossel/lean-egg
- OptiSatVerified equality saturation engine.lambdaclass/truth_research
- SaturnSAT solvers with proofs.siddhartha-gadgil/Saturn
- trestleSAT utilities: encodings, solver APIs, and file format parsers and printers.FormalSAT/trestle
- CLeanGoBindings and DSL for the Clingo answer set programming solver.kiranandcode/cleango
- waterfallACL2-style proof search for inductive goals.samth/waterfall
- sosSum-of-squares tactic for nonlinear real arithmetic.leanprover/sos
- SmtLibDslTyped SMT-LIB DSL with backends for Z3, cvc5, Kissat and CaDiCaL.palladin/SmtLibDsl
- cpsatBindings to the OR-Tools CP-SAT constraint solver.paulbutcher/leancpsat
- deriving such thatPort of Rocq's program derivation tactic.kiranandcode/deriving-such-that
- BetterFindExtended
#findfor searching declarations by pattern, closer to Rocq'sSearch.kiranandcode/BetterFind.lean