Die Standardlogik ist eine nicht-monotone Logik, die von Raymond Reiter vorgeschlagen wurde, um die Argumentation mit Standardannahmen zu formalisieren.

Die Standardlogik kann Fakten wie „standardmäßig ist etwas wahr“ ausdrücken; Im Gegensatz dazu kann Standardlogik nur ausdrücken, dass etwas wahr ist oder dass etwas falsch ist. Dies ist ein Problem, da die Argumentation oft Tatsachen beinhaltet, die in der Mehrzahl der Fälle zutreffen, jedoch nicht immer. Ein klassisches Beispiel ist: „Vögel fliegen normalerweise“. Diese Regel kann in der Standardlogik entweder durch „alle Vögel fliegen“ ausgedrückt werden, was nicht mit der Tatsache übereinstimmt, dass Pinguine nicht fliegen, oder durch „alle Vögel, die keine Pinguine sind und keine Straußen und … fliegen“, was alles erfordert Ausnahmen von der zu spezifizierenden Regel. Die Standardlogik zielt darauf ab, Inferenzregeln wie diese zu formalisieren, ohne alle Ausnahmen explizit zu erwähnen.

Syntax der Standardlogik
Eine Standardtheorie ist ein Paar  . W ist eine Menge von logischen Formeln, die als Hintergrundtheorie bezeichnet werden, die die Tatsachen formalisieren, die mit Sicherheit bekannt sind. D ist eine Reihe von Standardregeln, von denen jede folgende Form hat:

Laut dieser Vorgabe, wenn wir glauben, dass Prerequisite wahr ist, und jeweils  stimmt mit unseren derzeitigen Überzeugungen überein, wir glauben, dass die Schlussfolgerung wahr ist.

Die logischen Formeln in W und alle Formeln in einem Standardwert wurden ursprünglich als logische Formeln erster Ordnung angenommen, sie können jedoch möglicherweise Formeln in einer beliebigen formalen Logik sein. Der Fall, in dem sie Formeln in der Aussagenlogik sind, ist einer der am meisten untersuchten.

Beispiele
Die Standardregel „Vögel fliegen normalerweise“ wird durch die folgende Standardeinstellung formalisiert:

Diese Regel bedeutet, dass, wenn X ein Vogel ist und davon ausgegangen werden kann, dass er fliegt, wir daraus schließen können, dass er fliegt. Eine Hintergrundtheorie mit einigen Fakten über Vögel ist die folgende:
.

Gemäß dieser Standardregel fliegt ein Kondor, weil die Vorbedingung Bird (Condor) wahr ist und die Rechtfertigung Flies (Condor) nicht im Widerspruch zu dem gegenwärtig Bekannten steht. Im Gegensatz dazu erlaubt Vogel (Pinguin) nicht den Abschluss von Fliegen (Pinguin): Selbst wenn die Vorbedingung des Standard-Vogels (Pinguin) erfüllt ist, stimmt die Begründung Flies (Pinguin) nicht mit dem Bekannten überein. Aus dieser Hintergrundtheorie und diesem Standard kann Bird (Biene) nicht geschlossen werden, da die Standardregel nur das Ableiten von Fliegen (X) von Bird (X) erlaubt, nicht jedoch umgekehrt. Die Vorläufer einer Inferenzregel aus den Konsequenzen abzuleiten, ist eine Form der Erklärung der Konsequenzen und ist das Ziel des abduktiven Denkens.

Eine gängige Standardannahme ist, dass das, was nicht als wahr bekannt ist, als falsch angesehen wird. Dies ist als die Annahme der geschlossenen Welt bekannt und wird in der Standardlogik unter Verwendung eines Standardwerts wie dem folgenden für jede Tatsache F formalisiert.

Beispielsweise verwendet die Computersprache Prolog eine Art Standardannahme, wenn Negation behandelt wird: Wenn ein negatives Atom nicht als wahr nachgewiesen werden kann, wird angenommen, dass es falsch ist. Beachten Sie jedoch, dass Prolog die sogenannte Negation als Fehlschlag verwendet: wenn der Interpreter das Atom auswerten muss  versucht es zu beweisen, dass F wahr ist, und schließt daraus  ist wahr, wenn es fehlschlägt. In der Standardlogik stattdessen eine Standardeinstellung  als Begründung kann nur angewendet werden, wenn  stimmt mit dem aktuellen Wissen überein.

