Abstract: We present an algorithm to help converting expressions having non-negative quantities (like distances) in Euclidean geometry theorems to be usable in a complex algebraic geometry prover. The algorithm helps in refining the output of an existing prover, therefore it supports immediate deployment in high level prover systems. We prove that the algorithm may take doubly exponential time to produce the output in polynomial form, but in many cases it is still computable and useful.

Autoría

Descargar referencia