Semântica de modelo estável

O conceito de modelo estável, ou conjunto de respostas, é usado para definir uma semântica declarativa em programas lógicos com negação por falha. Esta é uma das várias abordagens para o significado da negação na lógica de programação, juntamente com a completude do programa e a semântica bem formada. A semântica de modelo estável é a base da programação de conjunto de resposta.

Motivação

Pesquisas sobre a semântica declarativa da negação na programação em lógica foram motivadas pelo fato de que o comportamento da resolução SLDNF – a generalização da resolução SLD usada pelo Prolog na presença de negação no corpo das regras - não corresponde completamente com as tabelas verdade advindas da lógica proposicional clássica. Considere, por exemplo, o programa

$p\$

$r\leftarrow p,\ q$

$s\leftarrow p,\ {\hbox{not }}q.$

Dado este programa, a consulta $p$ será bem sucedida pois o programa inclui $p$ como fato; a consulta $q$ irá falhar porque não ocorre no início de nenhuma das regras. A consulta $r$ também irá falhar, pois a única regra com $r$ em seu início contém a subquestão $q$ no seu corpo; e como já vimos, esta subquestão irá falhar. Finalmente, a consulta $s$ será bem sucedida, pois cada uma das subquestões $p$, ${\hbox{not }}q$ irão ser bem sucedidas. (A última irá ser bem sucedida pois a questão positiva correspondente $q$ irá falhar). Resumindo, o comportamento da resolução SLDNF no programa dado pode ser representado pelas seguintes atribuições verdade:

$p$ T

$q$ F

$r$ F

$s$ T.

Por outro lado, as regras do programa podem ser vistas como fórmulas proposicionais se nós interpretarmos a vírgula como uma conjunção $\land ,$ e o símbolo ${\hbox{not}}$ como uma negação $\neg ,$ e concordarmos em tratar $F\leftarrow G$ como a implicação $G\rightarrow F$ escrita ao contrário. Por exemplo, a última regra do programa seria, deste ponto de vista, uma notação alternativa para a fórmula proposicional

$p\land \neg q\rightarrow s.$

Se nós calcularmos os valores verdade das regras do programa pelas atribuições verdade mostradas acima, veríamos que cada regra recebe o valor T. Em outras palavras, esta atribuição é um modelo do programa. Mas este programa também possui outros modelos, como por exemplo

$p$ T

$q$ T

$r$ T

$s$ F.

Assim, um dos modelos do programa dado é especial no sentido de que representa corretamente o comportamento da resolução SLDNF. Quais são as propriedades matemáticas deste modelo que o fazem especial? Uma resposta para esta questão é fornecida pela definição de modelo estável.

Relação com a lógica não-monotônica

O significado de negação em programas lógicos está intimamente relacionado a duas teorias do raciocínio não-monotônico – lógica auto-epistêmica e lógica default. A descoberta dessas relações foi um passo fundamental para a invenção da semântica de modelo estável. A sintaxe da lógica auto-epistêmica usa um operador modal que nos permite distinguir o que é verdadeiro do que se acredita. Michael Gelfond [1987] propôs ler ${\hbox{not}}\ p$ no corpo de um regra como “não se acredita em $p$”, e compreender uma regra como a negação da fórmula correspondente da lógica auto-epistêmica. A semântica de modelo estável, na sua forma básica, pode ser vista como uma reformulação dessa ideia de evitar referencias explícitas à lógica auto-epistêmica. Na lógica default, um padrão é similar a uma regra de inferência, com a diferença que ela inclui, além das premissas e da conclusão, uma lista de fórmulas chamadas justificações. Um padrão pode ser usado para obter sua conclusão sob a suposição de que suas justificativas são consistentes com o que é atualmente acreditado. Nicole Bidoit e Christine Froidevaux [1987] propuseram tratar formulas atômicas negadas no corpo de regras como justificações. Por exemplo, a regra

$s\leftarrow p,\ {\hbox{not }}q$

pode ser entendida como o padrão que nos permite derivar $s$ de $p$ assumindo que $\neg p$ é consistente. A semântica de modelo estável utiliza a mesma ideia, mas não se refere explicitamente à lógica padrão.

Modelos Estáveis

A definição de modelo estável abaixo, replicada de [Gelfond and Lifschitz, 1988], usa duas convenções. Primeiramente, associamos uma valoração com o conjunto de fórmulas atômicas que recebem um valor T. Por exemplo, a valoração

