Theory exploration for interactive theorem proving
Se ha publicado un artículo sobre automatización del razonamiento titulado Theory exploration for interactive theorem proving.
Su autora es Moa Johansson (de la Universidad Técnica Chalmers en Gotemburgo, Suecia).
Su resumen es
Theory exploration is an automated reasoning technique for discovering and proving interesting properties about some set of given functions, constants and datatypes. In this note we describe ongoing work on integrating the HipSpec theory exploration system with the interactive prover Isabelle. We believe that such an integration would be beneficial for several reasons. In an interactive proof attempt a natural application would be to allow the user to ask for some suggestions of new lemmas that might help the current proof development. Theory exploration may also be used to automatically generate and prove some basic lemmas as a first step in a new theory development. Furthermore, when the theory exploration system is used as a stand-alone system, it should output a checkable proofs, for instance for Isabelle, so that sessions can be saved for future use.
El trabajo se presentó el 22 de julio en el AI4FM 2013 (4th International Workshop on Artifical Intelligence for Formal Methods).