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
CoqHammer 1.1.1 for Coq 8.9 Announcements	14	1388	February 23, 2020
CoqHammer 1.2.1 for Coq 8.10 and 8.11 Announcements	0	1029	June 7, 2020
Thinking of using hammer/automation to guide the order of proving lemmas Using Coq	0	443	October 24, 2021
Machine learning and hammers for Coq Using Coq	45	7036	June 6, 2022
What does it mean that Isabelle has better automation than Coq? Miscellaneous	15	4360	March 25, 2021