Stream: Coq users

Topic: SMT and CIC


view this post on Zulip Guillaume Melquiond (Sep 08 2021 at 12:28):

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

view this post on Zulip Bas Spitters (Sep 08 2021 at 12:40):

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?

view this post on Zulip Chantal Keller (Sep 08 2021 at 15:49):

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

view this post on Zulip Bas Spitters (Sep 11 2021 at 10:03):

Thanks @Chantal Keller Is there any more information available about veriT or CVC5 support for v3 ?
Google was not very helpful.

view this post on Zulip Chantal Keller (Sep 14 2021 at 07:42):

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