La logica predefinita è una logica non monotona proposta da Raymond Reiter per formalizzare il ragionamento con ipotesi predefinite.

La logica predefinita può esprimere fatti come « di default, qualcosa è vero »; al contrario, la logica standard può solo esprimere che qualcosa è vero o che qualcosa è falso. Questo è un problema perché il ragionamento spesso coinvolge fatti che sono veri nella maggior parte dei casi ma non sempre. Un esempio classico è: « in genere gli uccelli volano ». Questa regola può essere espressa in logica standard o « tutti gli uccelli volano », il che è incoerente con il fatto che i pinguini non volano, o da « tutti gli uccelli che non sono pinguini e non struzzi e … volare », che richiede tutto eccezioni alla regola da specificare. La logica predefinita mira a formalizzare regole di inferenza come questa senza menzionare esplicitamente tutte le loro eccezioni.

Sintassi della logica predefinita
Una teoria predefinita è una coppia  . W è un insieme di formule logiche, chiamate teoria dello sfondo, che formalizzano i fatti che sono noti con certezza. D è un insieme di regole predefinite, ognuna delle quali è della forma:

Secondo questo default, se crediamo che il Prerequisito sia vero, e ognuno di è coerente con le nostre attuali convinzioni, siamo portati a credere che la Conclusione sia vera.

Le formule logiche in W e tutte le formule in un predefinito erano originariamente considerate come formule logiche del primo ordine, ma possono potenzialmente essere formule in una logica formale arbitraria. Il caso in cui sono formule nella logica proposizionale è uno dei più studiati.

Esempi
La regola predefinita « in genere gli uccelli volano » è formalizzata dal seguente valore predefinito:

Questa regola significa che, se X è un uccello, e si può presumere che voli, allora possiamo concludere che vola. Una teoria di fondo contenente alcuni fatti sugli uccelli è la seguente:
.

Secondo questa regola predefinita, un condor vola perché il precondizionamento Bird (Condor) è vero e la giustificazione Flies (Condor) non è incoerente con ciò che è attualmente noto. Al contrario, Bird (Penguin) non consente la conclusione di Flies (Penguin): anche se la precondizione del default Bird (Penguin) è vera, la giustificazione Flies (Penguin) è incoerente con ciò che è noto. Da questa teoria di fondo e questa impostazione predefinita, Bird (Bee) non può essere concluso perché la regola predefinita consente solo la derivazione di Flies (X) da Bird (X), ma non viceversa. Derivare gli antecedenti di una regola di inferenza dalle conseguenze è una forma di spiegazione delle conseguenze ed è lo scopo del ragionamento abduttivo.

Un’assunzione comune di default è che ciò che non è noto per essere vero è ritenuto falso. Questo è noto come presupposto del mondo chiuso, ed è formalizzato nella logica di default usando un default come il seguente per ogni fatto F.

Ad esempio, il linguaggio informatico Prolog utilizza una sorta di assunto di default quando si tratta di negazione: se un atomo negativo non può essere dimostrato vero, allora si presume che sia falso. Si noti, tuttavia, che Prolog usa la cosiddetta negazione come fallimento: quando l’interprete deve valutare l’atomo  , prova a dimostrare che F è vera, e conclude quello  è vero se fallisce. Nella logica di default, invece, un default ha  come giustificazione può essere applicata solo se  è coerente con le conoscenze attuali.

restrizioni
Un default è categorico o prerequisito-free se non ha alcun prerequisito (o, equivalentemente, il suo prerequisito è tautologico). Un valore predefinito è normale se ha una giustificazione singola equivalente alla sua conclusione. Un valore predefinito è supernormale se è sia categoriale che normale. Un default è seminario se tutte le sue giustificazioni comportano la sua conclusione. Una teoria predefinita è definita categorica, normale, supernormale o seminormale se tutti i valori predefiniti che contiene sono categoriali, normali, supernormali o seminormali, rispettivamente.

Semantica di logica predefinita
Una regola predefinita può essere applicata a una teoria se la sua precondizione è implicata dalla teoria e le sue giustificazioni sono tutte coerenti con la teoria. L’applicazione di una regola predefinita porta all’aggiunta delle sue conseguenze alla teoria. Altre regole predefinite possono quindi essere applicate alla teoria risultante. Quando la teoria è tale che non si può applicare nessun altro valore predefinito, la teoria è chiamata un’estensione della teoria di default. Le regole predefinite possono essere applicate in ordine diverso e ciò potrebbe comportare estensioni diverse. L’esempio di diamante Nixon è una teoria predefinita con due estensioni:

Poiché Nixon è sia un repubblicano che un quacchero, possono essere applicate entrambe le impostazioni predefinite. Tuttavia, l’applicazione del primo default porta alla conclusione che Nixon non è un pacifista, il che rende il secondo predefinito non applicabile. Allo stesso modo, applicando il secondo valore di default otteniamo che Nixon è un pacifista, rendendo così il primo predefinito non applicabile. Questa particolare teoria di default ha quindi due estensioni, una in cui Pacifist (Nixon) è vero, e una in cui Pacifist (Nixon) è falso.

