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
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 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 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 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 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 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.Esta abordagem para a semântica de programas lógicoss sem a negação é creditada a Marteen van Emden e Robert Kowalski . (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
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
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
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
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
é a tautologia . O modelo dessa tautologia é um modelo estável de , mas o seu outro modelo não é. François Fages 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 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 , 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 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 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 .Gelfond and Lifschitz chama a segunda negação de “clássica” e a denota por .. 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.