$p$ T

$q$ F

$r$ F

$s$ T

é associada com o conjunto $\{p,s\}$. Essa convenção nos permite usar a relação de inclusão do conjunto para comparar valorações umas com as outras. A menor de todas as valorações $\emptyset$ é aquela que torna toda átomo falso. A maior é aquela que deixa todas os átomos como verdadeiro. Posteriormente, um programa lógico com variáveis é visto, de modo abreviado, como o conjunto de todas as instâncias livres de variáveis de suas regras, ou seja, o resultado da substituição de termos sem variáveis por variáveis de acordo com as regras do programa em todas as maneiras possíveis. Por exemplo, a definição em programação lógica dos números pares

$even(0)\$

$even(s(X))\leftarrow {\hbox{not }}even(X)$

é entendida como o resultado da substituição de X nesse programa pelos termos sem variáveis

$0,\ s(0),\ s(s(0)),\dots .$

de todas as maneiras possíveis. O resultado é o programa (livre de variáveis) infinito

$even(0)\$

$even(s(0))\leftarrow {\hbox{not }}even(0)$

$even(s(s(0)))\leftarrow {\hbox{not }}even(s(0))$

$\dots$

Definição

Seja $P$ um conjunto de regras da forma

$A\leftarrow B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$

onde $A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}$ são átomos livres de variáveis. Se $P$ não contém negação ($n=0$ em todas as regras do programa), então, por definição, o único modelo estável de $P$ é o seu modelo que é minimamente relativo à inclusão em conjunto. (Qualquer programa sem negação tem exatamente um modelo mínimo). Para estender essa definição ao caso de programas com negação precisamos do conceito auxiliar de 'redutiva' definido a seguir.

Para qualquer conjunto $I$ de átomos básicos, o reduto de $P$ em relação a $I$ é o conjunto de regras sem negação obtidas de $P$ primeiramente descartando toda regra na qual pelo menos um dos átomos $C_{i}$ no formato

$B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$

