Zulip Chat Archive

Stream: general

Topic: proof assistant automation tactics

Julian Berman (Jun 10 2022 at 16:21):

Is there a good resource for an overview of the "classes" of automation that exist in proof assistants? E.g. often folks ask things like "does Lean have sledgehammer", or "auto", or "a SAT solver", or a groebner basis tactic or etc. Presumably there are both mathematics-specific classes of tactic automation as well as pure CS ones, but curious to hear about whichever or both.

So -- how are pieces of automation (perhaps ones Lean indeed has, like simp, cc, etc.) categorized, and what's a good high level overview of the different uses of them?

Julian Berman (Jun 10 2022 at 16:23):

(Something hopefully more efficient than "read the tactics docs for Lean, Isabelle, Agda & Coq" :D)

Jason Rute (Jun 10 2022 at 18:18):

This might be a good question for the proof assistant stack exchange also.

Jason Rute (Jun 10 2022 at 19:17):

Also, there is always John Harrison’s massive tomb: Handbook of Practical Logic and Automated Reasoning

Jason Rute (Jun 10 2022 at 19:17):


Eric Wieser (Jun 10 2022 at 21:20):

Do you mean "tome"?

Last updated: Aug 03 2023 at 10:10 UTC