Beschränkungen
Eine Standardeinstellung ist kategorial oder voraussetzungsfrei, wenn sie keine Voraussetzung hat (oder, wenngleich ihre Voraussetzung tautologisch ist). Ein Standardwert ist normal, wenn er eine einzige Begründung hat, die seiner Schlussfolgerung entspricht. Ein Standardwert ist übermäßig, wenn er sowohl kategorial als auch normal ist. Eine Standardeinstellung ist seminormal, wenn alle ihre Begründung zu ihrer Schlussfolgerung führt. Eine Standardtheorie wird als kategorial, normal, supernormal oder seminormal bezeichnet, wenn alle darin enthaltenen Standardwerte kategorial, normal, supernormal oder seminormal sind.

Semantik der Standardlogik
Eine Standardregel kann auf eine Theorie angewendet werden, wenn ihre Vorbedingung sich aus der Theorie ergibt und ihre Begründung mit der Theorie übereinstimmt. Die Anwendung einer Standardregel fügt der Theorie ihre Konsequenz hinzu. Andere Standardregeln können dann auf die resultierende Theorie angewendet werden. Wenn die Theorie so ist, dass kein anderer Standard angewendet werden kann, wird die Theorie als Erweiterung der Standardtheorie bezeichnet. Die Standardregeln können in unterschiedlicher Reihenfolge angewendet werden. Dies kann zu unterschiedlichen Erweiterungen führen. Das Nixon-Beispiel ist eine Standardtheorie mit zwei Erweiterungen:

Da Nixon sowohl Republikaner als auch Quäker ist, können beide Standardeinstellungen angewendet werden. Die Anwendung des ersten Standardwerts führt jedoch zu der Schlussfolgerung, dass Nixon kein Pazifist ist, wodurch der zweite Standardwert nicht anwendbar ist.Auf die gleiche Weise wird bei der Anwendung des zweiten Standardwerts festgestellt, dass Nixon ein Pazifist ist, wodurch der erste Standardwert nicht anwendbar ist. Diese bestimmte Standardtheorie hat daher zwei Erweiterungen, eine, bei der Pacifist (Nixon) wahr ist, und eine, bei der Pacifist (Nixon) falsch ist.

Die ursprüngliche Semantik der Standardlogik basierte auf dem Festpunkt einer Funktion. Das Folgende ist eine äquivalente algorithmische Definition. Wenn ein Standard Formeln mit freien Variablen enthält, wird davon ausgegangen, dass er die Menge aller Standardwerte darstellt, die erhalten werden, indem allen diesen Variablen ein Wert zugewiesen wird. Ein Standard  gilt für eine Satztheorie T wenn  und alle Theorien  sind konsistent. Die Anwendung dieser Vorgabe auf T führt zur Theorie  . Eine Erweiterung kann durch Anwenden des folgenden Algorithmus generiert werden:

T=W           /* current theory */
A=0           /* set of defaults applied so far */
 
              /* apply a sequence of defaults */
while there is a default d that is not in A and is applicable to T
  add the consequence of d to T
  add d to A
 
              /* final consistency check */
if 
  for every default d in A
    T is consistent with all justifications of d
then
  output T

Dieser Algorithmus ist nicht deterministisch, da alternativ mehrere Standardwerte auf eine gegebene Theorie T angewendet werden können. Im Beispiel von Nixon Diamond führt die Anwendung des ersten Standardwerts zu einer Theorie, auf die der zweite Standardwert nicht angewendet werden kann, und umgekehrt. Als Ergebnis werden zwei Erweiterungen generiert: eine, bei der Nixon ein Pazifist ist, und eine, bei der Nixon kein Pazifist ist.

Die abschließende Überprüfung der Konsistenz der Begründungen aller angewendeten Standardwerte impliziert, dass einige Theorien keine Erweiterungen haben. Dies geschieht insbesondere immer dann, wenn diese Prüfung für jede mögliche Folge von anwendbaren Vorgaben fehlschlägt. Die folgende Standardtheorie hat keine Erweiterung:

Schon seit  ist im Einklang mit der Hintergrundtheorie, kann der Standardwert angewendet werden, was zu dem Schluss führt, dass  ist falsch. Dieses Ergebnis unterminiert jedoch die Annahme, die für die Anwendung des ersten Ausfalls getroffen wurde. Folglich hat diese Theorie keine Erweiterungen.

In einer normalen Standardtheorie sind alle Standardwerte normal: Jeder Standardwert hat das Formular  . Eine normale Standardtheorie hat garantiert mindestens eine Erweiterung.Darüber hinaus sind die Erweiterungen einer normalen Standardtheorie gegenseitig inkonsistent, dh miteinander inkonsistent.

