activity
20232025
most citedCoqPyt: Proof Navigation in Python in the Era of LLMs

5 citations · 6 across the 3 of their papers we have counts for

collaborators
Showing cs.LOShow all

1 paper · 1 filter

cs.LO2023★ 1 cited

Using Counterexample Generation and Theory Exploration to Suggest Missing Hypotheses

Ruben Gamboa, Panagiotis Manolios, Eric Smith +1

Newcomers to ACL2 are sometimes surprised that ACL2 rejects formulas that they believe should be theorems, such as (REVERSE (REVERSE X)) = X. Experienced ACL2 users will recognize…