A practical (and solvable in practical cases!) EXPTIME-complete problem is type inference (or even typability) in the ML type system (that is Hindley–Milner extended with let-polymorphism) or in Trevor Jim’s much nicer System P₂ (equivalently rank-2 intersection types; a fortiori his System P; no, I’m not going to stop shilling System P, it’s too neat to not have a language built upon it at least once).
Interesting decidable problems with even more insane complexity include provability in Presburger arithmetic (the one where you’re forbidden from multiplying variables together, so avoid the undecidability of Peano) and over the reals (with addition and multiplication only).
Interesting decidable problems with even more insane complexity include provability in Presburger arithmetic (the one where you’re forbidden from multiplying variables together, so avoid the undecidability of Peano) and over the reals (with addition and multiplication only).