ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.
Apache License 2.0
84 stars 18 forks source link

Support Vampire #25

Closed Vtec234 closed 2 years ago

Vtec234 commented 2 years ago

This is low priority and afaik there is no plan to reconstruct Vampire proofs, but it should not be too hard just to get the SMT-LIB out to Vampire and print sat/unsat, maybe some counterexamples.