🚀 go-pugleaf

I'm looking at some problems that involve producing constructive
proofs for Presburger-like formulas, except over the reals, not
over integers. 

Questions:

  * Is there a better name for this class of formulas other than 
	"Presburger over the reals"

  * Any pointers to algorithms or upper bounds for either verifying
	such formulas or producing constructive proofs?

We actually don't need full Presburger over the reals, but we do need
to deal with formulas that have an arbitrary number of alternating 
quantifiers. If there are any methods that work for subsets of Presburger 
that allow an arbitrary number of alternating quantifiers, that would be 
of interest as well.

  Thanks,
    Bill Pugh