La semantica originale della logica predefinita era basata sul punto fisso di una funzione. Quanto segue è una definizione algoritmica equivalente. Se un valore predefinito contiene formule con variabili libere, viene considerato rappresentare l’insieme di tutti i valori di default ottenuti dando un valore a tutte queste variabili. Un valore predefinito  è applicabile a una teoria proposizionale T se  e tutte le teorie  sono consistenti.L’applicazione di questo valore predefinito a T conduce alla teoria  . Un’estensione può essere generata applicando il seguente algoritmo:

  Teoria corrente T = W / * * /
 A = 0 / * set di valori predefiniti applicati finora * /
 
               / * applica una sequenza di valori predefiniti * /
 mentre c'è un default d che non è in A ed è applicabile a T
   aggiungi la conseguenza di d a T
   aggiungi d ad A
 
               / * controllo di coerenza finale * /
 Se 
   per ogni predefinito d in A
     T è coerente con tutte le giustificazioni di d
 poi
   uscita T

Questo algoritmo non è deterministico, in quanto diverse impostazioni predefinite possono essere applicate in alternativa a una determinata teoria. Nell’esempio del diamante Nixon, l’applicazione del primo valore predefinito porta a una teoria a cui non può essere applicato il secondo valore predefinito e viceversa. Di conseguenza, vengono generate due estensioni: una in cui Nixon è un pacifista e uno in cui Nixon non è un pacifista.

Il controllo finale della coerenza delle giustificazioni di tutti i valori di default che sono stati applicati implica che alcune teorie non hanno alcuna estensione. In particolare, ciò accade ogni volta che questo controllo fallisce per ogni possibile sequenza di valori di default applicabili. La seguente teoria di default non ha estensione:

Da  è coerente con la teoria dello sfondo, il default può essere applicato, portando così alla conclusione che  è falso. Questo risultato mina comunque l’ipotesi che è stata fatta per applicare il primo valore predefinito. Di conseguenza, questa teoria non ha estensioni.

In una normale teoria di default, tutti i valori di default sono normali: ogni default ha il modulo  . Una teoria di default normale è garantita per avere almeno un’estensione. Inoltre, le estensioni di una normale teoria di default sono reciprocamente incoerenti, cioè incoerenti tra loro.

entailment
Una teoria di default può avere zero, una o più estensioni. L’inclusione di una formula da una teoria predefinita può essere definita in due modi:

Scettico
una formula è implicata da una teoria di default se è implicata da tutte le sue estensioni;

credulo
una formula è implicata da una teoria di default se è implicata da almeno una delle sue estensioni.

Quindi, la teoria degli esempi di diamante di Nixon ha due estensioni, una in cui Nixon è un pacifista e uno in cui non è un pacifista. Di conseguenza, né Pacifist (Nixon) né ÌPacifist (Nixon) sono implicati in modo scettico, mentre entrambi sono credulonalmente implicati. Come mostra questo esempio, le credulissime conseguenze di una teoria di default possono essere incoerenti tra loro.

Regole di inferenza predefinite alternative
Le seguenti regole di inferenza alternative per la logica predefinita sono tutte basate sulla stessa sintassi del sistema originale.

giustificato
differisce da quello originale in quanto non viene applicato un valore predefinito se così l’insieme T diventa incoerente con una giustificazione di un default applicato;

Conciso
un default viene applicato solo se la sua conseguenza non è già implicata da T (la definizione esatta è più complicata di questa, questa è solo l’idea principale alla base);

Costretto
un valore predefinito viene applicato solo se l’insieme composto dalla teoria dello sfondo, le giustificazioni di tutti i valori predefiniti applicati e le conseguenze di tutti i valori predefiniti applicati (compreso questo) sono coerenti;

Razionale
simile alla logica di default vincolata, ma la conseguenza del default da aggiungere non è considerata nel controllo di coerenza;

prudente
le impostazioni predefinite che possono essere applicate ma sono in conflitto tra loro (come quelle dell’esempio diamante Nixon) non vengono applicate.

Le versioni giustificate e vincolate della regola di inferenza assegnano almeno un’estensione a ogni teoria predefinita.

Varianti di logica predefinita
Le seguenti varianti di logica predefinita differiscono da quella originale sia sulla sintassi che sulla semantica.

Varianti asserzionali
Un’affermazione è una coppia  composto da una formula e un insieme di formule. Tale coppia indica che p è vero mentre le formule  sono stati assunti coerenti per dimostrare che p è vero. Una teoria di default asserzionale è composta da una teoria asserzionale (un insieme di formule asserzionali) chiamata teoria dello sfondo e un insieme di valori predefiniti definiti nella sintassi originale. Ogni volta che un default viene applicato a una teoria asserzionale, la coppia composta dalle sue conseguenze e dal suo insieme di giustificazioni viene aggiunta alla teoria. Le seguenti semantiche usano teorie asserzionali:

