I had completely missed this announcement, so perhaps I am not the only one: "The underlying logic of SMT-LIB 3 has many elements of the Calculus of Inductive Constructions (CIC) used by proof assistants like Coq and Lean, with the main restriction of allowing only rank-1 polymorphism (actually, let-polymorphism) and not having a Prop-like kind for (constructive) propositions." http://smtlib.cs.uiowa.edu/version3.shtml

Exciting! Is there support for SMT-LIB3 already? Is any of the other tools (F*,lean,PVS,HOLs ) using it?

What does that mean for SMT-Coq, @Chantal Keller ?

Is there a project under way to verify this parts of LIB3? I guess there may be a translation to a simpler logic?

Hi @Bas Spitters

It allows SMT solvers to push towards higher-order (which is already the case for veriT and CVC5), which complements wells SMTCoq/Sniper

Thanks @Chantal Keller Is there any more information available about veriT or CVC5 support for v3 ?

Google was not very helpful.

According to the documentation, not yet for CVC5 (https://cvc5.github.io/docs/languages.html) nor veriT (https://verit.loria.fr), but I think that the experimental versions with parts of HOL actually support more than SMT-LIB 2, which led to v3

Last updated: Jan 29 2023 at 05:03 UTC