# Lógica autoepistêmica

A lógica autoepistêmica é uma lógica formal para a representação e raciocínio do conhecimento sobre o conhecimento. Enquanto a lógica proposicional pode apenas expressar fatos, a lógica autoepistêmica pode exprimir conhecimento e falta de conhecimento sobre fatos.
A semântica de modelo estável, que é usada para dar semântica à programação lógica com negação por falha, pode ser vista como uma forma simplificada da lógica autoepistêmica.

## Sintaxe

A sintaxe da lógica autoepistêmica estende aquela da lógica proposicional por um operador modal $\Box$ indicando conhecimento: se $F$ é uma fórmula, $\Box F$ indica que $F$ é conhecida. Como consequência, $\Box \neg F$ indica que$\neg F$ é conhecida e$\neg \Box F$ indica que $F$ não é conhecida.
Essa sintaxe é utilizada para permitir raciocínio baseado no conhecimento de fatos. Por exemplo, $\neg \Box F\rightarrow \neg F$ significa que $F$ é assumida como falsa se sua verdade não é conhecida. Isso é uma forma de Negação por falha

## Semântica

A semântica da lógica autoepistêmica é baseado nas expansões de uma teoria, que tem uma função similar à modelos na lógica proposicional. Enquanto um modelo proposicional especifica quais axiomas são verdadeiros e quais são falsos, uma expansão especifica quais formula $\Box F$ é verdade e quais são falsas. Em particular, as expansões de uma fórmula autoepistêmica $T$ faz essa distinção para toda subfórmula $\Box F$ contida em $T$. Essa distinção permite tratar $T$ como uma fórmula proposicional, assim como todas suas subfórmulas contendo $\Box$ são ou verdadeiras ou falsas. Em particular, checar se $T$ acarreta $F$ nessa condição pode ser feita usando as regras de Cálculo Proposicional. Em ordem para algo inicialmente assumido ser uma expansão, teremos que uma subfórmula $F$ é acarretada se e somente se $\Box F$ for inicialmente considerada verdadeira.
Por exemplo, na fórmula $T=\Box x\rightarrow x$, temos apenas uma única "subfórmula em caixa", na qual $\Box x$. Então, temos apenas dois candidatos à expansão, considerando ela verdadeira ou falsa, respectivamente. A verificação de elas serem expansões de fato é a seguinte.
$\Box x$ é falsa : Com essa suposição, $T$ é tautologia, pois $\Box x\rightarrow x$ é equivalente à $\neg \Box x\vee x$, e $\neg \Box x$ é suposta verdade; Logo, $x$ não é acarretada. Esse resultado confirma a suposição implicita em $\Box x$ ser falsa, isto é, que $x$ não é atualmente conhecida. Como resultado, a suposição que $\Box x$ é falsa é uma expansão.
$\Box x$ é verdadeira : Junto dessa suposição, $T$ acarreta $x$; então, a suposição inicial que é implicita em $\Box x$ ser verdade, por exemplo, que $x$ é conhecida à ser verdade, é satisfeita. Como resultado, essa é outra expansão.
A fórmula $T$ tem então duas expansões, uma na qual $x$ não é conhecido e uma na qual é conhecida. A segunda tem sido considerada como não-intuitiva, já que assume-se inicialmente que $\Box x$ ser verdadeira é a única razão pela qual $x$ é verdadeira, o que confirma o que foi assumido. Em outras palavras, o que foi assumido se suporta. Uma lógica que permite tal auto-suporte de crenças é chamada de não suficientemente livre de variáveis para diferenciá-las da lógica livre de variáveis, na qual auto-suporte não é possível. Variantes 'fortemente livre de variáveis' da lógica autoepistêmica existem.

## Generalizações

Em inferência incerta, a dualidade conhecida/desconhecida de valores verdades é substituída por um valor de certeza de um fato ou dedução; certeza pode variar de 0 (completamente desconhecido/incerto) até 1 (certo/conhecido). Em rede de lógica probabilística, valores verdades também são fornecidos uma interpretação probabilística (Como exemplo, valores verdade podem ser incertos, e, mesmo com uma certeza quase total, ainda ser "provavelmente" verdadeiros (ou falsos)).