Reseña: The Boyer-Moore waterfall model revisited

Uno de los problemas fundamentales dentro del campo del razonamiento automático es la automatización de la inducción. El método fundamental para automatizar la inducción es el de la cascada presentado por Robert S. Boyer y J S. Moore en su libro A Computational Logic e integrado en sus sistemas Nqthm y ACL2.

En el trabajo The Boyer-Moore waterfall model revisited se presenta una implementación del modelo de Boyer-Moore en el sistema HOL Light.

Sus autores son Petros Papapanagiotou y Jacques Fleuriot (de la Universidad de Edimburgo).

Su resumen es

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. 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 are also discussed. Finally, we present a thorough evaluation of the approach using a set of 150 theorems, and discuss the effectiveness of our additions and relevance of the model in light of our results.

El trabajo es una extensión de la Tesis de Máster de Petros Papapanagiotou titulada On the automation of inductive proofs in HOL
Light y sirve como lectura complementaria en el curso Automated Reasoning (2012-13) de la Universidad de Edimburgo. Las transparencias del correspondiente tema del curso son Inductive theorem proving.