Lógica padrão

A lógica padrão é uma lógica não monotônica proposta por Raymond Reiter para formalizar o raciocínio com suposições default.

A lógica padrão pode expressar fatos como “por padrão, algo é verdadeiro”; Por outro lado, a lógica padrão só pode expressar que algo é verdadeiro ou que algo é falso. Isso é um problema porque o raciocínio geralmente envolve fatos que são verdadeiros na maioria dos casos, mas nem sempre.Um exemplo clássico é: “pássaros normalmente voam”. Esta regra pode ser expressa na lógica padrão por “todos os pássaros voam”, o que é inconsistente com o fato de que os pingüins não voam, ou “todas as aves que não são pinguins e não avestruzes e … voam”, o que requer exceções à regra a ser especificada. A lógica padrão visa formalizar regras de inferência como essa sem mencionar explicitamente todas as suas exceções.

Sintaxe da lógica padrão
Uma teoria padrão é um par  . W é um conjunto de fórmulas lógicas, chamado de teoria de fundo, que formaliza os fatos que são conhecidos com certeza. D é um conjunto de regras padrão, sendo cada uma delas da forma:

De acordo com esse padrão, se acreditarmos que o pré-requisito é verdadeiro e cada um  é consistente com nossas crenças atuais, somos levados a acreditar que a conclusão é verdadeira.

As fórmulas lógicas em W e todas as fórmulas em um padrão foram originalmente assumidas como fórmulas lógicas de primeira ordem, mas elas podem ser, potencialmente, fórmulas em uma lógica formal arbitrária. O caso em que são fórmulas na lógica proposicional é um dos mais estudados.

Exemplos
A regra padrão “os pássaros normalmente voam” é formalizada pelo seguinte padrão:

Esta regra significa que, se X é um pássaro, e pode-se supor que voa, então podemos concluir que ele voa. Uma teoria de fundo contendo alguns fatos sobre aves é a seguinte:
.

De acordo com essa regra padrão, um condor voa porque a precondição Bird (Condor) é verdadeira e a justificação Flies (Condor) não é inconsistente com o que é atualmente conhecido. Pelo contrário, Bird (Penguin) não permite concluir Flies (Penguin): mesmo que a pré-condição do padrão Bird (Penguin) seja verdadeira, a justificativa Flies (Penguin) é inconsistente com o que é conhecido.A partir dessa teoria de background e desse padrão, Bird (Bee) não pode ser concluído porque a regra padrão permite apenas derivar Flies (X) de Bird (X), mas não vice-versa. Derivar os antecedentes de uma regra de inferência das conseqüências é uma forma de explicação das conseqüências, e é o objetivo do raciocínio abdutivo.

Uma suposição padrão comum é que o que não é conhecido como verdadeiro é considerado falso.Isso é conhecido como a Hipótese do Mundo Fechado e é formalizado na lógica padrão usando um padrão como o seguinte para cada fato F.

Por exemplo, a linguagem de computador Prolog usa um tipo de suposição padrão ao lidar com a negação: se um átomo negativo não puder ser provado como verdadeiro, então é assumido como falso. Note, no entanto, que o Prolog usa a chamada negação como falha: quando o intérprete tem que avaliar o átomo  , tenta provar que F é verdadeiro e conclui que  é verdade se falhar. Na lógica padrão, em vez disso, um padrão  como justificativa só pode ser aplicada se é consistente com o conhecimento atual.

Restrições
Um padrão é categórico ou livre de pré-requisito, se não tiver pré-requisito (ou, equivalentemente, seu pré-requisito é tautológico). Um padrão é normal se tiver uma única justificação equivalente à sua conclusão. Um padrão é supernormal se for categórico e normal. Um padrão é seminormal se todas as suas justificações implicarem sua conclusão. Uma teoria padrão é chamada de categórica, normal, supernormal ou seminormal se todos os padrões que ela contém forem categóricos, normais, supernormais ou seminormais, respectivamente.

Semântica da lógica padrão
Uma regra padrão pode ser aplicada a uma teoria se sua pré-condição for imposta pela teoria e suas justificativas forem todas consistentes com a teoria. A aplicação de uma regra padrão leva à adição de sua consequência à teoria. Outras regras padrão podem então ser aplicadas à teoria resultante. Quando a teoria é tal que nenhum outro padrão pode ser aplicado, a teoria é chamada de extensão da teoria padrão. As regras padrão podem ser aplicadas em ordem diferente, e isso pode levar a extensões diferentes. O exemplo do diamante Nixon é uma teoria padrão com duas extensões:

