Topic: SMT Integration
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.
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
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.
Simon Cruanes (Jan 25 2019 at 20:06):
What fragment do you plan to encode into SMTLIB, and how?
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.
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
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.
Simon Hudon (Jan 25 2019 at 21:36):
I'm building proof obligation generators in Lean and smt solvers are useful to discharge those
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.
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
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.
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