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."

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 ( nor veriT (, but I think that the experimental versions with parts of HOL actually support more than SMT-LIB 2, which led to v3

Last updated: Jun 24 2024 at 12:02 UTC