Itauto

gitlab.inria.frsite

SMT-like tactics for combined propositional reasoning about function symbols, constructors, and arithmetic.

from

Coq

added

2026-10-10

likes

0

similar

1. ▲

   Fiat github.com

   Mostly automated synthesis of correct-by-construction programs.

   tool link ↗
   
2. ▲

   AAC Tactics github.com

   Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator.

   tool link ↗
   
3. ▲

   Nonanti/mathcore github.com

   Symbolic mathematics library with CAS capabilities. Supports differentiation, integration, equation solving, and arbitrary precision arithmetic

   tool topic math link ↗
   
4. ▲

   SMTCoq github.com

   Tool that checks proof witnesses coming from external SAT and SMT solvers.

   tool topic math link ↗
   
5. ▲

   Trakt github.com

   Generic goal preprocessing tool for proof automation tactics.

   tool topic math link ↗
   
6. ▲

   Ltac2 coq.inria.fr

   Experimental typed tactic language similar to Coq's classic Ltac language.

   site link ↗
   site

Coq › Projects > Plugins: “SMT-like tactics for combined propositional reasoning about function symbols, constructors, and arithmetic.”