Eine graphische, kanonische Darstellung von Beweisen in Fragmenten der linearen Logik, bei der Formeln und ihre Verbindungen als Knoten und Kanten modelliert werden; Beweisnetze legen Parallelität offen, reduzieren die syntaktische Bürokratie sequentieller Beweise und erlauben graphische Korrektheitskriterien sowie Cut-Elimination als lokale Graphtransformationen.

Prinzip

Eine Beweisdarstellung als graphartige Struktur kodieren (Links für logische Konnektive, Axiom-Links für atomare Paare), sodass Korrektheitsbedingungen diejenigen Graphen identifizieren, die gültigen sequentiellen Beweisen entsprechen; Cut-Elimination wird durch lokale Graphumformungen realisiert, die Korrektheit erhalten.

Demonstration

In der multiplikativen linearen Logik lässt sich eine Herleitung von A⊗B als Netz zeichnen, mit einem Tensor-Link, der die Teilnetze für A und B verbindet, und Axiom-Links, die duale Atome paaren; eine Korrektheitsbedingung (Azyklizität und Zusammenhang unter verschiedenen 'Switchings') bestätigt, dass das Diagramm einen gültigen Beweis darstellt und Cut-Elimination durch Graphumformungen erfolgt.

Fehlanwendung

Jedes beliebige Graph mit ähnlichen Knotengraden als Beweisnetz zu behandeln, ohne die vorgeschriebenen Korrektheitsbedingungen zu prüfen, oder Transformationen aus einem Fragment auf ein inkompatibles Fragment anzuwenden, kann zu unsauberen 'Beweisen' oder zum Verlust von Cut-Eliminationseigenschaften führen.

Konsequenz

Richtig gebildet liefern Beweisnetze ein kanonisches, oft kompaktes Zeugnis der Beweisbarkeit, machen Parallelität explizit, vereinfachen die Äquivalenz von Beweisen und wandeln Cut-Elimination in lokale, konfluente Graphumformungen um—was Analysen zu Komplexität und Normalisierung erleichtert.

Umkehrung

Das Gegenbild ist der sequentielle Sequentenbeweis: eine linear geordnete Regel-für-Regel-Herleitung, die die Reihenfolge der Regelanwendungen explizit festhält. Sequentielle Beweise machen das operationale Verhalten sichtbar, verschleiern jedoch die parallele Struktur und führen zu vielen syntaktischen Varianten desselben Netzes.

Abgrenzung

Beweisnetze sind für mehrere Fragmente der linearen Logik gut ausgearbeitet (multiplikativ, mit Vorsicht auch multiplikativ-exponentiell), erfordern jedoch fragment-spezifische Verknüpfungs- und Korrektheitsmechanismen; sie sind nicht ohne Weiteres für beliebige nichtlineare oder klassische Logiken verwendbar.

Semantische Spannung

Spannung zwischen Beweisnetzen und sequentieller Darstellung: Netze betonen kanonische Parallelstruktur und Äquivalenzklassen von Beweisen, Sequenten dagegen die syntaktische Reihenfolge und Operationalität; die Umkehrabbildung (Sequenzialisierung) ist fragmentabhängig und oft komplex.

Synthese

Beweisnetze komprimieren sequentielle Herleitungen zu Graphobjekten, die die wesentliche parallele Struktur und den kanonischen Inhalt von Beweisen in der linearen Logik sichtbar machen: mithilfe exakter Korrektheitsprüfungen und der Interpretation von Cut-Elimination als Graphumformungen bieten sie eine kompakte, semantisch transparente Darstellung von Beweisen und deren Normalisierung.