pertence a $I$, então descartando as partes ${\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$ dos corpos de todas as regras restantes.

Dizemos que $I$ é um modelo estável de $P$ se $I$ é o modelo estável do reduto de $P$ relativo a $I$ (Como o reduto não contém negação seu modelo estável já foi definido.) Como o termo modelo estável sugere, todo modelo estável de $P$ é modelo de $P$.

Exemplo

Para ilustrar essas definições, vamos checar se $\{p,s\}$ é um modelo estável do programa

$p\$

$r\leftarrow p,\ q$

$s\leftarrow p,\ {\hbox{not }}q.$

A redutiva desse programa relativa à $\{p,s\}$ é

$p\$

$r\leftarrow p,\ q$

$s\leftarrow p.$

(De fato, como $q\not \in \{p,s\}$ o reduto é obtido do programa descartando a parte ${\hbox{not }}q.\$). O modelo estável do reduto é $\{p,s\}$. (De fato, esse conjunto de átomos satisfaz toda a regra da redutiva e não tem nenhum subconjunto próprio com a mesma propriedade.) Então depois de computar o modelo estável do reduto chegamos no mesmo modelo $\{p,s\}$ com o qual começamos. Consequentemente, esse conjunto é um modelo estável.

Checando da mesma maneira os outros 15 conjuntos consistindo dos átomos $p,\ q,\ r,\ s$ mostramos que esse programa não tem nenhum outro modelo estável. Por exemplo, o reduto do programa relativo a $\{p,q,r\}$ é

$p\$

$r\leftarrow p,\ q.$

Logo, o modelo estável da redutiva é $\{p\}$, que é diferente do conjunto $\{p,q,r\}$ com o qual começamos.

Programas sem um modelo estável específico

Um programa com negação pode ter vários modelos estáveis ou nenhum modelo estável. Por exemplo, o programa

$p\leftarrow {\hbox{not }}q$

$q\leftarrow {\hbox{not }}p$

tem dois modelos estáveis $\{p\}$, $\{q\}$. O programa de uma só afirmação

$p\leftarrow {\hbox{not }}p$

não tem modelos estáveis.

Se pensarmos nas semânticas de modelo estável como uma descrição do comportamento de Prolog na presença de negação, então programas sem um modelo estável único podem ser julgados como insatisfatíveis. Eles não fornecem uma especificação não ambígua para a consulta eletrônica estilo Prolog. Por exemplo, os dois programas acima não são razoáveis como programas do Prolog - a resolução de SLDNF não termina neles.

Mas o uso de modelos estáveis na programação de conjuntos-resposta fornece uma perspectiva diferente sobre tais programas. Neste paradigma de programação, um determinado problema de pesquisa é representado por um programa lógico, de modo que os modelos estáveis do programa correspondem a soluções. Em seguida, os programas com muitos modelos estáveis correspondem a problemas com muitas soluções e programas sem modelos estáveis correspondem a problemas insolúveis. Por exemplo, o conhecido enigma das oito rainhas tem 92 soluções, número muito grande para ser resolvido usando o modelo de programação-resposta e codificá-lo por um programa em lógica com 92 modelos estáveis. Podemos considerar, então, programas lógicos com exatamente um modelo estável, como tão especiais com polinômios com somente uma raiz em álgebra, entre o conjunto de programas lógicos.

Propriedades da semântica de modelo estáveis

Nesta seção, como na definição de modelo estável, por um programa lógico queremos dizer um conjunto de regras na forma

$A\leftarrow B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$

na qual são átomos sem variáveis.

Átomos" de Cabeçalho": Se uma atômica $A$ pertence a um modelo estável de um programa lógico $P$ então $A$ inicia uma das regras de $P$.

Minimalidade: Qualquer modelo estável de um programa lógico é mínimo entre os modelos de relativa à inclusão do conjunto.

Propriedade Anticadeia: Se $I$ e $J$ são modelos estáveis do mesmo programa lógico então $I$ não é um subconjunto próprio de $J$. Em outras palavras, o conjunto de modelos estáveis é uma anticorrente.

NP-Completude: Testar se um programa lógico finito e sem variáveis tem um modelo estável é um problema NP-Completo.

Relação com outras teorias de negação por falha

Completação do Programa

Qualquer modelo estável de um programa sem variáveis não é apenas um modelo do programa em si, mas também um modelo de sua conclusão. [Marek and Subrahmanian, 1989]. O inverso, porém, não é verdade. Por exemplo, a conclusão do programa de uma só regra

$p\leftarrow p$

é a tautologia $p\leftrightarrow p$. O modelo $\emptyset$ dessa tautologia é um modelo estável de $p\leftarrow p$, mas o seu outro modelo $\{p\}\$ não é. François Fages [1994] achou uma condição sintática em programas lógicos que elimina esses contraexemplos e garante a estabilidade de todo modelo da conclusão do programa. Um programa que satisfaz aquela condição é chamado de seguro (tight).

Fangzhen Lin e Yuting Zhao [2004] mostram como tornar a conclusão de um programa não-seguro mais forte para que todos seus modelos não estáveis sejam eliminados. As fórmulas adicionais que eles adicionam a essa conclusão são chamadas de Fórmulas de Loop.

Semântica Bem-Fundada

O modelo bem-fundado de um programa lógico particiona todos os átomos sem variáveis em três conjuntos: verdadeiro, falso, e desconhecido. Se um átomo é verdadeiro no modelo bem fundado de $P$, então ele pertence a todos os modelos estáveis de $P$. O contrário, geralmente, não é válido. Por exemplo, o programa:

$p\leftarrow {\hbox{not }}q$

$q\leftarrow {\hbox{not }}p$

$r\leftarrow p$

$r\leftarrow q$

tem dois modelos estáveis, $\{p,r\}$ e $\{q,r\}$. Por mais que $r$ pertença a ambos, seu valor no modelo bem fundado é desconhecido.

Além disso, se um átomo é falso no modelo bem fundado então não pertence à nenhum modelo estável. Então o modelo bem fundado de um programa lógico fornece um limitante inferior sobre a interseção de seus modelos estáveis e um limitante superior sobre sua união.

Negação forte

Representando uma informação incompleta

Da perspectiva da representação do conhecimento, um conjunto de átomos pode ser imaginado como uma descrição de um estado completo de conhecimento: os que pertencem a um conjunto são conhecidos como verdadeiros, e aqueles que não pertencem ao conjunto são conhecidos como falsos. A possibilidade do estado incompleto do conhecimento pode ser descrito usando um consistente mas possivelmente incompleto conjunto de literais. Se uma atômica $p$ não pertence ao conjunto e a sua negação não pertence ao conjunto também, então não é sabido se $p$ é verdadeiro. No contexto da logica de programação, a ideia se baseia na necessidade de distinguir entre dois tipos de negação, negação por falha, discutida acima, e negação forte, que é denotada como $\sim$.. O exemplo a seguir, ilustrando a diferença entre os dois tipos de negação, pertence a John McCarthy. Um ônibus de uma escola pode atravessar os trilhos de um trem sobre a condição de não ter nenhum trem cruzando-os. Se nós não necessariamente soubermos se o trem esta se aproximando, então usamos a negação por falha.

${\hbox{Cross}}\leftarrow {\hbox{not Train}}$

Não é uma representação adequada a esta ideia: Ela diz que está certo passar nos trilhos na ausência de informação sobre a aproximação do trem. A regra mais fraca, que usa negação forte em seu modelo, é preferível.

${\hbox{Cross}}\leftarrow \,\sim {\hbox{Train}}.$

Ela diz que está certo passar nos trilhos se nós sabemos que não há trens se aproximando.

Modelos Estaveis Coerentes

Para incorporar a Negação forte na teoria de modelos estáveis, Gelfond and Lifschitz [1991] permitiram ambas as expressões $A$, $B_{i}$, $C_{i}$ em uma regra

$A\leftarrow B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$

serem um átomo ou um átomo prefixado com o símbolo de negação forte. Ao invés de modelos estáveis, sua generalização usa conjuntos de respostas, que podem incluir átomos ou átomos prefixados com negação forte. Uma alternativa semelhante [Ferraris and Lifschitz, 2005] trata a negação forte como uma parte do átomo, e não requer nenhuma mudança em sua definição de modelo estavel. Em sua teoria de negação forte, nós distinguimos os átomos em dois tipos, positivo e negativo, e assumimos que cada átomo negativo é uma expressão de forma $\sim A$, onde $A\$ é um átomo positivo. Um conjunto de átomos é chamado de coerente se não contem pares “complementares” de átomos $\ A,\sim A$. Modelos Estaveis coerentes de um programa são identicos a seu conjunto de respostas consistentes na visão de [Gelfond and Lifschitz, 1991] Por exemplo, o programa

$p\leftarrow {\hbox{not }}q$

$q\leftarrow {\hbox{not }}p$

$r\$

$\sim r\leftarrow {\hbox{not }}p$

tem dois modelos estáveis $\{p,r\}\$ e $\ \{q,r,\sim r\}$. O primeiro modelo é coerente, o segundo não, pois contém a atômica $\ r$ e a atômica $\ \sim r$.

Suposição do Mundo Fechado

De acordo com [Gelfond and Lifschitz, 1991], o pressuposto do mundo fechado para um predicado P pode ser expresso pela sentença

$\sim p(X_{1},\dots ,X_{n})\leftarrow {\hbox{not }}p(X_{1},\dots ,X_{n})$

(a relação $p\$ não é válida para a tupla $X_{1},\dots ,X_{n}$ se não existe evidencia de que ela será valida). Por exemplo, modelo estável do programa

$p(a,b)\$

$p(c,d)\$

$\sim p(X,Y)\leftarrow {\hbox{not }}p(X,Y)$

Consiste de 2 atômicas positivas

$p(a,b),\ p(c,d)\$

E 14 atômicas negativas

$\sim p(a,a),\ \sim p(a,c),\ \dots$

i.e. , as negações fortes de todas as outras atômicas positivas formadas por $p,\ a,\ b,\ c,\ d$. Um programa lógico com negação forte pode incluir as sentenças da suposição do mundo fechado para alguns de seus predicados e deixar outros predicados no domínio da suposição do mundo aberto.

Programas com restrições

A semântica do modelo estável tem sido generalizada a partir de vários programas lógicos diferentes das coleções de sentenças “tradicionais” discutidas acima. Sentenças da forma

$A\leftarrow B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$

Onde $A,B_{1},\dots ,B_{m},C_{1},\dots ,C_{n}$ são atômicas. Uma simples extensão permite programas conter restrições - regras com premissa vazia:

$\leftarrow B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}.$

