Theoretische Informatik
Die theoretische Informatik beschäftigt sich mit der Theorie formaler Sprachen bzw. Automatentheorie, Berechenbarkeitstheorie, Komplexitätstheorie, Logik (u. a. Aussagenlogik und Prädikatenlogik), formaler Semantik und bietet Grundlagen für den Bau von Programmiersprachen und die mathematische Formalisierung von Problemstellungen. Sie ist somit das formale Rückgrat der Informatik.Sie beschäftigt sich außerdem mit der mathematischen Lösbarkeit von Problemen, also inwieweit sich Probleme überhaupt mathematisch formulieren und damit lösen lassen, und welchen Aufwand man dazu treiben muss.
Dabei werden formale Systeme, Automaten, Graphen und Syntaxdiagramme dazu genutzt, die innere Logik eines formalen Problems exakt wiederzugeben. Oft ist dieser formale Schritt ein wesentlicher Teil zur Lösung der eigentlichen Problemstellung und erschließt eine durch Maschinensemantik noch bequemer gewordene Welt der Mathematik und Computerei.
Zu den bekanntesten Problemen der theoretischen Informatik gehören die NP-vollständigen Probleme wie z.B. das Traveling-Salesperson-Problem und die sich daraus ergebende Frage, ob P=NP ist.
Siehe auch: Algorithmus, Entscheidbarkeit, Alan Turing, Turingmaschine, Registermaschine, Chomsky-Hierarchie, mathematisches Beweisen, Programmiermaschine, Logik-Programmierung, reflexiv-transitive Hüllen, Graphentheorie, Compiler, Fixpunktsemantik, Pumping-Lemma, Kurt Gödel, Backus-Naur-Form, Halteproblem, Churchsche These, Stephen A. Cook