Beweissystemen

Beweissysteme sind formale Verfahren zur Erzeugung und Überprüfung von Beweisen in einer gegebenen formalen Sprache. In der Logik und Mathematik ermöglichen sie, aus Axiomen und zulässigen Ableitungsregeln schrittweise neue Sätze abzuleiten. Formalisiert wird ein Beweissystem durch die Menge der Formeln sowie eine Regelmenge, mit der aus einer Sequenz von Formeln eine neue Formel abgeleitet werden kann. Eine Beweisführung besteht daher aus einer endlichen Folge von Formeln, die am Ende den zu beweisenden Satz enthält.

In der theoretischen Informatik wird oft der Begriff Cook–Reckhow-Beweissystem verwendet: Ein Beweissystem P für eine Sprache L ist eine computierbare Relation zwischen einem Satz φ und einer Beweiszeichenkette π, so dass π ein gültiger Beweis von φ in S ist. Wichtige Eigenschaften sind Soundness (nur wahre Sätze können bewiesen werden) und Vollständigkeit (jeder wahre Satz besitzt einen Beweis). Zusätzlich interessiert die Effizienz: Beweise und deren Verifikation sollen möglichst in polynomialer Zeit erfolgen.

Zu den Beweissystemen zählen klassische Hilbert-Systeme, natürliche Deduktion, Sequentenkalkül sowie spezielle Beweissysteme wie Resolution für die Aussagenlogik. In der Praxis spielen auch Beweisassistenten eine Rolle, und in der formalen Verifikation werden Programme und Hardware durch Beweissysteme geprüft.

Anwendungen umfassen mathematische Beweise, formale Verifikation sicherheitskritischer Systeme und kryptographische Beweisverfahren wie Zero-Knowledge- oder interaktive Beweise. Die Geschichte der Beweissysteme reicht von der frühen formalen Logik über Hilbert und Gentzen bis zur Entwicklung computergestützter Beweisführung im 20. und 21. Jahrhundert.