“Newcomers to ACL2 are sometimes surprised that ACL2 rejects formulas that they believe should be theorems. … Counterexample generation (cgen) is a technique that helps by giving the user a number of counterexamples (and also witnesses) to the formula, e.g., letting the user know that the intended theorem is false when X is equal to 10. In this paper we describe a tool called DrLA that goes further by suggesting additional hypotheses that will make the theorem true.”

Find the paper and full list of authors at ArXiv.