The language of [real closed fields](https://en.wikipedia.org/wiki/Real_closed_field) $\mathcal{L}_\text{rcf}$ 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*.

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.