Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse




Conference Paper

The `hardest´ natural decidable theory


Vorobyov,  Sergei
Computational Biology and Applied Algorithmics, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Vorobyov, S. (1997). The `hardest´ natural decidable theory. In G. Winskel (Ed.), Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS-97) (pp. 294-305). New York, USA: IEEE.

Cite as:
Since mid-seventies it was an open problem as to whether there exist natural decidable theories requiring time (lower bound) exceeding any linearly growing towers of 2s to decide. It was conjectured that all natural decidable theories can be decided (upper bound) within time bounded by a tower of 2s growing linearly with the length of input. Although it happens to be true for the majority of non-elementary theories (Rabin's S2S, theory of term algebras, extended regular expressions, etc), the conjecture fails. We demonstrate that a modest fragment of L.Henkin's theory of propositional types (1963) has the tower of 2s growing *exponentially* with the length of input as a lower bound. This new unprecedentedly high lower bound allows us to considerably improve the known lower bounds and to settle the new ones for other theories.