# Lógica default

A lógica default é uma lógica não-monotônica proposta por Raymon Reiter para formalizar o raciocínio com suposições defaults.
A lógica default pode expressar fatos como "por default, algo é verdadeiro"; por outro lado, a lógica clássica só pode expressar que algo é verdade ou que algo é falso. Esse é um problema porque o raciocínio, em muitos casos, envolve fatos que são conhecidos como verdadeiros na maioria dos casos. Um exemplo clássico é: "pássaros tipicamente voam". Essa regra pode ser expressada na lógica clássica ou por "todos os pássaros voam", o que é inconsistente com o fato de que pinguins não voam, ou por "todos os pássaros que não são pinguins e não são avestruzes e... voam", o que requere todas as exceções das regras à ser especificadas. Lógica Default tenta formalizar regras de inferência como esta sem mencionar explicitamente todas suas exceções.

## Sintaxe da Lógica Default

Uma teoria Default é um par $\langle W,D\rangle$. $W$ é um conjunto de fórmulas lógicas, chamado de a teoria de fundo, que formaliza os fatos que são conhecidos com certeza. $D$ é um conjunto de regras defaults, cada uma do seguinte formato:
    ${\frac {{\text{Pré-Requisito: Justificativa}}_{1},\dots ,{\text{Justificativa}}_{n}}{\text{Conclusão}}}$
De acordo com esse default, acreditamos que ${\text{Pré-Requisito}}$ é verdade, e que cada uma de $Justificativa_{i}$ é consistente com nossa crença atual, então somos levados à acreditar que ${\text{Conclusão}}$ é verdade.
As fórmulas lógicas em $W$ e todas as fórmulas em um default são originalmente supostas como fórmulas de lógica de primeira ordem, mas elas podem ser fórmulas em uma lógica formal arbitrária. O caso no qual elas são fórmulas em lógica proposicional é um dos mais estudados.

## Exemplos

A regra Default "pássaros tipicamente voam" é formalizada pelo seguinte Default:
    $D=\left\{{\frac {Bird(X):Flies(X)}{Flies(X)}}\right\}$
Essa regra significa que, se $X$ é um pássaro, e pode se assumir que ele voa, então podemos concluir que X voa. A teoria de fundo contendo alguns fa(c)tos sobre pássaros é a seguinte:
    $W=\{Bird(Condor),Bird(Pinguim),\neg Flies(Pinguim),Flies(Abelha)\}$.
De acordo com essa regra default, um condor voa porque o pré-requisito $Bird(Condor)$ é verdade e a justificativa $Flies(Condor)$ não é inconsistente com e que sabemos até agora. Contrariamente, $Bird(Pinguim)$ não permite que concluamos $Flies(Pinguim)$: mesmo que o prérequisito do default $Bird(Pinguim)$ seja verdade, a justificativa $Flies(Pinguim)$ é inconsistente com o que é conhecido.
Dessa teoria de fundo e desse default, $Bird(Abelha)$ não pode ser concluido porque a regra default permite apenas derivar $Flies(X)$ de $Bird(X)$, mas não o contrário. Derivar os antecedentes de uma regra de inferência de suas consequências é uma forma de explicar as consequências e o objetivo do raciocínio abdutivo.
Uma suposição default comum é que aquilo que não é conhecido como verdade é acreditado como falso. Isso é conhecido como a suposição de mundo fechado, e é formalizada na lógica default usando um default como o seguinte para todo o fa(c)to $F$.
    ${\frac {:{\neg }F}{{\neg }F}}$
Por exemplo, a linguagem de programação Prolog usa um tipo de suposição default quando trabalhando com negação: se uma atômica negada não pode ser provada verdadeira, então é assumida como falsa.
Nota-se, porém, que Prolog usa a tão chamada negação como falha: quando o interpretador tem que valorar a atômica $\neg F$, ele tenta provar que $F$ é verdade, e concluir que $\neg F$ é verdade caso falha. Na lógica default , pelo contrário, um default contendo $\neg F$ como justificativa só pode ser aplicado se $\neg F$ é consistente com o conhecimento atual.

