Gute Referenz über ungefähre Methoden zur Lösung von Logikproblemen

Es ist bekannt, dass viele Logikprobleme (z. B. Erfüllbarkeitsprobleme mehrerer Modallogiken) nicht entscheidbar sind. Es gibt auch viele unentscheidbare Probleme in der Algorithmustheorie, z. B. bei der kombinatorischen Optimierung. In der Praxis eignen sich Heuristiken und Näherungsalgorithmen jedoch gut für praktische Algorithmen.

Man kann also davon ausgehen, dass auch ungefähre Algorithmen für Logikprobleme geeignet sein können. Der einzige Forschungstrend in dieser Richtung, den ich gefunden habe, ist das Max-SAT-Problem, dessen Entwicklung in den neunziger Jahren aktiv war.

Gibt es andere aktive Forschungstrends, Workshops, Stichwörter, gute Referenzen für die Verwendung und Entwicklung von Näherungsmethoden für die Modallogik, die Logikprogrammierung usw.?

Wenn das automatisierte Denken in zukünftigen Anwendungen der Informatik eine herausragende Rolle spielen soll, muss man in der Lage sein, die Unentscheidbarkeitsbeschränkungen der Logik zu überwinden, und ungefähre Methoden oder Heuristiken können ein natürlicher Weg sein, nicht wahr?

Die Motivation, die Sie zum Umgang mit Unentscheidbarkeit angeben, gilt auch für entscheidbare, aber schwierige Probleme. Wenn Sie ein NP-hartes oder PSPACE-hartes Problem haben, müssen wir normalerweise eine Näherungsform (im weiteren Sinne des Wortes) verwenden, um eine Lösung zu finden.

Es ist nützlich, zwischen verschiedenen Begriffen der Annäherung zu unterscheiden.

• Numerische Approximation: Wird angewendet, wenn Sie eine Metrik für den Lösungsraum haben und die Entfernung von der Lösung messen können. Dies ist der Fall bei Problemen wie #SAT, bei denen Sie Lösungen zählen und einen Approximationsalgorithmus entwerfen können, der einen Wert innerhalb von der Lösung zurückgibt .$\varepsilon$
• Probabilistische Approximation: Wenn Sie einen zufälligen Algorithmus verwenden, können Sie die Gewissheit über die Lösung aufgeben, die Sie jedes Mal erhalten, wenn Sie den Algorithmus ausführen. Sie können zwischen der Zufälligkeit im Algorithmus und der Zufälligkeit im Lösungsraum wechseln, indem Sie eine Wahrscheinlichkeitsverteilung über die Lösungen berücksichtigen. Dann ist die Annäherung hier, dass Sie mit einer Wahrscheinlichkeit größer als eine korrekte Lösung erhalten.$\delta$

Es gibt -Algorithmen für Probleme wie ALLSAT, die die beiden obigen Perspektiven kombinieren. Im konkreten Fall von unentscheidbaren Problemen oder Problemen, bei denen es keine offensichtliche Metrik gibt und wir keinen randomisierten Algorithmus verwenden möchten, stellt sich die Frage, welcher Begriff von Annäherung zu verwenden ist. Dieses Problem tritt speziell bei der Analyse von Programmen bei der Optimierung von Compilern und bei der Programmüberprüfung auf. Das Bestimmen komplexer Eigenschaften von Programmen ist entweder unentscheidbar oder rechenintensiv, weshalb eine Art von Approximation erforderlich ist.$(\varepsilon,\delta)$

Hier ist ein Beispiel für einen anderen Begriff der Annäherung. Angenommen, Sie führen eine Berechnung wie das Multiplizieren von zwei großen Zahlen durch und möchten überprüfen, ob die Multiplikation korrekt war. Es gibt viele heuristische Techniken, die in der Praxis verwendet werden, um die Richtigkeit zu überprüfen, ohne die Berechnung erneut zu wiederholen. Sie können überprüfen, ob die Zeichen multipliziert wurden, um das richtige Zeichen zu erhalten. Sie können überprüfen, ob die Zahlen die richtige Parität haben (Eigenschaften für gerade / ungerade Zahlen). Sie können ein ausgefeilteres Häkchen verwenden, z. B. Neunen ausstreichen. Alle diese Techniken haben eine gemeinsame Eigenschaft, die Ihnen sagen kann, ob Sie einen Fehler gemacht haben, aber sie können nicht garantieren, ob Sie die richtige Antwort erhalten haben. Diese Eigenschaft kann als logische Annäherung angesehen werden, da Sie möglicherweise nachweisen können, dass die ursprüngliche Berechnung falsch ist, Sie jedoch möglicherweise nicht nachweisen können, dass sie korrekt ist.

