Elementary recursive quantifier elimination based on Thom encoding and sign determination

Perrucci, Daniel Roberto; Roy, Marie Françoise

info:eu-repo/semantics/article

Fecha

2017-08

Registro en:

Perrucci, Daniel Roberto; Roy, Marie Françoise; Elementary recursive quantifier elimination based on Thom encoding and sign determination; Elsevier Science; Annals Of Pure And Applied Logic; 168; 8; 8-2017; 1588-1604

0168-0072

http://hdl.handle.net/11336/159267

CONICET Digital

CONICET

https://repositorioslatinoamericanos.uchile.cl/handle/2250/4389351

Autor

Perrucci, Daniel Roberto

Roy, Marie Françoise

Institución

Consejo Nacional de Investigaciones Científicas y Tecnológicas (Argentina)

Resumen

We describe a new quantifier elimination algorithm for real closed fields based onThom encoding and sign determination. The complexity of this algorithm is elemen-tary recursive and its proof of correctness is completely algebraic. In particular, thenotion of connected components of semialgebraic sets is not used.

Materias

QUANTIFIER ELIMINATION

SIGN DETERMINATION

THOM ENCODING

Mostrar el registro completo del ítem