### Restrições

Um default é categórico ou livre de pré-requisitos se não tem pré-requisitos (ou, equivalente, seu pré-requisito [e tautológico). Um default é normal se tem apenas uma justificativa que é equivalente à sua conclusão. Um default é super normal se é tanto categórico como normal. Um default é seminormal, se todas suas justificativas acarretam sua conclusão. Uma teoria default é chamada categórica, normal, super normal ou seminormal, se todos os defaults contidos são categóricos, normais, super normais ou seminormais, respectivamente.

## Semântica da lógica default

Uma regra default pode ser aplicada à uma teoria se seu pré-requisito é acarretado pela teoria e suas justificativas são todas consistentes com a teoria. A aplicação de uma regra default leva à adição de sua consequência para a teoria. Outras regras defaults podem então ser aplicadas à teoria resultante. Quando a teoria está em um estado em que nenhum outro default pode ser aplicado, a teoria é chamado uma extensão da teoria default. As regras defaults podem ser aplicadas em ordem diferentes, e isso pode levar à diferentes extensões. O exemplo do diamante de Nixon é uma teoria default com duas extensões:
    $\left\langle \left\{{\frac {Republicano(X):\neg Pacifista(X)}{\neg Pacifista(X)}},{\frac {Quacre(X):Pacifista(X)}{Pacifista(X)}}\right\},\left\{Republicano(Nixon),Quacre(Nixon)\right\}\right\rangle$
Como Nixon é tanto um republicano quanto um Quacre, os dois defaults podem ser aplicados. Porém, aplicar o primeiro default leva à conclusão que Nixon não é pacifista, o que torna o segundo default não-aplicável. Do mesmo modo, aplicando primeiramente o segundo default obtemos que Nixon é um pacifista, fazendo o primeiro default não aplicável. Essa particular teoria default então tem duas extensões, uma em que $Pacifist(Nixon)$ é verdadeira, e uma na qual $Pacifist(Nixon)$ é falsa.
As semânticas originais da lógica default são baseadas no ponto fixo de uma função. O seguinte é uma definição algorítmica equivalente. Se um default contém fórmulas com variáveis livres, ele é considerado como representação do conjunto de todos os defaults obtidos dando um valor para todas essas variáveis. Um default ${\frac {\alpha :\beta _{1},\ldots ,\beta _{n}}{\gamma }}$ é aplicável à teoria proposicional $T$ se $T\models \alpha$ e todas as teorias $T\cup \{\beta _{i}\}$ são consistentes. A aplicação desse default em $T$ Leva à teoria $T\cup \{\gamma \}$. Uma extensão pode ser criada aplicando-se o algoritmo a seguir:
Esse algoritmo é não-determinístico, já que vários outros defaults podem ser aplicados à uma dada teoria $T$. No exemplo do diamante de Nixon, a aplicação do primeiro default leva à uma teoria em que o segundo default não é aplicável e vice-versa. Como resultado, as duas extensões são criadas, uma na qual Nixon é pacifista e uma na qual Nixon não é pacifista.
A verificação final de consistências das justificativas de todos os defaults que foram aplicados implica que algumas teorias não tem nenhuma extensão. Em particular, isso acontece quando a verificação falha para toda sequência possível de defaults aplicados. A teoria default a seguir não tem extensão:
    $\left\langle \left\{{\frac {:A(b)}{\neg A(b)}}\right\},\emptyset \right\rangle$
Como $A(b)$ é consistente com a teoria de fundo, o default pode ser aplicado, levando à conclusão de que $A(b)$ é falsa. Esse resultado porém enfraquece a suposição que foi feita para a aplicação do primeiro default. Consequentemente, a teoria não tem extensões.
Em uma teoria padrão normal, todos os defaults são normais: cada default tem a forma ${\frac {\phi :\psi }{\psi }}$. Uma teoria default normal é garantida à ter pelo menos uma extensão. Além disso, as extensões de uma teoria normal default são mutalmente inconsistentes, i.e, inconsistente uma com as outras.

### Acarretamento

Uma teoria default pode ter zero, uma ou mais extensões. Acarretamento de uma fórmula de uma teoria default pode ser definido de duas maneiras:

#### Cético

    a fórmula é acarretada por uma teoria default se é acarretada por todas suas extensões;

#### Crédula

    a fórmula é acarretada por uma teoria default se é acarretada por pelo menos uma de suas extensões.
Então, o exemplo do diamante de Nixon tem duas extensões, uma na qual Nixon é pacifista e uma na qual ele não é pacifista. Consequentemente, nem $Pacifist(Nixon)$ nem $\neg Pacifist(Nixon)$ são ceticamente acarretadas, enquanto ambas são credulamente acarretadas. Como esse exemplo mostra, as consequências crédulas de uma teoria default podem ser inconsistentes uma com as outras.

### Regras de Inferência Default Alternativas

As seguintes regras de inferência default alternativas são todas baseadas na mesma sintaxe do sistema original.

#### Justificadas

    diferem do original no fa(c)to de que um default não é aplicada se assim o conjunto $T$ fica inconsistente com a justificativa de um default aplicado;

#### Concisas

    um default é aplicado apenas se sua consequência não já é acarretada por $T$ (a definição exata é mais complicada que essa; isso é apenas a ideia principal por trás do conceito);

#### Restringida

    um default é aplicado apenas se o conjunto composto da teoria de fundo, as justificativas de todos os defaults já aplicados, e as consequências de todos os defaults já aplicados (incluindo este) é consistente;

#### Racional

    similar à lógica default restringida, mas a consequência do default à ser adicionado não é considerado na verificação da consistência;

#### Cauteloso

    defaults que podem ser aplicados mas são conflitantes um com o outro (como aqueles no exemplo do diamante de Nixon) não são aplicados.
As versões justificadas e restringidas da regra de inferência garantem pelo menos uma extensão para toda teoria default.

## Variantes da lógica default

As seguintes variantes da lógica default diferem da original tanto em sintaxe quanto semântica.

### Variantes assertivas

    Uma assertiva é um par $\langle p:\{r_{1},\ldots ,r_{n}\}\rangle$ composto de uma fórmula e um conjunto de fórmulas. Tal par indica que $p$ é verdade enquanto as fórmulas $r_{1},\ldots ,r_{n}$ tem sido assumidas consistentes para provar que $p$ é verdade. Uma teoria default assertiva é composta de uma teoria assertiva (um conjunto de fórmulas assertivas) chamada de teoria de fundo e um conjunto de defaults definidos na sintaxe original. Quando um default é aplicado à uma teoria assertiva, o par composto de sua consequência e seu conjunto de justificativas é adicionado à teoria. As semânticas a seguir usam teorias assertivas:
* Lógica default acumulativa
* Lógica default comprometidas à suposições.
* Lógica quase-default

### Extensões fracas

    em vez de checar se as pré-condições são válidas na teoria composta da teorai de fundo e das consequências dos defaults aplicados, as pré-condições são verificadas por validade na extensão que será gerada; em outras palavras, o algoritmo para gerar extensões começa adivinhando uma teoria e a usando no lugar da teoria de fundo; o que resulta deste processo de geração de extensão é na verdade uma extensão apenas se é equivalente à teoria adivinhada no começo. Essa variante da lógica default é relacionada ao principio da lógica autoepistêmica, onde uma teoria $\Box x\rightarrow x$ tem o modelo no qual $x$ é verdade apenas porque, assumindo $\Box x$ como verdade, a fórmula $\Box x\rightarrow x$ apoia a suposição inicial.

### Lógica default disjuntiva

    a consequência de um default é um conjunto de fórmulas em vez de uma fórmula só. Quando o default é aplicado, pelo menos uma de suas consequências é não-deterministicamente escolhida e valorada como verdade.

### Prioridade em defaults

    a prioridade relativa de defaults pode ser explicitamente especificada; junto dos defaults que são aplicáveis à uma teoria, apenas um dos mais preferidos podem ser aplicados. Algumas semânticas de lógica default não requerem que prioridades sejam explicitamente especificadas; então, defaults mais específicos (aqueles que são aplicáveis em menos casos) são preferidos do que defaults menos específicos.

### Variante estatística

    um default estatístico é um default com um limite superior anexado à sua frequência de erro; em outras palavras, o default é assumido como uma regra de inferência incorreta em no máximo aquela fração de vezes na qual ele é aplicado.

## Traduções

Teorias defaults podem ser traduzidas em teorias de outras lógicas e vice-versa. As condições de traduções a seguir tem sido consideradas:

### Preservação de Consequência

    a teoria original e a traduzida tem a mesma (proposicional) consequência;

### Fiel

    essa condição só faz sentido quando traduzindo entre duas variantes da lógica default ou entre lógica default e uma lógica na qual um conceito similar de extensão existe, como modelos na lógica modal; uma tradução é fiel se existe um mapeamento (tipicamente uma bijeção) entre as extensões (ou modelos) das teorias original e traduzida.

### Modular

    uma tradução de uma lógica default para alguma outra lógica é modular se os defaults e a teoria de fundo podem ser traduzidas separadamente; além disso, a adição de fórmulas a teoria de fundo apneas leva à adição de novas fórmulas ao resultado da tradução;

### Mesmo-Alfabeto

    a teoria original e a traduzida usam o mesmo alfabeto de símbolos.

### Polinomial

    o tempo de execução da tradução ou o tamanho da teoria gerada devem ser polinomiais no tamanho da teoria original.
Traduções tem tipicamente o requisito de serem fiéis ou pelo menos de preservar a consequência, enquanto as condições de modularidade e mesmo alfabeto são às vezes ignoradas.
Características sobre tradução entre lógica default proposicional e as seguintes lógicas tem sido estudadas:
* lógica clássica proposicional;
* lógica auto epistêmica;
* lógica default proposicional restringida à teorias seminormais;
* semânticas alternativas da lógica default;
* circunscrição.
Traduções existem ou não dependendo de quais condições são impostas. Traduções da lógica default proposicional para a lógica clássica proposicional nem sempre podem gerar uma teoria proposicional polinomial, a não ser que a hierarquia polinomial seja descartada. Traduções para a lógica auto epistêmica existem ou não dependendo se modularidade ou o uso do mesmo alfabeto são necessários.

## Complexidade

A complexidade computacional dos seguintes problemas sobre lógica default são conhecidas:

### Existência de extensões

    decidir se uma teoria default proposicional tem pelo menos uma extensão é $\Sigma _{2}^{P}$-completo;

### Acarretamento Cético

    decidir se uma teoria default proposicional ceticamente acarreta uma fórmula proposicional é $\Pi _{2}^{P}$-completo;

### Acarretamento Crédulo

    decidir se uma teoria default proposicional credulamente acarreta uma fórmula proposicional é $\Sigma _{2}^{P}$-completo;

### Verificação de Extensão

    decidir se uma fórmula proposicional é equivalente à uma extensão de uma teoria default proposicional é $\Delta _{2}^{P[log]}$-completo;

### Verificação de Modelo

    decidir se uma interpretação proposicional é um modelo de uma extensão de uma teoria default proposicional é $\Sigma _{2}^{P}$-completo.

## Implementações

Três sistemas que implementam lógica default são DeReS, XRay e GADeL