Resolution for Constrained Pseudo-Propositional Logic

Technisches Resümee: Resolution für die beschränkte pseudo-propositionale Logik

Problemstellung
Die vorliegende Arbeit befasst sich mit den Einschränkungen der Standard-Aussagenlogik und der mit ihr verbundenen SAT-Algorithmen beim Umgang mit Zählbeschränkungen. Da SAT-Solver, die auf dem Resolutionsbeweissystem basieren, für Probleme in der formalen Verifikation, Planung und Zeitplanung hocheffektiv sind, ist die Ausdrucksstärke der standardmäßigen Aussagentechnischen Sprache für eine native Zählung unzureichend. Die Kodierung von Zählbeschränkungen in die konjunktive Normalform (KNF) führt typischerweise zu einer massiven Erhöhung der Anzahl an Klauseln und Variablen, was zu einer unpraktikablen Rechenkomplexität führt.

Um dies zu mildern, wurde die Constrained Pseudo-Propositional Logic (CPPL) als Erweiterung der Aussagenlogik entwickelt. CPPL integriert natürliche Zahlen und Beschränkungssymbole in das Alphabet, was eine kompakte Formulierung von Zählbeschränkungen ermöglicht. Das bestehende Beweissystem für CPPL stützt sich jedoch auf eine lange Liste von Inferenzregeln (wie in der referenzierten Tabelle 1 der Quellliteratur detailliert), was für eine computergestützte Implementierung umständlich ist. Ein Beweissystem mit weniger Regeln ist wünschenswert, um die zu berücksichtigenden Fälle zu reduzieren und die Effizienz der Implementierung zu steigen.

Methodik
Die Arbeit schlägt ein generalisiertes Resolutionsbeweissystem vor, das speziell für CPPL entwickelt wurde und als CPPL-Resolution bezeichnet wird. Die Methodik umfasst:

1. Formalisierung der CPPL-Syntax und -Semantik: Die Arbeit definiert die Sprache der CPPL, welche propositionale Variablen, natürliche Zahlen und Beschränkungssymbole ($>, \ge, =, <, \le$) umfasst. Sätze werden als Tripel $(\phi, \bowtie, n)$ gebildet, wobei $\phi$ eine pseudo-propositionale Formel ist, $\bowtie$ eine Beschränkung darstellt und $n$ eine natürliche Zahl ist. Die Semantik wird über Interpretationen definiert, die Formeln auf Paare von Integern abbilden, welche Wahrheitswerte und Zählwerte repräsentieren.
2. Standardisierung: Die Arbeit beschränkt das Resolutionssystem auf Sätze in „Standardform“, bei denen die Formel in Normalform (eine Summe von Pseudo-Literalen) vorliegt und die Beschränkung spezifisch $\ge$ ist. Es wird angemerkt, dass jeder CPPL-Satz äquivalent in diese Standardform transformiert werden kann.
3. Regelreduktion: Im Gegensatz zum vorherigen System mit zahlreichen Inferenzregeln nutzt das vorgeschlagene CPPL-Resolutionssystem nur zwei primäre Ableitungsregeln:
   • Regel I (Monotonie/Initial): Behandelt Teilmengenbeziehungen zwischen Mengen von Sätzen.
   • Regel II (Resolution): Eine generalisierte Resolutionsregel. Gegeben seien zwei Sätze $(\phi_1 + \beta)(\ge, n_1)$ und $(\phi_2 + \neg\beta)(\ge, n_2)$, so leitet die Regel $(\phi_1 + \phi_2)(\ge, n_1 + n_2 - |\beta|)$ ab. Diese Regel eliminiert effektiv das Literal $\beta$ und dessen Negation, während sie den Beschränkungsschwellenwert basierend auf den Koeffizienten anpasst.
4. Beweis der Eigenschaften: Die Arbeit liefert einen konstruktiven Beweis, der zeigt, dass dieses Zwei-Regel-System sowohl korrekt (abgeleitete Sätze sind semantisch gültig) als auch vollständig (alle semantisch gültigen Sätze sind ableitbar) ist. Der Beweis der Vollständigkeit stützt sich auf das Zornsche Lemma, um konsistente Mengen zu maximal konsistenten Mengen zu erweitern, die dann als erfüllbar gezeigt werden können.

Zentrale Beiträge

• Generalisierung der Resolution: Die Arbeit generalisiert das propositionale Resolutionssystem erfolgreich auf den Bereich der CPPL.
• Minimalistisches Regelsatz: Sie etabliert ein Resolutionssystem für die CPPL, das nur zwei Inferenzregeln benötigt, wodurch das logische Framework im Vergleich zum bisher existierenden Multi-Regel-System signifikant vereinfacht wird.
• Konstruktive Korrektheit und Vollständigkeit: Die Arbeit liefert einen rigorosen, konstruktiven Beweis dafür, dass das vorgeschlagene CPPL-Resolutionssystem sowohl korrekt als auch vollständig ist.
• Erweiterung auf unendliche Klauseln: Ein bedeutendes theoretisches Nebenprodukt dieser Arbeit ist der Nachweis, dass die propositionale Resolution auch dann korrekt und vollständig bleibt, wenn sie auf Formeln mit einer unendlichen Menge von Klauseln angewendet wird – eine Eigenschaft, die für die Standard-KNF nicht erforderlich ist, aber vom CPPL-Framework natürlich unterstützt wird.

Ergebnisse
Das Primärergebnis ist die Validierung des CPPL-Resolutionssystems. Die Arbeit beweist, dass für jede Menge von Sätzen $S$ und $S'$ gilt: Wenn $S$ semantisch $S'$ impliziert ($S \models S'$), dann ist $S'$ aus $S$ unter Verwendung der vorgeschlagenen Resolutionsregeln ableitbar ($S \vdash_r S'$). Der Beweis nutzt die Eigenschaften maximal konsistenter Mengen, um die Lücke zwischen semantischer Implikation und syntaktischer Ableitbarkeit zu schließen.

Bedeutung
Die Arbeit behauptet, dass das vorgeschlagene System eine effizientere Grundlage für das automatisierte Schließen in der beschränkten pseudo-propositionalen Logik bietet. Durch die Reduktion der Inferenzregeln auf einen minimalen Satz analog zur propositionalen Resolution wird das System besser für eine computergestützte Implementierung geeignet, was potenziell die Leistung von SAT-basierten Solvern für Probleme mit Zählbeschränkungen verbessert. Darüber hinaus zeigt die Arbeit, dass die Robustheit der propositionalen Resolution über endliche Klauselmenge hinausgeht und ihre Korrektheit und Vollständigkeit im Kontext unendlicher Klauselmenge innerhalb des CPPL-Frameworks beibehält.