Alle oben erwähnten Überprüfungen sind Beispiele für eine Technik, die als abstrakte Interpretation bezeichnet wird. Durch die abstrakte Interpretation wird ein Begriff der logischen Approximation, der sich von numerischen und probabilistischen Approximationen unterscheidet, streng definiert. Das Problem, das ich bei der Analyse einer einzelnen Berechnung beschrieben habe, erstreckt sich auf den komplexeren Fall der Analyse eines Programms. In der Literatur zur abstrakten Interpretation wurden Techniken und Rahmenbedingungen für eine ungefähre, logische Argumentation über Programme und in jüngerer Zeit über Logik entwickelt. Die folgenden Verweise könnten nützlich sein.

1. Abstrakte Interpretation in Kürze von Patrick Cousot, die eine einfache Übersicht ist.
2. Überblick über die Abstraktion von Patrick Cousot als Teil seines Kurses. Es gibt ein sehr schönes Beispiel für eine Abstraktion zur Bestimmung der Eigenschaften eines Blumenstraußes. Die Blumenstrauß-Analogie enthält feste Punkte und kann vollständig mathematisch präzise gemacht werden.
3. Kurs über abstrakte Interpretation von Patrick Cousot, wenn Sie all die Tiefe und Details wollen.
4. Abstrakte Interpretation und Anwendung auf Logikprogramme , Patrick Cousot und Radhia Cousot, 1992. Gilt für Logikprogramme gemäß Ihrer Anfrage. Der erste Abschnitt formalisiert auch das Neunergussverfahren als abstrakte Interpretation.

All dies wurde typischerweise auf Computerprogramme angewendet. In jüngster Zeit wurde daran gearbeitet, Ideen aus der abstrakten Interpretation anzuwenden, um Entscheidungsverfahren für Logik zu untersuchen. Der Schwerpunkt lag nicht auf der Modallogik, sondern auf der Erfüllbarkeit der Aussagenlogik und quantifikatorfreien Theorien erster Ordnung. (Da ich in diesem Raum gearbeitet habe, ist ein Papier unten meins)

1. Eine Verallgemeinerung der Methode von Staalmarck durch Aditya Thakur und Thomas Reps, 2012. Gibt eine Verallgemeinerung der Methode von Staalmarck auf Probleme in der Programmanalyse.
2. Das reduzierte Produkt aus abstrakten Domänen und der Kombination von Entscheidungsverfahren , Patrick Cousot, Radhia Cousot und Laurent Mauborgne, 2011. Diese Arbeit untersucht die Nelson-Oppen-Technik zur Kombination von Entscheidungsverfahren und zeigt, dass sie auch für unvollständige Kombinationen verwendet werden kann ist besonders interessant, wenn Sie unentscheidbare Probleme haben.
3. Erfüllbarkeitslöser sind statische Analysatoren , meine Arbeit mit Leopold Haller und Daniel Kroening, 2012. Wendet die gitterbasierte Approximationsansicht zur Charakterisierung vorhandener Löser an. Sie können sich stattdessen auch meine Folien zum Thema ansehen .

Keines der oben genannten Papiere beantwortet jetzt Ihre spezifische Frage, wie Sie nicht entscheidbare Erfüllbarkeitsprobleme angreifen können. Was diese Arbeiten tun, ist eine approximationsorientierte Sicht auf logische Probleme, die nicht numerisch oder probabilistisch sind. Diese Ansicht wurde ausgiebig auf die Argumentation zu Programmen angewendet, und ich glaube, sie geht genau auf Ihre Fragen ein.

Um es auf die Modallogik anzuwenden, würde ich vorschlagen, dass ein Ausgangspunkt die algebraische Semantik von Jonsson und Tarski oder die spätere Semantik von Lemmon und Scott ist. Dies liegt daran, dass die abstrakte Interpretation in Form von Gittern und monotonen Funktionen formuliert ist. Boolesche Algebren mit Operatoren sind daher eine bequeme Semantik für die Arbeit. Wenn Sie mit Kripke-Frames beginnen möchten, können Sie den Dualitätssatz von Jonsson und Tarski (den manche als Stone-Dualität bezeichnen) anwenden und die algebraische Darstellung ableiten. Danach können Sie die Theoreme der abstrakten Interpretation zur logischen Approximation anwenden.