Das entscheidungsbezogene oder algorithmische Problem, zu bestimmen, ob eine Menge von Prämissen Γ eine Schlussformel φ in einer gegebenen Logik und Semantik semantisch impliziert (Γ ⊨ φ), typischerweise durch Beweis- oder Gegenmodell-Suche.

Prinzip

Folgerungsprüfung reduziert sich darauf, entweder zu zeigen, dass jedes Modell von Γ auch ein Modell von φ ist (semantischer Ansatz), oder dass φ aus Γ in einem korrekten Beweissystem ableitbar ist (syntaxlicher Ansatz); Gleichheit hängt von Korrektheit und Vollständigkeit des Systems gegenüber der Semantik ab.

Demonstration

In der Aussagenlogik prüft man Γ ⊨ φ durch Erfüllbarkeitsprüfung: Γ ⊨ φ genau dann, wenn Γ ∪ {¬φ} unerfüllbar ist; ein SAT-Solver kann also Entailment bestätigen, indem er Unerfüllbarkeit meldet.

Fehlanwendung

Die syntaktische Beweisbarkeit (Γ ⊢ φ) mit semantischem Entailment zu verwechseln, wenn das gewählte Beweissystem für die intendierte Semantik unvollständig ist, oder Entailment-Prüfverfahren außerhalb ihres Entscheidbarkeitsbereichs anzuwenden (z. B. eine Entscheidbarkeit für unentscheidbare Logiken anzunehmen).

Konsequenz

Zuverlässige Folgerungsprüfung ermöglicht automatisches Theorembeweisen, Programmverifikation und Anfragebeantwortung; ihre Komplexität bzw. Entscheidbarkeit steuert das Design von Werkzeugen (z. B. NP-vollständig in der Aussagenlogik, semi-entscheidbar oder unentscheidbar in vielen ersterordnungslogischen Fragmenten).

Umkehrung

Nicht-Folgerung (Γ ⊭ φ) lässt sich in ein informatives Zeugnis umkehren: ein Gegenmodell, das Γ erfüllt und φ widerlegt, womit die vorgeschlagene Folgerung entkräftet wird und das Debugging oder die Hypothesenrevision unterstützt.

Abgrenzung

Entscheidbar und oft effizient lösbar in der Aussagenlogik und vielen beschränkten, entscheidbaren Fragmenten; unentscheidbar oder nur semi-entscheidbar in der allgemeinen ersten Ordnung, abhängig vom Fragment und der Semantik; hängt von der gewählten Logik, Signatur und der Frage nach endlichen Modellen ab.

Semantische Spannung

Spannung besteht zwischen modelltheoretischem Entailment (semantisch) und beweistheoretischer Ableitbarkeit (syntaxlich): praktische Systeme navigieren diesen Konflikt mit hörbaren, vollständigen oder unvollständigen Heuristiken und oft einem Kompromiss zwischen Vollständigkeit und Laufzeitverhalten.

Synthese

Folgerungsprüfung ist die operationale Aufgabe zu entscheiden, ob Prämissen eine Schlussfolgerung implizieren, durch semantische Modellsuche oder syntaktische Beweissuche; ihre Anwendbarkeit und Garantien hängen von der Entscheidbarkeit der Logik und der gewählten Strategie ab.