Eine atomare Formel oder ihre Negation, häufig verwendet als Grundeinheit in klausebasierten Darstellungen und Erfüllbarkeitsverfahren.

Prinzip

Ein Literal ist die kleinste signierte propositionale Einheit: entweder ein Atom (positives Literal) oder die Negation eines Atoms (negatives Literal); Klauseln werden als Disjunktionen von Literalen gebildet und viele Inferenzregeln arbeiten auf Literalebene.

Demonstration

Gegeben das Atom p sind die beiden Literale p und ¬p; in der Prädikatenlogik sind P(x) und ¬P(a) Literale, wobei P ein Prädikatsymbol und x bzw. a Terme sind.

Fehlanwendung

Zusammengesetzte Formeln wie (p ∧ q) oder quantifizierte Formeln als Literale zu behandeln ist missbräuchlich und bricht klausebasierte Algorithmen, die voraussetzen, dass Literale atomar oder negiert-atomar sind.

Konsequenz

Die korrekte Identifikation von Literalen ermöglicht Klauseldarstellung, Unit-Propagation, Resolutionsschritte und effizientes Indexieren; viele SAT- und Theorembeweiser-Optimierungen beruhen auf Literal-Operationen.

Umkehrung

Statt in signierte Atome zu zerlegen, Literale zu komplexen Unterformeln zusammenzufassen kehrt die atomare Sicht um und verlagert die Arbeit zu strukturellerem, höherstufigem Reasoning.

Abgrenzung

Ein Literal muss ein Atom oder dessen explizite Negation sein; es schließt boolesche Kombinationen (Konjunktionen, Disjunktionen) aus, es sei denn, diese werden kodiert, und Gleichheit kann je nach Formalismus als atomarer Prädikat betrachtet werden oder nicht.

Semantische Spannung

Literal vs Atom vs signiertes Literal: 'Atom' bezeichnet die unsignierte atomare Formel, 'Literal' impliziert typischerweise die signierte Form; manche Texte verwenden 'signiertes Literal', um die Polarität zu betonen.

Synthese

Ein Literal ist die atomare Aussage oder deren Negation, die als grundlegende signierte Einheit in klausebasierten Formalismen dient; es ermöglicht polaritätsbewusste Inferenzmechanismen in SAT-Solvern und Resolutionskalkülen.