# A language that is not even context-sensitive?

Is there a language actually in use that can't be recognized by a linear bounded automaton? I only know of ones that don't have a practical use, like "the set of pairs of equivalent regular expressions with exponentiation" (Wikipedia). Or would any such language be too slow to recognize to be useful?

-
In use by whom? For what? Would "English" count? –  Qiaochu Yuan Feb 25 '12 at 22:37
Does something PSPACE-complete count as useful? Because those certainly can't. –  Harry Altman Feb 25 '12 at 22:48
Automated proof checkers are computer programs that recognize the language of all valid proofs in some system. I don't think this language can be recognized by a linear bounded automaton, but I don't actually know. –  Tanner Swett Feb 25 '12 at 22:49

The set of true statements in Presburger Arithmetic is not context sensitive (as it has been shown that it is not $\text{NPSPACE}(n)$ decideable).