Como Nixon é tanto um republicano quanto um Quaker, ambos os padrões podem ser aplicados. No entanto, aplicar o primeiro padrão leva à conclusão de que Nixon não é pacifista, o que torna o segundo padrão não aplicável. Da mesma forma, aplicando o segundo padrão, obtemos que Nixon é um pacifista, tornando assim o primeiro padrão não aplicável. Essa teoria padrão em particular tem, portanto, duas extensões, uma na qual Pacifist (Nixon) é verdadeira, e uma na qual Pacifist (Nixon) é falsa.

A semântica original da lógica padrão foi baseada no ponto fixo de uma função. A seguir, uma definição algorítmica equivalente. Se um padrão contiver fórmulas com variáveis ​​livres, considera-se que representa o conjunto de todos os padrões obtidos, dando um valor a todas essas variáveis. Um padrão  é aplicável a uma teoria proposicional T se  e todas as teorias  são consistentes. A aplicação desse padrão em T leva à teoria . Uma extensão pode ser gerada aplicando o seguinte algoritmo:

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

Esse algoritmo não é determinístico, pois vários padrões podem ser aplicados alternativamente a uma dada teoria T. No exemplo do diamante de Nixon, a aplicação do primeiro padrão leva a uma teoria na qual o segundo padrão não pode ser aplicado e vice-versa. Como resultado, duas extensões são geradas: uma em que Nixon é um pacifista e outra em que Nixon não é pacifista.

A verificação final da consistência das justificações de todos os padrões que foram aplicados implica que algumas teorias não têm extensões. Em particular, isso acontece sempre que essa verificação falha para todas as possíveis sequências de padrões aplicáveis. A seguinte teoria padrão não tem extensão:

Desde a  é consistente com a teoria de fundo, o padrão pode ser aplicado, levando à conclusão de que  é falso. No entanto, esse resultado enfraquece a suposição de que foi aplicado o primeiro padrão. Consequentemente, esta teoria não tem extensões.

Em uma teoria padrão normal, todos os padrões são normais: cada padrão tem o formulário  . Uma teoria normal padrão é garantida para ter pelo menos uma extensão. Além disso, as extensões de uma teoria normal padrão são mutuamente inconsistentes, isto é, inconsistentes entre si.

Entailment
Uma teoria padrão pode ter zero, uma ou mais extensões. O comprometimento de uma fórmula de uma teoria padrão pode ser definido de duas maneiras:

Cético
uma fórmula é implicada por uma teoria padrão, se for implicada por todas as suas extensões;

Crédulo
uma fórmula é implicada por uma teoria padrão, se for implicada por pelo menos uma de suas extensões.

Assim, a teoria do exemplo do diamante de Nixon tem duas extensões, uma na qual Nixon é um pacifista e uma na qual ele não é um pacifista. Consequentemente, nem Pacifist (Nixon) nem ¬ Pacifist (Nixon) são céticos, enquanto ambos são credulamente implicados. Como este exemplo mostra, as conseqüências crédulas de uma teoria padrão podem ser inconsistentes entre si.

Regras alternativas de inferência padrão
As seguintes regras de inferência alternativas para lógica padrão são todas baseadas na mesma sintaxe do sistema original.

Justificado
difere do original em que um padrão não é aplicado se, desse modo, o conjunto T se tornar inconsistente com uma justificativa de um padrão aplicado;

Conciso
um padrão é aplicado apenas se sua consequência já não estiver relacionada a T (a definição exata é mais complicada que essa; essa é apenas a idéia principal por trás dela);

Constrangido
um padrão é aplicado somente se o conjunto composto pela teoria de segundo plano, as justificativas de todos os padrões aplicados e as conseqüências de todos os padrões aplicados (incluindo este) for consistente;

Racional
semelhante à lógica padrão restrita, mas a conseqüência do padrão a ser adicionado não é considerada na verificação de consistência;

Cauteloso
padrões que podem ser aplicados, mas estão em conflito entre si (como os do exemplo do diamante de Nixon) não são aplicados.

As versões justificadas e restritas da regra de inferência atribuem pelo menos uma extensão a toda teoria padrão.

Variantes da lógica padrão
As seguintes variantes da lógica padrão diferem da original na sintaxe e na semântica.

Variantes Assercionais
Uma afirmação é um par  composto de uma fórmula e um conjunto de fórmulas. Esse par indica que p é verdadeiro enquanto as fórmulas  foram assumidos consistentes para provar que p é verdadeiro. Uma teoria de default assertiva é composta de uma teoria assertiva (um conjunto de fórmulas assercionais) chamada teoria de fundo e um conjunto de padrões definidos como na sintaxe original. Sempre que um padrão é aplicado a uma teoria de asserção, o par composto de sua consequência e seu conjunto de justificações é adicionado à teoria. A semântica a seguir usa teorias de asserção:

