Zulip Chat Archive

Stream: general

Topic: SMT Integration


view this post on Zulip Wojciech Nawrocki (Jan 25 2019 at 19:47):

What's the status of integrating SMT solvers with Lean? There are some references to it in the documentation, (e.g. https://leanprover.github.io/reference/tactics.html#the-smt-state) but all are empty. It would be nice to have some automatic solving.

view this post on Zulip Simon Hudon (Jan 25 2019 at 19:51):

The smt tactics are not very much used. I just started this week looking at wrapping veriT into Lean tactics and as far as I know, that's the only such work going on in Lean

view this post on Zulip Simon Hudon (Jan 25 2019 at 19:53):

Maybe Jasmin Blanchette's team has something related in the works but I don't know any details.

view this post on Zulip Simon Cruanes (Jan 25 2019 at 20:06):

What fragment do you plan to encode into SMTLIB, and how?

view this post on Zulip Simon Hudon (Jan 25 2019 at 20:07):

Right now, I haven't settled on a fragment, I'm just looking at building the interface for now.

view this post on Zulip Simon Cruanes (Jan 25 2019 at 20:20):

I suppose the closest existing thing is SMTCoq, especially regarding proof reconstruction, but that's a lot of work

view this post on Zulip Simon Hudon (Jan 25 2019 at 21:35):

I'm looking at SMTCoq and Blanchette's work for Isabelle. I think it's probably work worth doing.

view this post on Zulip Simon Hudon (Jan 25 2019 at 21:36):

I'm building proof obligation generators in Lean and smt solvers are useful to discharge those

view this post on Zulip Simon Cruanes (Jan 25 2019 at 21:36):

I know Jasmin has been talking about an independent Sledgehammer-like tool that could be shared between proof assistants, but that'd be even more work…
If you do it directly in Lean it'll be easier to reconstruct proofs.

view this post on Zulip Simon Hudon (Jan 25 2019 at 21:44):

That's my opinion too. I think whereas Jasmin's project is more general and long term, mine is to address an immediate need and I'm ok with doing it imperfectly at first

view this post on Zulip Gabriel Ebner (Jan 25 2019 at 21:49):

There is https://github.com/leanprover/smt2_interface from quite some time ago, but it doesn't generate proofs.

view this post on Zulip Simon Hudon (Jan 25 2019 at 21:57):

Thanks for the link! I was trying to find it again but didn't look in the most obvious place


Last updated: May 17 2021 at 22:15 UTC