Vale relembrar que sentenças tradicionais podem ser vistas como uma notação alternativa para a formula proposicional se nós identificarmos a virgula como conjunção $\land ,$, e o simbolo ${\hbox{not}}$ como negação $\neg ,$ e concordar de tratar $F\leftarrow G$ como uma implicação $G\rightarrow F$ escrita de trás para frente. Para estender essa convenção para restrição, nós identificamos a restrição com negação da formula correspondente a :

$\neg (B_{1}\land \cdots \land B_{m}\land \neg C_{1}\land \cdots \land \neg C_{n}).$

Nós podemos agora estender a definição de modelo estável para programas com restrições. Como no caso de programas tradicionais, nos podemos começar com programas que não contém negações. Esse programa pode ser inconsistente; então falamos que não existem modelos estáveis. Se tal programa $P$ é consistente então $P$ tem um modelo mínimo, e esse modelo é considerado o único modelo de $P$. Modelos estáveis de um programa arbitrário com restrições são definidos usando reduções, formadas do mesmo jeito que no caso de programas tradicionais (veja a definição de Modelo Estável acima). Um conjunto $I$ de atômicas é um modelo estável de um programa $P$ com restrições se uma redução $P$ relativa a $I$ tem um modelo estável, e seu modelo estável é igual a $I$. As propriedades da semântica do modelo estável descritas acima para programas tradicionais também são válidas na presença de restrições. As restrições têm um papel importante na resposta de um conjunto de programas porque adicionar restrições à lógica de uma programa $P$ afeta sua coleção de modelos estáveis de uma maneira simples: elimina os modelos estáveis que violam as restrições. Em outras palavras, para qualquer programa P com restrições e qualquer restrição C, o modelo estável P U {C} pode ser caracterizado como um modelo estável de P que satisfaz C.

