Ein deterministischer Algorithmus oder Mechanismus, der für jede Eingabeformel in einer bestimmten logischen Theorie oder einem Fragment terminiert und korrekt entscheidet, ob die Formel erfüllbar ist (oder zur Theorie gehört), gemäß Soundness- und Vollständigkeitsgarantien für dieses Fragment.

Prinzip

Beschränkung der Sprache oder Theorie auf ein entscheidbares Fragment und Entwurf terminierender, korrekter Regeln oder Algorithmen (häufig mittels Normalformen, Automatenkonstruktionen, Kongruenzabschluss, Quantorenelimination oder Tableaus), die den Suchraum innerhalb endlicher Ressourcen erschöpfend untersuchen.

Demonstration

Ein Entscheidungsverfahren für Gleichheit mit uninterpretierten Funktionen (EUF), implementiert durch Kongruenzabschluss, entscheidet deterministisch, ob eine Menge von Gleichungen und Ungleichungen erfüllbar ist, indem es Äquivalenzklassen pflegt und Verschmelzungen propagiert, bis entweder ein Widerspruch abgeleitet oder ein Modell konstruiert wird.

Fehlanwendung

Die Anwendung eines Entscheidungsverfahrens außerhalb seines deklarierten Fragments (z. B. ein Presburger-Verfahren auf Formeln mit Multiplikation quantifizierter Variablen) kann zu Nichtterminierung oder falschen Antworten führen; das Behandeln eines unvollständigen Solvers als Entscheidungsverfahren führt zu unsicherer Annahme von Erfüllbarkeitsaussagen.

Konsequenz

Sind Entscheidungsverfahren für eine Theorie verfügbar, ermöglichen sie modulare Reasoning-Komponenten in größeren Systemen (z. B. SMT-Solver), bieten automatisierte Korrektheitsgarantien für dieses Fragment und erlauben die vollständige Automatisierung von Verifikationsaufgaben, die im Fragment ausdrückbar sind.

Umkehrung

Die Umkehr ist eine unentscheidbare oder semi-entscheidende Methode, die nicht für alle Eingaben terminiert oder nur Teilantworten liefert (z. B. enumerative Suche oder heuristische Solver); solche Methoden tauschen Vollständigkeit und Terminierung gegen breitere Anwendbarkeit ein.

Abgrenzung

Gilt für Algorithmen mit nachgewiesener Terminierung und Korrektheit auf einem klar spezifizierten logischen Fragment oder einer Theorie. Schließt Heuristiken, Approximationen, semi-entscheidende Verfahren, die divergieren können, und Methoden, die nur wahrscheinliche oder statistische Antworten liefern, aus.

Semantische Spannung

Es besteht Spannung zwischen der Allgemeinheit des logischen Fragments (weitere Fragmente sind oft unentscheidbar) und der algorithmischen Tragbarkeit; zudem besteht Spannung zwischen dem Aufbau eines vollständig entscheidungsfähigen, aber potenziell teuren Verfahrens und der Nutzung unvollständiger, schnellen Heuristiken in der Praxis.

Synthese

Ein Entscheidungsverfahren ist ein formal spezifizierter Algorithmus für ein entscheidbares Fragment, der Terminierung und korrekte Ja/Nein-Antworten zur Erfüllbarkeit garantiert, indem er die Ausdrucksstärke einschränkt und vollständige symbolische oder automatenbasierte Techniken zur vollständigen Durchsuchung des Fragments anwendet.