We develop a probabilistic test for the vanishing of radical expressions, that is, expressions involving the four rational operations (+,−,×,÷) and square root extraction. This extends the well-known
Schwartz’s probabilistic test for the vanishing of polynomials. The probabilistic test forms the basis of a new theorem prover
for conjectures about ruler & compass constructions. Our implementation uses the Core Library which can perform exact comparison
for radical expressions. Some experimental results are presented.
This work was performed while Daniela Tulone was at NYU.
This work is supported in part by NSF Grant #CCR 9402464.
Acknowledgments Daniela Tulone would like to acknowledge Alfredo Ferro and Pina Carrà for their advice and discussions in the initial stages
of this project.