The Boyer-Moore Waterfall Model Revisited

Understand

In this paper, we investigate the potential of the Boyer-Moore waterfall model for the automation of inductive proofs within a modern proof assistant.

• We analyze the basic concepts and methodology underlying this 30-year-old model and implement a new, fully integrated tool in the theorem prover HOL Light that can be invoked as a tactic.
• We also describe several extensions and enhancements to the model.
• These include the integration of existing HOL Light proof procedures and the addition of state-of-the-art generalization techniques into the waterfall.