Entailment
Eine Standardtheorie kann null, eine oder mehrere Erweiterungen haben. Die Inanspruchnahme einer Formel aus einer Standardtheorie kann auf zwei Arten definiert werden:

Skeptisch
Eine Formel beinhaltet eine Standardtheorie, wenn sie durch alle ihre Erweiterungen mit einbezogen wird.

Leichtgläubig
Eine Formel beinhaltet eine Standardtheorie, wenn sie mindestens eine ihrer Erweiterungen enthält.

Daher hat die Nixon-Diamantbeispieltheorie zwei Erweiterungen, eine, bei der Nixon ein Pazifist ist und eine, bei der er kein Pazifist ist. Folglich sind weder Pacifist (Nixon) noch ¬Pacifist (Nixon) skeptisch, während beide leichtgläubig sind. Wie dieses Beispiel zeigt, sind die glaubwürdigen Konsequenzen einer Standardtheorie möglicherweise inkonsistent.

Alternative Standard-Inferenzregeln
Die folgenden alternativen Inferenzregeln für die Standardlogik basieren alle auf derselben Syntax wie das ursprüngliche System.

Gerechtfertigt
unterscheidet sich von der ursprünglichen dahingehend, dass ein Standardwert nicht angewendet wird, wenn dadurch die Menge T mit einer Begründung eines angewendeten Standardwerts unvereinbar wird;

Prägnant
Eine Standardeinstellung wird nur angewendet, wenn ihre Konsequenz nicht bereits von T (die genaue Definition ist komplizierter als diese; dies ist nur die Hauptidee dahinter);

Eingeschränkt
Ein Standardwert wird nur angewendet, wenn der Satz aus der Hintergrundtheorie, den Begründungen aller angewendeten Standardwerte und den Folgen aller angewendeten Standardwerte (einschließlich dieser) konsistent ist.

Rational
ähnlich einer eingeschränkten Standardlogik, aber die Folge des hinzuzufügenden Standardwerts wird bei der Konsistenzprüfung nicht berücksichtigt.

Vorsichtig
Standardwerte, die angewendet werden können, aber miteinander in Konflikt stehen (wie im Beispiel des Nixon-Diamanten), werden nicht angewendet.

Die begründeten und eingeschränkten Versionen der Inferenzregel weisen jeder Standardtheorie mindestens eine Erweiterung zu.

Varianten der Standardlogik
Die folgenden Varianten der Standardlogik unterscheiden sich sowohl in der Syntax als auch in der Semantik von der ursprünglichen.

Assertional-Varianten
Eine Behauptung ist ein Paar  bestehend aus einer Formel und einem Satz von Formeln. Ein solches Paar zeigt an, dass p während der Formeln wahr ist wurden als konsistent angenommen, um zu beweisen, dass p wahr ist. Eine Assertional-Default-Theorie besteht aus einer Assertional-Theorie (einem Satz von Assertional-Formeln), die als Hintergrundtheorie bezeichnet wird, und einem Satz von Defaults, die wie in der Originalsyntax definiert sind. Immer, wenn eine Behauptungstheorie auf eine Behauptungstheorie angewandt wird, wird das aus der Konsequenz und ihren Begründungen zusammengesetzte Paar der Theorie hinzugefügt. Die folgende Semantik verwendet Assertional Theorien:

Kumulative Standardlogik
Verpflichtung zu den Annahmen-Standardlogik
Quasi-Standardlogik

Schwache Erweiterungen
Anstatt zu prüfen, ob die Vorbedingungen in der aus der Hintergrundtheorie zusammengesetzten Theorie und den Folgen der angewendeten Standardwerte gültig sind, werden die Vorbedingungen auf Gültigkeit in der zu generierenden Erweiterung geprüft. Mit anderen Worten, der Algorithmus zum Erzeugen von Erweiterungen beginnt mit dem Erraten einer Theorie und deren Verwendung anstelle der Hintergrundtheorie. Was aus dem Prozess der Erweiterungserzeugung resultiert, ist tatsächlich nur eine Erweiterung, wenn sie der anfangs vermuteten Theorie entspricht. Diese Variante der Standardlogik bezieht sich prinzipiell auf die autoepistemische Logik, wo eine Theorie vorliegt  hat das Modell, in dem x nur deshalb wahr ist, vorausgesetzt  wahr, die Formel  unterstützt die ursprüngliche Annahme.

