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

editar

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

 
 
 


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

 
T

 
F

 
F

 
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   e o símbolo   como uma negação   e concordarmos em tratar   como a implicação   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

 

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


 
T

 
T

 
T

 
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

editar

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   no corpo de um regra como “não se acredita em  ”, 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

 

pode ser entendida como o padrão que nos permite derivar   de   assumindo que   é 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

editar

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

 
T

 
F

 
F

 
T

é associada com o conjunto  . 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   é 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

 
 

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

 

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

 
 
 
 

Definição

editar

Seja   um conjunto de regras da forma

 

onde   são átomos livres de variáveis. Se   não contém negação (  em todas as regras do programa), então, por definição, o único modelo estável de   é o seu modelo que é minimamente relativo à inclusão em conjunto.[1] (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   de átomos básicos, o reduto de   em relação a   é o conjunto de regras sem negação obtidas de   primeiramente descartando toda regra na qual pelo menos um dos átomos   no formato

 

pertence a  , então descartando as partes   dos corpos de todas as regras restantes.

Dizemos que   é um modelo estável de   se   é o modelo estável do reduto de   relativo a   (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   é modelo de  .

Exemplo

editar

Para ilustrar essas definições, vamos checar se   é um modelo estável do programa

 
 
 

A redutiva desse programa relativa à   é

 
 
 

(De fato, como   o reduto é obtido do programa descartando a parte  ). O modelo estável do reduto é  . (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   com o qual começamos. Consequentemente, esse conjunto é um modelo estável.

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

 
 

Logo, o modelo estável da redutiva é  , que é diferente do conjunto   com o qual começamos.

Programas sem um modelo estável específico

editar

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

 
 

tem dois modelos estáveis  ,  . O programa de uma só afirmação

 

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

editar

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

 

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

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

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

Propriedade Anticadeia: Se   e   são modelos estáveis do mesmo programa lógico então   não é um subconjunto próprio de  . 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

editar

Completação do Programa

editar

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

 

é a tautologia  . O modelo   dessa tautologia é um modelo estável de  , mas o seu outro modelo   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

editar

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  , então ele pertence a todos os modelos estáveis de  . O contrário, geralmente, não é válido. Por exemplo, o programa:

 
 
 
 

tem dois modelos estáveis,   e  . Por mais que   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

editar

Representando uma informação incompleta

editar

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   não pertence ao conjunto e a sua negação não pertence ao conjunto também, então não é sabido se   é 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  .[2]. 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.

 

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.

 

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

Modelos Estaveis Coerentes

editar

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

 

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  , onde   é um átomo positivo. Um conjunto de átomos é chamado de coerente se não contem pares “complementares” de átomos  . 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

 
 
 
 

tem dois modelos estáveis   e  . O primeiro modelo é coerente, o segundo não, pois contém a atômica   e a atômica  .

Suposição do Mundo Fechado

editar

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

 

(a relação   não é válida para a tupla   se não existe evidencia de que ela será valida). Por exemplo, modelo estável do programa

 
 
 

Consiste de 2 atômicas positivas

 

E 14 atômicas negativas

 

i.e. , as negações fortes de todas as outras atômicas positivas formadas por  . 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

editar

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

 

Onde   são atômicas. Uma simples extensão permite programas conter restrições - regras com premissa vazia:

 

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  , e o simbolo   como negação   e concordar de tratar   como uma implicação   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 :

 

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   é consistente então   tem um modelo mínimo, e esse modelo é considerado o único modelo de  . 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   de atômicas é um modelo estável de um programa   com restrições se uma redução   relativa a   tem um modelo estável, e seu modelo estável é igual a  . 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   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

editar

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

 

(o ponto e virgula é visto como uma alternativa para notação de disjunção  ). As sentenças tradicionais correspondem para  , e as restrições para  . 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(  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   de atômicas é um modelo estável de   se   é um modelo estavel da redução   relativa a  . Por exemplo, o conjunto   é modelo estável de um programa disjuntivo

 
 

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

 
 

O programa acima tem mais um modelo estável,  . Como no caso dos programas tradicionais, cada elemento de qualquer modelo estável do programa disjuntivo   é uma atômica de  , no sentido de que ocorre na premissa de uma das sentenças de  . 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 é  -complete [Eiter and Gottlob, 1993].

Modelo estável de um conjunto de formulas proposicionais

editar

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

editar

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

 

Relativo a   é

 

Como   é um modelo da redução, então os subconjuntos próprios daquele conjunto não são modelos da redução,   é um modelo estável dado o conjunto de fórmulas. Nós vimos que   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

editar

O teorema afirma que todos os elementos de qualquer modelo estável de um programa   com premissa atômica de   pode ser estendida para conjuntos de fórmulas proposicionais, se nós definirmos premissas atômicas como no exemplo a seguir. Uma atômica   é uma premissa atômica de um conjunto   de fórmulas proposicionais se pelo menos uma ocorrência de   na fórmula de   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

 

Tem dois modelos estáveis,   e  . 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  -complete, no caso de programas disjuntivos.

  1. Esta abordagem para a semântica de programas lógicoss sem a negação é creditada a Marteen van Emden e Robert Kowalski [1976].
  2. Gelfond and Lifschitz [1991] chama a segunda negação de “clássica” e a denota por  .

Referências

editar
  • N. Bidoit and C. Froidevaux [1987] Minimalism subsumes default logic and circumscription. In: Proceedings of LICS-87, pages 89–97.
  • 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.
  • S. Hanks and D. McDermott [1987] Nonmonotonic logic and temporal projection. Artificial Intelligence, Vol. 33, pages 379-412.
  • 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.