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