Von der Beweistheorie zu maschinellen Beweisassistenten

Die moderne Beweistheorie eröffnet die Möglichkeit, interaktive und automatische Beweisassistenten zu entwickeln, die sowohl Beweise in der Mathematik als auch Softwareprogramme in der Informatik überprüfen können. Die zunehmende Komplexität von menschlichem Wissen und menschlicher Technik macht Verifikation zu einem Schlüsselproblem zukünftiger Entwicklungen, insbesondere auf dem Gebiet der Künstlichen Intelligenz. Der Artikel zeigt aber auch, wie tief diese aktuellen Entwicklungsfragen in den Grundlagen von Logik, Mathematik und Philosophie verwurzelt sind.