In particular, generalized chess (chess on an NxN board, with an appropriate number of pieces) is EXPTIME-complete: for any instance of a binary decision problem in EXPTIME, you can reduce it to a generalized chess board position such that the White (Black) player can win iff the answer to the instance of the decision problem is Yes.
The complexity of theorem proving depends on the formal system. There are some logics where theorem proving is PSPACE-complete, which is contained in EXPTIME. Other interesting logics are undecidable, thus you can’t reduce them to a game of generalized chess, although semidecidable logics can be reduced to other, more complex games.
Yes.
In particular, generalized chess (chess on an NxN board, with an appropriate number of pieces) is EXPTIME-complete: for any instance of a binary decision problem in EXPTIME, you can reduce it to a generalized chess board position such that the White (Black) player can win iff the answer to the instance of the decision problem is Yes.
The complexity of theorem proving depends on the formal system. There are some logics where theorem proving is PSPACE-complete, which is contained in EXPTIME.
Other interesting logics are undecidable, thus you can’t reduce them to a game of generalized chess, although semidecidable logics can be reduced to other, more complex games.