A Strategy Language for Controlled Proof Search

Technisches Resümee: Eine Strategiesprache für kontrollierte Beweisrecherche

Problemstellung
In der automatisierten Argumentation garantiert die statische Vollständigkeit eines logischen Kalküls (die Existenz eines Beweises für jeden Satz) nicht die dynamische Vollständigkeit eines Beweisers (die Fähigkeit, diesen Beweis tatsächlich zu finden). In semidecidierbaren Logiken können Inferenzregeln unendlich viele Nachfolger generieren. Wenn eine Beweisrecherche-Strategie eine unfaire Exploration anwendet – etwa einen naiven Tiefensuche-Ansatz, der einen Zweig unendlich lange priorisiert –, kann sie relevante Inferenzen auf ewig aufschieben und somit gültige Beweise nicht entdecken, selbst wenn diese existieren. Dieses Problem ist besonders akut in Frameworks wie Pgeon, die Inferenzregeln von Beweisrecherche-Strategien trennen, da das Design der Explorationspolitik ein entscheidender Faktor für den Erfolg ist.

Methodik
Das Paper führt eine formale Strategiesprache für Pgeon ein, ein Meta-Beweiser-Framework, das deklarative Spezifikationen logischer Kalküle in ausführbare Beweiser kompiliert. Der kernmethodische Wwickel besteht darin, die Beweisrecherche nicht als Relation zwischen Zuständen, sondern als Enumeration von Beweiszuständen mittels Streams zu modellieren.

1. Formale Semantik: Ein Beweiszustand ($\Sigma$) wird als ein teilweise konstruierter Beweisbaum behandelt. Eine Strategie wird als eine Funktion $s: \Sigma \to \text{Str}(\Sigma)$ definiert, die einen Zustand auf einen Stream (endlich oder unendlich) von Nachfolgezuständen abbildet. Dies macht Nichtdeterminismus explizit:

   • Ein leerer Stream repräsentiert Scheitern.
   • Ein Singleton-Stream repräsentiert deterministischen Erfolg.
   • Ein Stream mit mehreren Elementen repräsentiert nichtdeterministisches Abzweigen.
   • Unendliche Streams repräsentieren Regeln, die ungebunden viele Nachfolger generieren können.

2. Kombinatoren: Die Sprache stellt eine Menge von Operatoren bereit, um diese Strategien zu komponieren, wobei zwischen biased (Tiefensuche) und fairer (interleaved) Exploration unterschieden wird:

   • Sequenzielle Komposition ($;$): Wendet eine Strategie auf die Ergebnisse einer anderen an.
   • Links-biased Wahl ($\parallel$): Versucht die erste Strategie; falls diese scheitert (leerer Stream), fällt sie auf die zweite zurück.
   • Faire sequenzielle Komposition ($\&;$): Interleavt die Ergebnisse sequenzieller Anwendungen mittels Diagonalisierung ($\triangle$), wodurch sichergestellt wird, dass wenn ein Ergebnis in endlichen Schritten erreichbar ist, es schließlich exploriert wird.
   • Faire Wahl ($\&|$): Interleavt die Ergebnisse zweier alternativer Strategien fair.
   • Repetition ($*$): Definiert als ein Fixpunkt der kleinsten Ordnung unter Verwendung von fairer sequenzieller Komposition ($\mu X. \text{id} \&; (s \&; X)$), was sicherstellt, dass alle endlichen Iterationstiefen exploriert werden, anstatt strikt nach dem Tiefenprioritätsprinzip vorzugehen.

3. Primitivoperationen: Die Sprache enthält primitive Regeln ($r$) und einen Operator zur exhaustiven Anwendung ($r!$), der eine Regel auf alle zulässigen Übereinstimmungen in einem Zustand anwendet.

Kernbeiträge

• Kompositionelle Stream-Semantik: Das Paper liefert eine kompositionelle Algebra für Strategie-Kombinatoren, bei der der Suchraum als First-Class-Objekt (ein Stream) reifiziert wird. Dies ermöglicht es, über Fairness und Enumeration unabhängig von Implementierungsdetails wie Stack-Disziplin oder Kontinuationen zu argumentieren.
• Fairness-Mechanismen: Durch die Einführung von auf Diagonalisierung basierenden Interleaving-Operatoren ($\&;$ und $\&|$) adressiert das Framework das „Starvation“-Problem, bei dem unendliche Zweige die Entdeckung endlicher Beweise verhindern.
• Formale Strategiesprache für Pgeon: Die Arbeit formalisiert die Strategie-Komponente des Pgeon-Frameworks, indem sie den Kontrollfluss der Beweisrecherche in eine deklarative Sprache abstrahiert.

Ergebnisse und Fallstudien
Das Paper demonstriert die Ausdrucksstärke und Effektivität des Ansatzes durch zwei Fallstudien:

1. Prädikatenlogik erster Ordnung (LK): Die Autoren behandeln die Interaktion zwischen Closure (Unifikation) und Regelsättigung. Eine naive Strategie wiederholter Regelanwendung scheitert oft daran, Beweise zu finden, weil sie sich zu früh auf spezifische Instanziierungen festlegt. Die vorgeschlagene Strategie $(\odot^* \&; (\alpha \parallel \delta \parallel \beta \parallel \gamma!)^*)^*$ nutzt faire Komposition, um Closure-Versuche mit Regelsättigung zu verweben. Dies stellt sicher, dass verschiedene Unifikationsentscheidungen über alle Suchtiefen hinweg exploriert werden, was verhindert, dass das System in unendlichen Instanziierungsschleifen stecken bleibt und dabei eine abschließende Ableitung übersieht.

2. Modallogik (S4): In S4 ist die nichtdeterministische Regel $\theta$ (beliebige Entfernung von Formeln) notwendig, um die Anwendung der Modallogik-Regel S4 zu ermöglichen, birgt aber das Risiko, benötigte Formeln zu verwerfen. Ein unkontrollierter Einsatz von $\theta$ führt zu Sackgassen. Die Autoren schlagen eine kombinierte Strategie $\theta^* \&; \text{S4}$ vor, die alle Wege zur Entfernung von Formeln zur Ermöglichung von S4-Anwendungen fair exploriert. Diese wird in eine größere Strategie $((\alpha \parallel \beta \parallel T)^*; (\theta^* \&; \text{S4}))^*$ integriert, was sicherstellt, dass wenn eine erfolgreiche Anwendung von S4 eine spezifische Teilmenge entfernter Formeln erfordert, diese Konfiguration schließlich erreicht wird, ohne dass Starvation eintritt.

Bedeutung
Das Paper behauptet, dass dieser Ansatz eine prinzipielle und modulare Grundlage für die Spezifikation und Analyse von Beweisrecherche-Verfahren bietet. Durch die Trennung von Inferenzregeln und Suchstrategien sowie die Bereitstellung einer formalen Sprache mit kompositioneller Semantik ermöglicht das Framework die systematische Exploration von Suchräumen in semidecidierbaren Logiken. Es zeigt, dass dynamische Vollständigkeit selbst dann erreicht werden kann, wenn naive Tiefensuche-Strategien versagen, indem Fairness explizit durch Stream-Interleaving verwaltet wird. Die Arbeit ermöglicht das Argumentieren über Beweisrecherche-Verfahren auf einer abstrakten Ebene, unabhängig von der spezifischen Implementierung des Beweisers.