Reseña: Automating inductive proofs using theory exploration
Se ha publicado un artículo de razonamiento automático sobre programas funcionales en Haskell titulado Automating inductive proofs using theory exploration.
Sus autores son Koen Claessens, Moa Johansson, Dan Rosén y Nicholas Smallbone (de la Universidad de Chalmers).
El trabajo se presentará en el CADE-24 (24th International Conference on Automated Deduction).
Su resumen es
HipSpec is a system for automatically deriving and proving properties about functional programs. It uses a novel approach, combining theory exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems about the available recursive functions of a program. These equational properties make up an algebraic specification for the program and can in addition be used as a background theory for proving additional user-stated properties. Experimental results are encouraging: HipSpec compares favourably to other inductive theorem provers and theory exploration systems.
El código de HipSpec se encuentra en aquí. Los experimentos con HipSpec se encuentran aquí.