Boyer-Moore

In this project, we investigate the potential of the Boyer-Moore waterfall model for the automation of inductive proofs within a modern proof assistant. Based on the concepts and methodology underlying this 40-year-old model, we have implemented a new, fully integrated tool in the theorem prover HOL Light that can be invoked as a tactic.

We have also included 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. Various features, such as proof feedback and heuristics dealing with non-termination, that are needed to make this automated tool useful within our interactive setting have also been implemented.

We have evaluated this system using a set of 150 theorems, and demonstrated its effectiveness as a tool for automated inductive proofs within an interactive environment.

The library has been released in the main HOL Light repository.