Disjunktive Standardlogik
Die Konsequenz eines Standardwerts ist eine Menge von Formeln anstelle einer einzelnen Formel.Immer wenn der Standard angewendet wird, wird mindestens eine der Folgen nicht deterministisch ausgewählt und erfüllt.

Prioritäten bei den Standardwerten
Die relative Priorität der Standardwerte kann explizit angegeben werden. Von den Standardwerten, die auf eine Theorie anwendbar sind, kann nur eine der am meisten bevorzugten verwendet werden.Bei einigen Semantiken der Standardlogik müssen Prioritäten nicht explizit angegeben werden.vielmehr werden spezifischere Voreinstellungen (die in weniger Fällen anwendbar sind) gegenüber weniger spezifischen bevorzugt.

Statistische Variante
Ein statistischer Standardwert ist ein Standardwert mit einer angehängten oberen Grenze für die Fehlerhäufigkeit. Mit anderen Worten, es wird angenommen, dass der Standardwert höchstens in dem Bruchteil der Fälle, in dem er angewendet wird, eine falsche Inferenzregel ist.

Übersetzungen
Standardtheorien können in andere Logiken in Theorien übersetzt werden und umgekehrt. Die folgenden Bedingungen für Übersetzungen wurden berücksichtigt:

Konsequenzerhaltend
die ursprünglichen und die übersetzten Theorien haben die gleichen (propositionellen) Folgen;

Treu
Diese Bedingung macht nur Sinn, wenn zwischen zwei Varianten der Standardlogik oder zwischen der Standardlogik und einer Logik übersetzt wird, in der ein der Erweiterung ähnliches Konzept vorhanden ist, z. B. Modelle in der modalen Logik. eine Übersetzung ist treu, wenn zwischen den Erweiterungen (oder Modellen) der ursprünglichen und der übersetzten Theorien eine Abbildung (normalerweise eine Zwischenposition) vorhanden ist;

Modular
Eine Übersetzung von der Standardlogik in eine andere Logik ist modular, wenn die Standardwerte und die Hintergrundtheorie separat übersetzt werden können. Darüber hinaus führt das Hinzufügen von Formeln zur Hintergrundtheorie nur dazu, die neuen Formeln zum Ergebnis der Übersetzung hinzuzufügen.

Same-Alphabet
Die ursprünglichen und übersetzten Theorien basieren auf demselben Alphabet.

Polynom
Die Laufzeit der Übersetzung oder die Größe der generierten Theorie müssen ein Polynom in der Größe der ursprünglichen Theorie sein.

Übersetzungen müssen in der Regel treu sein oder zumindest konsequenzerhaltend sein, während die Bedingungen der Modularität und des gleichen Alphabets manchmal ignoriert werden.
Die Übersetzbarkeit zwischen der propositionalen Standardlogik und den folgenden Logiken wurde untersucht:

klassische Satzlogik;
autoepistemische Logik;
propositionale Standardlogik beschränkt auf seminormale Theorien;
alternative Semantik der Standardlogik;
Umschreibung.

Übersetzungen sind vorhanden oder nicht abhängig von den Auflagen. Übersetzungen von der Satzlogik auf die klassische Satzlogik können nicht immer eine Satztheorie in Polynomform erzeugen, es sei denn, die Polynomialhierarchie bricht zusammen. Übersetzungen in autoepistemische Logik existieren oder nicht, je nachdem, ob Modularität oder die Verwendung desselben Alphabets erforderlich ist.

Komplexität
Die rechnerische Komplexität der folgenden Probleme bezüglich der Standardlogik ist bekannt:

Existenz von Erweiterungen
zu entscheiden, ob eine aussagenlogische Standardtheorie mindestens eine Erweiterung hat, ist  -Komplett;

Skeptische Inklusion
zu entscheiden, ob eine aussagenlogische Ausfalltheorie skeptisch eine aussagenlogische Formel beinhaltet, ist  -Komplett;

Gläubige Folgerung
zu entscheiden, ob eine aussagenlogische Ausfalltheorie glaubwürdig eine aussagenlogische Formel beinhaltet  -Komplett;

Erweiterungsprüfung
zu entscheiden, ob eine Satzformel einer Erweiterung einer Satzsatztheorie entspricht, ist  -Komplett;

Modellprüfung
zu entscheiden, ob eine aussagenlogische Interpretation ein Modell einer Erweiterung einer aussagenlogischen Standardtheorie ist, ist  -Komplett.

Implementierungen
Drei Systeme, die Standardlogiken implementieren, sind DeReS, XRay und GADeL