Real Automation in the Field
Cesar A. Munoz, Micaela Mayero, Dennis Meyer Bushnell · NASA STI Repository (National Aeronautics and Space Administration)
We provide a package of strategies for automation of non-linear arithmetic in PVS. In particular, we describe a simplication procedure for the field of real numbers and a strategy for cancellation of common terms.