The language of ordered rings is a first-order language with operators for $+$, $-$, and $\cdot$, constants for $0$ and $1$, and relations for $<$, $=$ and $>$.

To decide whether such a statement can be classically proven (in, say, ZFC) for the real numbers is easy: 

- Use [Cylindrical algebraic decomposition (CAD)](https://en.wikipedia.org/wiki/Cylindrical_algebraic_decomposition) to compute if it is true or not. 
- If yes, then it is classically provable. If not, then it is not classically provable.

But now consider the problem of deciding whether such a statement is provable about the (Dedekind) reals in, say, [neutral constructive mathematics](https://ncatlab.org/nlab/show/neutral+constructive+mathematics). The above algorithm no longer works on the input $\forall x. \forall y. (x = y) \lor \lnot (x = y)$. The algorithm above will state that it is provable since CAD says it is true, but it is in fact not constructively provable since it is the [analytic WLPO](https://ncatlab.org/nlab/show/principle+of+omniscience#analytic), which is a constructive taboo. A correct algorithm would declare this statement to be *not provable*. (See [aws's comment](https://mathoverflow.net/questions/468849/is-it-decidable-whether-a-statement-about-reals-in-mathcall-textrcf-1#comment1217664_468849) for a description of this set of sentences using topos theory.)

So my question is **does such an algorithm exist?**

I have a feeling though that this should still be computable. Constructive algebra is basically just "fuzzy" classical algebra.

Note though that for first-order *arithmetic*, the answer is no. A $\Sigma^0_1$ statement is provable iff it is true (whether considering classical or constructive proofs), and deciding this would let you solve the halting problem.

Also note that, constructively, formulas do not in general have a [Prenex normal form](https://en.wikipedia.org/wiki/Prenex_normal_form).