Programas Disjuntivos

Em uma sentença disjuntiva, a premissa pode ser uma disjunção de varias atômicas:

$A_{1};\dots ;A_{k}\leftarrow B_{1},\dots ,B_{m},{\hbox{not }}C_{1},\dots ,{\hbox{not }}C_{n}$

(o ponto e virgula é visto como uma alternativa para notação de disjunção $\lor$). As sentenças tradicionais correspondem para $k=1$, e as restrições para $k=0$. Para estender a semântica de modelo estável para programas disjuntos [Gelfond and Lifschitz, 1991], nós primeiramente definimos que na ausência de negação($n=0$ em cada sentença) os modelos estáveis do programa são seus modelos minimais. A definição de redução para programas disjuntivos se mantém a mesma que antes. Um conjunto $I$ de atômicas é um modelo estável de $P$ se $I$ é um modelo estavel da redução $P$ relativa a $I$. Por exemplo, o conjunto $\{p,r\}$ é modelo estável de um programa disjuntivo

$p;q\$

$r\leftarrow {\hbox{not}}\ q$

Porque é um dos dois modelos minimais da redução

$p;q\$

$r.\$

O programa acima tem mais um modelo estável, $\{q\}$. Como no caso dos programas tradicionais, cada elemento de qualquer modelo estável do programa disjuntivo $P$ é uma atômica de $P$, no sentido de que ocorre na premissa de uma das sentenças de $P$. Como no caso tradicional, o modelo estável de um programa disjuntivo são minimais e formam anticadeias. Testando se um programa disjuntivo finito tem um modelo estável é $\Sigma _{2}^{\rm {P}}$-complete [Eiter and Gottlob, 1993].

Modelo estável de um conjunto de formulas proposicionais

Premissas, e até premissas disjuntivas possuem uma forma sintática especial em comparação com fórmulas proposicionais comuns. Cada premissa disjuntiva é essencialmente uma implicação que o seu antecedente e a conjunção de literais, e seu consequente é uma disjunção de atômicas. David Pearce [1997] e Paolo Ferraris [2005] mostraram como estender a definição de modelo estável a um conjunto de fórmulas proposicionais comum. Essa generalização tem aplicações na programação de conjunto de resposta. A formulação de Pearce parece diferir da definição original de modelo estável. Ao invés de reduções, ela se refere a “equilíbrio lógico”- um sistema da lógica não-monotônica baseado nos modelos de Kripke. A formulação de Ferrari, por outro lado, é baseada em reduções, apesar do processo de construção da redução seja diferente do processo descrito acima.

Definição geral de modelos estáveis

De acordo com [Ferraris, 2005], a redução da fórmula proposicional $F$ relativa a um conjunto $I$ de atômicas é uma formula obtida de $F$ substituindo cada subfórmula maximal que não satisfaz $I$ com a constante logica $\bot$ (falso). A redução do conjunto $P$ das formulas proposicionais relativas a $i$ consiste das reduções de todas as formulas vindas de $P$ relativas a $i$. No caso de um programa disjuntivo, podemos dizer que o conjunto $I$ de atômicas é um modelo estável de $P$ se $I$ é minimal (respeitando a inclusão do conjunto) entre os modelos de redução de $P$ relativo a $i$. Por exemplo, a redução do conjunto

