Techniken und Transformationen zur Reduzierung der Größe, Länge oder strukturellen Komplexität eines Beweises bei gleichzeitiger Bewahrung seiner Korrektheit und Überprüfbarkeit.

Prinzip

Kompression entfernt redundante Teilbeweise, fasst identische Herleitungen in gemeinsamen Strukturen (DAGifizierung) zusammen, führt Lemmas oder Abstraktionen ein und nutzt Normalisierung oder Schnitt-Einführung/-Elimination, um Gültigkeit zu erhalten und gleichzeitig die Darstellung zu verkleinern.

Demonstration

Ein langer sequentieller Beweis mit wiederholten Herleitungen desselben Zwischenlemmas wird in einen gerichteten azyklischen Graphen umgewandelt, der die gemeinsame Teilbeweiskonstruktion einmal teilt, wodurch die Knotenanzahl sinkt und die erneute Überprüfung durch Beweisassistenten beschleunigt wird.

Fehlanwendung

Übermäßig aggressive Kompression, die nachprüfbare Struktur entfernt oder Schritte durch implizite Annahmen ersetzt, kann den Beweis für Standardprüfer unüberprüfbar machen oder die menschliche Interpretierbarkeit verringern; das Einführen unbelegter Lemmas zerstört die Korrektheit.

Konsequenz

Reduziert Speicher- und Übertragungskosten, beschleunigt automatisches Beweisprüfen und -wiedergeben und legt häufig höherstufige Struktur (Lemmas, modulare Argumente) offen, die für Wartung und Verständnis nützlich ist.

Umkehrung

Beweisausweitung: Alle Makroschritte auflösen und alle Lemmata in primitive Schritte eininline-en, was die Größe erhöht und trotz maximaler Explizitheit die Struktur verschleiern kann.

Abgrenzung

Gilt für formale Beweise in deduktiven Systemen, bei denen Transformationen logische Gültigkeit und Prüfbarkeit erhalten; schließt verlustbehaftete Zusammenfassungen aus, die Prüfbarkeit opfern, sowie informelle Skizzen, die Herleitungen ganz weglassen.

Semantische Spannung

Spannung zwischen maximaler Kompression für maschinelle Effizienz und der Bewahrung für Menschen lesbarer, prüfbarer Beweisstruktur; auch Spannung zu Beweiszertifikaten, die Prüfbarkeit über minimale Größe stellen.

Synthese

Beweiskompression umfasst korrekte Transformationen — Teilen von Unterherleitungen, Lemmaextraktion, Normalisierung —, die die Darstellungsgröße eines Beweises reduzieren und zugleich Korrektheit und Prüfbarkeit erhalten, wobei Effizienz und Nachvollziehbarkeit abgewogen werden.