Einführung #
Der mathematische Begriff “Beweis” spielt eine zentrale Rolle. Es soll hier formal definiert werden, was unter einem Beweis zu verstehen ist und welche Parallelen zwischen Beweis und Berechnung bestehen.
Die in diesem Bereich beschriebenen Konzepte werden in der Beweistheorie, mathematischen Logik und des maschinengestützten Beweisens eingesetzt. Letzeres hat ein interessante praktische Anwendung, nämlich die Möglichkeit des Beweises, ob ein Programm fehlerfrei ist.
Um die Syntax zu beschreiben, wird die Backus–Naur Form verwendet.
Es soll eine Einführung in folgende Themen gegeben werden: