Square Root and Division Elimination in PVS
| Autor: | Pierre Neron |
|---|---|
| Přispěvatelé: | Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Sandrine Blazy and Christine Paulin-Mohring and David Pichardie |
| Rok vydání: | 2013 |
| Předmět: |
0102 computer and information sciences
02 engineering and technology Computational reflection Division (mathematics) Symbolic computation 01 natural sciences Cylindrical algebraic decomposition TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Strategy language [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] Square root 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering Embedding 020201 artificial intelligence & image processing Arithmetic Algorithm Mathematics |
| Zdroj: | Interactive Theorem Proving ISBN: 9783642396335 ITP ITP-4th Conference on Interactive Theorem Proving ITP-4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.457-462, ⟨10.1007/978-3-642-39634-2_33⟩ |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|