Lógica Padrão Cumulativa
Compromisso com a lógica padrão de suposições
Lógica quase-padrão

Extensões fracas
em vez de verificar se as pré-condições são válidas na teoria composta pela teoria de base e as consequências dos padrões aplicados, as pré-condições são verificadas quanto à validade na extensão que será gerada; em outras palavras, o algoritmo para gerar extensões começa por adivinhar uma teoria e usá-la no lugar da teoria de fundo; o que resulta do processo de geração de extensão é, na verdade, uma extensão apenas se for equivalente à teoria adivinhada no início. Esta variante da lógica padrão está relacionada, em princípio, à lógica autoepistêmica, em que uma teoria  tem o modelo em que x é verdadeiro apenas porque, assumindo verdade, a fórmula  suporta a suposição inicial.

Lógica padrão disjuntiva
a conseqüência de um padrão é um conjunto de fórmulas em vez de uma única fórmula. Sempre que o padrão é aplicado, pelo menos uma de suas consequências é escolhida não-deterministicamente e se torna verdadeira.

Prioridades nos padrões
a prioridade relativa dos padrões pode ser explicitamente especificada; Entre os padrões aplicáveis ​​a uma teoria, apenas um dos mais preferidos pode ser aplicado. Algumas semânticas da lógica padrão não exigem que as prioridades sejam explicitamente especificadas; em vez disso, padrões mais específicos (aqueles que são aplicáveis ​​em menos casos) são preferidos aos menos específicos.

Variante estatistica
um padrão é um padrão com um limite superior anexado em sua frequência de erro; Em outras palavras, o padrão é considerado uma regra de inferência incorreta em no máximo essa fração de vezes que é aplicada.

Traduções
As teorias padrão podem ser traduzidas em teorias em outras lógicas e vice-versa. As seguintes condições nas traduções foram consideradas:

Preservação de Consequências
as teorias original e traduzida têm as mesmas conseqüências (proposicionais);

Fiel
essa condição só faz sentido ao traduzir entre duas variantes da lógica padrão ou entre a lógica padrão e uma lógica na qual existe um conceito similar à extensão, por exemplo, modelos na lógica modal; uma tradução é fiel se houver um mapeamento (tipicamente, uma bijeção) entre as extensões (ou modelos) das teorias original e traduzida;

Modular
uma tradução da lógica padrão para outra lógica é modular se os padrões e a teoria de segundo plano puderem ser traduzidos separadamente; além disso, o acréscimo de fórmulas à teoria de fundo apenas leva a adicionar as novas fórmulas ao resultado da tradução;

Mesmo alfabeto
as teorias original e traduzida são construídas no mesmo alfabeto;

Polinomial
o tempo de execução da tradução ou o tamanho da teoria gerada são obrigados a serem polinomiais no tamanho da teoria original.

Normalmente, as traduções são obrigadas a ser fiéis ou, pelo menos, a preservar as conseqüências, enquanto as condições de modularidade e o mesmo alfabeto são, às vezes, ignoradas.
A tradutibilidade entre a lógica padrão proposicional e as seguintes lógicas foram estudadas:

lógica proposicional clássica;
lógica autoepistêmica;
lógica default proposicional restrita a teorias seminormais;
semântica alternativa da lógica padrão;
circunscrição.

Traduções existem ou não dependendo de quais condições são impostas. Traduções da lógica padrão proposicional para a lógica proposicional clássica nem sempre podem gerar uma teoria proposicional de tamanho polinomial, a menos que a hierarquia polinomial entre em colapso. As traduções para a lógica autoepistêmica existem ou não dependendo se a modularidade ou o uso do mesmo alfabeto é necessário.

Complexidade
A complexidade computacional dos seguintes problemas sobre a lógica padrão é conhecida:

Existência de extensões
decidir se uma teoria padrão proposicional tem pelo menos uma extensão é  -completo;

Envolvimento cético
decidir se uma teoria proposicional padrão implica uma fórmula proposicional é  -completo;

Implicação de credulidade
decidir se uma teoria padrão proposicional implica credulamente uma fórmula proposicional é  -completo;

Verificação de extensão
decidir se uma fórmula proposicional é equivalente a uma extensão de uma teoria padrão proposicional é  -completo;

Verificação do modelo
decidir se uma interpretação proposicional é um modelo de uma extensão de uma teoria proposicional padrão é  -completo.

Implementações
Três sistemas que implementam lógicas padrão são DeReS, XRay e GADeL