I was curious about ATPs within the logic of Coq itself (e.g. that do induction sort of smartly). Do people know of tools better than sauto, coqhammer? (note SMTCoqhammer also uses FOL solvers/atps so I don’t think that’s quite what I’m curious about) I had a similar discussion (that sort of ended)…

What is a hammer/atp within the logic of coq that does things like induction in coq?

brando90 March 24, 2022, 8:55pm 2

Topic		Replies	Views
Inductive proof automation Using Rocq	6	1065	March 25, 2022
CoqHammer 1.2.1 for Coq 8.10 and 8.11 Announcements	0	1048	June 7, 2020
What does it mean that Isabelle has better automation than Coq? Miscellaneous	15	4507	March 25, 2021
Best formulation for inductive propositions? Using Rocq	4	584	April 21, 2020
CoqHammer 1.1.1 for Coq 8.9 Announcements	14	1413	February 23, 2020