Reseña: Square root and division elimination in PVS
Se ha publicado un artículo de automatización del razonamiento en PVS titulado Square root and division elimination in PVS.
Su autor es Pierre Neron (del INRIA en Paris – Rocquencourt).
El trabajo se presentará en julio en el ITP 2013 (4th Conference on Interactive Theorem Proving).
Su resumen es
In this paper we present a new strategy for PVS that implements a square root and division elimination in order to use automatic arithmetic strategies that were not able to deal with these operations in a first place. This strategy relies on a PVS formalization of the square root and division elimination and deep embedding of PVS expressions inside PVS. Therefore using computational reflection and symbolic computation we are able to automatically transform expressions into division and square root free ones before using these decisions procedures.
El código de las correspondientes teorías PVS se encuentra aquí.