|
|
|---|
|
|
|
|---|
How ACL2 selects induction schemes
This topic is for those curious about induction heuristics in ACL2. It is not necessary to understand those heuristics to be able to use ACL2 successfully.
ACL2's heuristics for generating an induction scheme for a conjecture are very similar to Nqthm's and can trace their roots all the way back to the Edinburgh Pure Lisp Theorem Prover, the first prover to support induction in a general setting.
For a detailed description of how ACL2 generates induction schemes see ``ACL2 Induction Heuristics.'' That paper is intended for a general audience familiar with induction but not necessarily familiar with theorem provers or ACL2. However, it can also serve as a guided tour through that part of the ACL2 source code that creates and selects induction schemes.