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 that the theorem only holds for intended values of X, and given ACL2's total logic, there are many counterexamples for which this formula is simply not true. 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. In this case, for example, DrLA may suggest that X needs to be either a TRUE-LIST or a STRING. The suggestions are discovered using the ideas of theory exploration and subsumption from automated theorem proving.

翻译：ACL2的新手有时会感到惊讶，因为ACL2会拒绝他们本应视为定理的公式，例如(REVERSE (REVERSE X)) = X。有经验的ACL2用户会认识到，该定理仅对X的预期值成立，而在ACL2的全量逻辑中，存在许多反例使得该公式不成立。反例生成（cgen）技术通过向用户提供该公式的若干反例（及见证例）来辅助理解，例如告知用户当X等于10时该假设定理不成立。本文描述了一个名为DrLA的工具，该工具通过建议使定理成立所需的额外假设来进一步推进。以该案例为例，DrLA可能建议X需为TRUE-LIST或STRING类型。这些建议通过自动定理证明中的理论探索与子概念包含思想发现。