Skip to Main content Skip to Navigation
Conference papers

Square root and division elimination in PVS

Abstract : In this paper we present a new strategy for PVS that imple- ments a square root and division elimination in order to use automatic arithmetic strategies that were not able to deal with these operations in the ﰁrst 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 reﰂection and symbolic com- putation we are able to automatically transform expressions into division and square root free ones before using these decision procedures.
Document type :
Conference papers
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download

https://hal.inria.fr/hal-00924359
Contributor : Pierre Neron <>
Submitted on : Monday, January 6, 2014 - 4:44:02 PM
Last modification on : Friday, May 25, 2018 - 12:02:06 PM
Long-term archiving on: : Thursday, April 10, 2014 - 5:25:11 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Pierre Neron. Square root and division elimination in PVS. ITP - 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.457-462, ⟨10.1007/978-3-642-39634-2_33⟩. ⟨hal-00924359⟩

Share

Metrics

Record views

419

Files downloads

387