2
$\begingroup$

Euclidean geometry is complete, so the problem of determining whether a statement $A$ is provable is computable. Do we know its time complexity?

$\endgroup$
3
$\begingroup$

It is common to prove the decidability of first-order Euclidean geometry by encoding the language of Euclidean geometry into the language of real closed fields and then showing that the latter is decidable. A singly-exponential space upper bound on deciding the first-order theory of real closed fields was proven in Ben-Or, Kozen, and Reif (1986). This implies a doubly-exponential time upper bound.

I believe this is the best known complexity for the decision problem for general first-order sentences in the language of real closed fields. However, I am not sure whether deciding real closed fields is equivalent (bidirectionally) to deciding Euclidean geometry, since a typical encoding of (say) the language of Tarski's axioms into the language of real closed fields only uses a small subset of the possible polynomials. So maybe first-order Euclidean geometry can be decided with lower complexity than this. It is at least PSPACE-hard, since TQBF is easily encoded into first-order Euclidean geometry.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.