Der Mechanismus des Identifizierens, Isolierens oder Erzeugens von Zwischenlemmas bzw. Lemmakandidaten aus Beweisen, Suchspuren oder Heuristiken, um nachfolgendes Schließen zu beschleunigen, zu strukturieren oder wiederverwendbar zu machen.

Prinzip

Fasse wiederkehrende oder nützliche Zwischenfakten zusammen, die Beweisstruktur komprimieren und Redundanz reduzieren; qualitativ hochwertige Lemmata sind so allgemein, dass sie über Unterziele hinweg nutzbar sind, und zugleich spezifisch genug, um zukünftige Suche wirksam zu beschneiden.

Demonstration

Ein automatischer Beweiser speichert Konfliktklauseln aus einer SAT‑Suche als Lemmata, um dieselbe konfliktträchtige Belegung nicht erneut zu durchlaufen; ein Beweisassistent extrahiert häufig verwendete Beweismuster als benannte Lemmata, um interaktive Beweise zu verkürzen; induktive Heuristiken schlagen Lemmata vor, die ein Muster verallgemeinern, das in einem gescheiterten Beweisversuch gefunden wurde.

Fehlanwendung

Zu spezifische Lemmata extrahieren, die nur zu einer einzigen Beweisspur passen (führt zu Fragmentierung und Speicheraufwand), oder falsche Lemmata aufgrund fehlerhafter Instrumentation extrahieren, die danach nachfolgendes Schließen korrumpieren und unsichere Ergebnisse liefern.

Konsequenz

Effektive Lemmenextraktion verbessert die Modularität von Beweisen, reduziert redundante Suche, ermöglicht Lemma‑Bibliotheken und Caching und kann exponentielle Suchen in handhabbare Aufgaben verwandeln; schlechte Lemmata hingegen können Overhead erhöhen und Suche fehlleiten.

Umkehrung

Monolithische Beweissuche, die niemals Zwischenlemmata aufzeichnet oder wiederverwendet: jedes Teilziel wird wiederholt neu entdeckt, oft zu hohen Kosten; umgekehrt können übergeneralisierte Lemmata Struktur vernichten und Beweise brüchig machen.

Abgrenzung

Die Qualität extrahierter Lemmata hängt von der Extraktionsheuristik, der Domänenstruktur und der Verifikation der Lemmakorrektheit ab; Extraktion ist keine Allheilmittel — manche Domänen liefern wenige wiederverwendbare Lemmata und manche Extraktionsverfahren sind rechenintensiv.

Semantische Spannung

Zwischen Generalität und Nützlichkeit eines Lemmas: allgemeine Lemmata maximieren Wiederverwendung, laufen aber Gefahr, zu schwach zu sein, um Suche zu beschneiden; sehr spezifische Lemmata schneiden lokal gut, übertragen sich jedoch selten zwischen Problemen.

Synthese

Lemmenextraktion identifiziert und speichert Zwischenaussagen, die wiederkehrende Schlussmuster destillieren; durchdachte Extraktion und Validierung schaffen wiederverwendbare Bausteine, die Beweise komprimieren, Suche beschleunigen und modulares Schließen ermöglichen, wobei Kompromisse bei Generalität, Korrektheit und Speicherbedarf zu berücksichtigen sind.