Logica cumulativa predefinita
Impegno alla logica di default delle assunzioni
Logica quasi predefinita

Estensioni deboli
piuttosto che verificare se le precondizioni sono valide nella teoria composta dalla teoria dello sfondo e le conseguenze dei valori predefiniti applicati, le condizioni preliminari vengono verificate per la validità nell’estensione che verrà generata; in altre parole, l’algoritmo per generare estensioni inizia indovinando una teoria e usandola al posto della teoria dello sfondo; ciò che risulta dal processo di generazione dell’estensione è in realtà un’estensione solo se è equivalente alla teoria indovinata all’inizio. Questa variante della logica di default è correlata in linea di principio alla logica autoepistemica, dove una teoria  ha il modello in cui x è vero solo perché, assumendo  vero, la formula  supporta l’ipotesi iniziale.

Logica di default disgiuntiva
la conseguenza di un valore predefinito è un insieme di formule anziché una singola formula. Ogni volta che viene applicato il valore predefinito, almeno una delle sue conseguenze viene scelta in modo non deterministico e resa reale.

Priorità ai valori predefiniti
la priorità relativa dei valori predefiniti può essere specificata esplicitamente; tra i valori predefiniti applicabili a una teoria, solo uno dei più preferiti può essere applicato. Alcune semantiche di logica predefinita non richiedono che vengano specificate esplicitamente priorità; piuttosto, i valori predefiniti più specifici (quelli applicabili in meno casi) sono preferiti rispetto a quelli meno specifici.

Variante statistica
un default statistico è un valore predefinito con un limite superiore attaccato alla sua frequenza di errore; in altre parole, si presume che l’impostazione predefinita sia una regola di inferenza errata al massimo in quella frazione di volte in cui viene applicata.

Traduzioni
Le teorie predefinite possono essere tradotte in teorie in altre logiche e viceversa. Sono state considerate le seguenti condizioni sulle traduzioni:

Conseguenza-Preservare
l’originale e le teorie tradotte hanno le stesse conseguenze (proposizionali);

Fedele
questa condizione ha senso solo quando si traduce tra due varianti della logica predefinita o tra la logica predefinita e una logica in cui esiste un concetto simile all’estensione, ad esempio, i modelli in logica modale; una traduzione è fedele se esiste una mappatura (tipicamente, una biiezione) tra le estensioni (o modelli) delle teorie originali e tradotte;

componibile
una traduzione dalla logica predefinita a un’altra logica è modulare se i valori predefiniti e la teoria dello sfondo possono essere tradotti separatamente; inoltre, l’aggiunta di formule alla teoria dello sfondo porta solo ad aggiungere le nuove formule al risultato della traduzione;

Same-Alphabet
le teorie originali e tradotte sono costruite sullo stesso alfabeto;

Polinomio
il tempo di esecuzione della traduzione o la dimensione della teoria generata devono essere polinomiali nella dimensione della teoria originale.

Le traduzioni sono tipicamente richieste per essere fedeli o almeno per preservare le conseguenze, mentre le condizioni di modularità e lo stesso alfabeto sono a volte ignorate.
La traducibilità tra la logica di default proposizionale e le seguenti logiche sono state studiate:

logica proposizionale classica;
logica autoepistemica;
logica di proposizione predefinita limitata alle teorie seminormali;
semantica alternativa di logica predefinita;
circoscrizione.

Le traduzioni esistono o meno a seconda delle condizioni imposte. Le traduzioni dalla logica proposizionale di default alla logica proposizionale classica non possono sempre generare una teoria proposizionale di dimensioni polinomiali, a meno che la gerarchia polinomiale non collassi. Esistono o meno traduzioni alla logica autoepistemica a seconda che sia richiesta la modularità o l’uso dello stesso alfabeto.

Complessità
La complessità computazionale dei seguenti problemi relativi alla logica predefinita è nota:

Esistenza di estensioni
decidere se una teoria di default proposizionale ha almeno un’estensione  -completare;

Coinvolgimento scettico
decidere se una teoria di default proposizionale implichi scetticamente una formula proposizionale  -completare;

Impegno credulone
decidere se una teoria di asserzione proposizionale è credulariamente una formula proposizionale  -completare;

Controllo dell’estensione
è decidere se una formula proposizionale è equivalente a un’estensione di una teoria di default proposizionale  -completare;

Controllo del modello
decidere se un’interpretazione proposizionale è un modello di un’estensione di una teoria di default proposizionale  -completare.

implementazioni
Tre sistemi che implementano logiche predefinite sono DeReS [link permanente permanente], XRay e GADeL