$\{p,\ p\land q\rightarrow r,\ p\land \neg q\rightarrow s\}$

Relativo a $\{p,s\}$ é

$\{p,\ \bot \rightarrow \bot ,\ p\land \neg \bot \rightarrow s\}.$

Como $\{p,s\}$ é um modelo da redução, então os subconjuntos próprios daquele conjunto não são modelos da redução, $\{p,s\}$ é um modelo estável dado o conjunto de fórmulas. Nós vimos que $\{p,s\}$ também é um modelo estável de mesma fórmula, escrita na notação da programação lógica, em relação à sua definição original. É um caso do fato em geral: aplicada a um conjunto de (fórmulas correspondendo a) sentenças tradicionais, a definição de modelos estáveis de acordo com Ferrari é equivalente à definição original. O mesmo é verdadeiro, mais geral, para programas com restrições e para programas disjuntivos.

Propriedades da semântica de modelos estáveis generalizada

O teorema afirma que todos os elementos de qualquer modelo estável de um programa $P$ com premissa atômica de $P$ pode ser estendida para conjuntos de fórmulas proposicionais, se nós definirmos premissas atômicas como no exemplo a seguir. Uma atômica $A$ é uma premissa atômica de um conjunto $P$ de fórmulas proposicionais se pelo menos uma ocorrência de $A$ na fórmula de $P$ está tanto no escopo da negação quanto no antecedente da implicação. ( Nós assumimos aqui que a equivalência tratada como abreviação, não como um conectivo primitivo.) O minimalidade e a propriedade anticadeia dos modelos estáveis de um programa tradicional não é válido para o caso geral. Por exemplo, (o conjunto único consistente da) a fórmula

$p\lor \neg p$

Tem dois modelos estáveis, $\emptyset$ e $\{p\}$. O consequente não é mínimo, e é um superconjunto próprio do anterior. Testando se um conjunto finito de fórmulas proposicionais tem modelo estável $\Sigma _{2}^{\rm {P}}$-complete, no caso de programas disjuntivos.

Referências

• N. Bidoit and C. Froidevaux [1987] Minimalism subsumes default logic and circumscription. In: Proceedings of LICS-87, pages 89–97.

• T. Eiter and G. Gottlob [1993] Complexity results for disjunctive logic programming and application to nonmonotonic logics. In: Proceedings of ILPS-93, pages 266-278.

• M. van Emden and R. Kowalski [1976] The semantics of predicate logic as a programming language. Journal of ACM, Vol. 23, pages 733-742.

• F. Fages [1994] Consistency of Clark's completion and existence of stable models. Journal of Methods of Logic in Computer Science, Vol. 1, pages 51–60.

• P. Ferraris [2005] Answer sets for propositional theories. In: Proceedings of LPNMR-05, pages 119-131.

• P. Ferraris and V. Lifschitz [2005] Mathematical foundations of answer set programming. In: We Will Show Them! Essays in Honour of Dov Gabbay, King's College Publications, pages 615-664.

• M. Gelfond [1987] On stratified autoepistemic theories^{[ligação inativa]}. In: Proceedings of AAAI-87, pages 207-211.

• M. Gelfond and V. Lifschitz [1988] The stable model semantics for logic programming. In: Proceedings of the Fifth International Conference on Logic Programming (ICLP), pages 1070-1080.

• M. Gelfond and V. Lifschitz [1991] Classical negation in logic programs and disjunctive databases. New Generation Computing, Vol. 9, pages 365-385.

• S. Hanks and D. McDermott [1987] Nonmonotonic logic and temporal projection. Artificial Intelligence, Vol. 33, pages 379-412.

• F. Lin and Y. Zhao [2004] ASSAT: Computing answer sets of a logic program by SAT solvers. Artificial Intelligence, Vol. 157, pages 115-137.

• V. Marek and V.S. Subrahmanian [1989] The relationship between logic program semantics and non-monotonic reasoning. In: Proceedings of ICLP-89, pages 600-617.

• D. Pearce [1997] A new logical characterization of stable models and answer sets. In: Non-Monotonic Extensions of Logic Programming (Lecture Notes in Artificial Intelligence 1216), pages 57–70.

• R. Reiter [1980] A logic for default reasoning. Artificial Intelligence, Vol. 13, pages 81–132.