Improving Eliminate-Irrelevance for ACL2
Matt Kaufmann (joint work with J Moore)
October 14, 2016
ACL2 Seminar

Abstract:

One of the ``waterfall'' processes used by ACL2 (and its predecessor,
NQTHM) is the ``eliminate-irrelevance'' process.  This process
can heuristically delete information from a goal before entering a
sub-induction.  This talk will:

o review the ACL2 waterfall and its eliminate-irrelevance clause-processor,

o present a recent change in its heuristics, and

o remark on considerations when designing and implementing that change.