de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

The `hardest´ natural decidable theory

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45677

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-3A20-F
Zusammenfassung
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.