Elsa Carvalho 163 Universidade da Madeira Departamento de Matemática Programação em Lógica e Funcional (2000/01) (Actualizado em 2004/05) Teoria dos Modelos

Elsa Carvalho

Programação em Lógica e Funcional (2000/01)(Actualizado em 2004/05)

1Universidade da Madeira

Departamento de Matemática

Teoria dos Modelos e das ProvasLógica fornece duas noções de consequência: lógica e sintática.

Teoria dos ModelosSeja S um conjunto de frases lógicas e f uma frase lógica: f é consequência lógica de S se e só se todos os modelos de S são modelos de f. Escreve-se da seguinte forma:

S╞ f

A Teoria dos Modelos proporciona uma forma de atribuir significado (semântica) às frases lógicas.

Elsa Carvalho




Teoria dos Modelos e das Provas

Teoria das ProvasSeja S um conjunto de frases lógicas, f uma frase lógica e R um conjunto de regras de inferência: f é consequência sintáctica (ou é derivável a partir) de S se e só se é possível inferir f a partir de S aplicando as regras de inferência R. Escreve-se da seguinte forma:

S├ f

A Teoria das Provas proporciona uma forma de gerar frases a partir da manipulação sintáctica de outras frases.

Elsa Carvalho




Teoria dos Modelos - ConceitosUma interpretação atribui significado a uma frase lógica, associando-a a alguma declaração que tenha valores lógicos (verdade ou falso), num domínio específico escolhido.

Uma interpretação que faz uma frase lógica ser verdade designa-se um modelo da frase (ou que satisfaz a frase).

Podemos estender esta definição para um conjunto de frases:Uma interpretação é um modelo para o conjunto se e só se é um modelo para cada um dos membros do conjunto.

Uma interpretação que não satisfaz uma frase diz-se um contra-modelo (ou que não satisfaz).

Uma frase válida é uma frase lógica em que todas as suas interpretações são modelos.

Elsa Carvalho




Teoria dos Modelos - ConceitosExemplo

Considere-se a seguinte fórmula chã

gosta(barney, bambam)

e escolha-se um domínio constituído por apenas 2 elementos.

De forma a realizarmos uma interpretação teremos de associar os elementos do domínio com as constantes da fórmula: barney e bambam e também associar alguma relação binária no domínio com o predicado binário - gosta - da fórmula.

Elsa Carvalho




Exemplo (cont.)

A frase gosta(barney, bambam) é verdade na interpretação:

= barney = bambam

egosta =

< > < > < >

porque o tuplo < > pertence ao domínio da relação gosta.

Teoria dos Modelos

Elsa Carvalho




Teoria dos Modelos

a interpretação anterior é um modelo de gosta(barney, bambam)

frase que não tem modelos(X)(Y) (gosta(X,Y) gosta(X,Y))

frase válida(X)(Y) (gosta(X,Y) gosta(X,Y))

Duas frases são logicamente equivalentes (S1 S2) se e só se tiverem os mesmos modelos.

Elsa Carvalho




Teoria das Provas - ConceitosA Teoria das Provas preocupa-se com a derivabilidade de frases lógicas a partir de outras frases, usando regras de inferência.

As frases iniciais são chamadas de axiomas.

As frases derivadas são chamadas teoremas (ou consequências sintácticas).

Regras de inferência operam unicamente sobre a sintaxe das frases (e não sobre o seu significado).

Elsa Carvalho




Teoria das Provas - ConceitosA regra de inferência mais popular (usada pela lógica clássica) é o Modus Ponens:

“do par de frases {W2, W1W2} inferir a frase W1”

Os axiomas mais as regras de inferência constituem um sistema de inferência.

Os axiomas juntamente com os teoremas derivados constituem uma Teoria.

Uma teoria é inconsistente se e só se contém conjuntamente uma frase e a sua negação. Caso contrário é consistente.

Elsa Carvalho




Teoria das Provas - ConceitosDefinição formal de ProvaSeja A um conjunto de axiomas e R um conjunto de regras de inferência. Uma prova derivada do sistema de inferência [A, R] é a sequência

< s1, s2, ..., sn >

em que cada si ou é um axioma de A ou é derivado através da aplicação de uma regra de R em axiomas de A e/ou de frases que precedem si.

A sequência é denominada por prova de si i.e. A ├ si

A relação de derivabilidade usando R é definida por:

├R = {(A, s) s é provado através de A usando R}

Elsa Carvalho




Relação entre Teoria dos Modelos e das Provas

Seja S um conjunto de frases lógicas e c uma conclusão. Requisito mínimo:

Se S expressa correctamente o nosso problema a resolver então c expressa correctamente a conclusão.

Se correcto quer dizer “verdade numa interpretação própria” então podemos dizer que, para uma dada interpretação I:

Se I é um modelo de S então I é um modelo de c

Elsa Carvalho




Mas o computador só manipula símbolos e nada sabe sobre as nossas intenções.

Terá de ser algo mais forte, ou seja, para todas as possíveis interpretações I:

Se I é um modelo de S então I é um modelo de c

Por outras palavras, queremos mostrar que S╞ c.

Felizmente, é possível mostrar que S╞ c sem ter que verificar todas as interpretações.

Usamos simplesmente um sistema de inferência que estabeleça a relação S├ c.


Elsa Carvalho




Duas propriedades essenciais dos sistemas de inferência

Correcto (Soundness)

para todo o S e c, se S├ c então S╞ c

Um procedimento de prova que não prove fórmulas falsas diz-se que é correcto.

Completo (Completeness)

para todo o S e c, se S╞ c então S├ c

Um procedimento de prova com o qual é possível provar qualquer fórmula verdadeira diz-se que é completo.

Um sistema que não é completo não tem poder inferencial suficiente para resolver todos os problemas que têm solução.


Elsa Carvalho




Sistemas de Inferência para a Forma Clausal

As letras que vamos utilizar de seguida, A, B, C, etc., referem-se a proposições.

Um exemplo de um sistema correcto e completo é:

modus ponens {B, A B} ├ A com

transporte de literais (A B C A B C)

Um problema com o uso do modus ponens é que é usado sem particular objectivo de uma conclusão específica. Assim pode inferir coisas nas quais não estamos interessados.

Elsa Carvalho





Considerando isto, é geralmente melhor usar um sistema de inferência com a seguinte regras:

{(C A C1 … Cn), (A B)}├ C B C1 … Cn

Um caso especial desta regra é modus tollens:

{A, (A B)}├ B

{ A, (A B)}├ B (formato condicional)

Com este novo método, primeiro nega-se a conclusão desejada e depois tenta-se inferir a cláusula vazia ( ) (inconsistência).

Elsa Carvalho





Generalizando, tendo um programa P (conjunto de cláusulas), uma desejada conclusão A e um sistema de inferência que é correcto e completo para ├, então:

P {A}╞ se e só se P╞ (falso A)

P {A}╞ se e só se P╞ A

P {A}├ se e só se P├ A

Na primeira equivalência utiliza-se uma teorema da consequência lógica que diz

para qq conjunto de frases S = {s1, ..., sn} e qq frase f,

S╞ f se e só se S – {si}╞ (f si) [para qq i]

Elsa Carvalho




Assim, se a conclusão A pode ser inferida directamente de P, então a sua negação A pode ser refutada de P.

Qualquer prova de é designada por refutação.

A execução de um programa em lógica é baseado no método de provas por refutação. Dado um programa P e uma fórmula negada A (ambas na forma clausal) tentamos mostrar que

P {A} é inconsistente


Elsa Carvalho




Resolução (versão proposicional)

Resolução é uma regra de inferência que, usada isoladamente, é suficiente para testar se um dado conjunto de cláusulas é inconsistente (derivando ).

Assim temos, dado um conjunto de cláusulas P:

1. Escolher uma cláusula A A1 … Am P

2. Procurar outra cláusula C A C1 … Cn P

3. Construir a cláusula C A1 … Am C1 … Cn

4. Adicionar a cláusula construída a P

Elsa Carvalho





Dado

pai mae progenitor e homem pai

construir

homem mae progenitor

A aplicação da regra chama-se um passo da resolução.

As cláusulas escolhidas para um passo de resolução são chamadas premissas.

A cláusula que é derivada chama-se resolvente.

Elsa Carvalho





Propriedades

É correcto: cada resolvente é implicado pelas suas premissas.

Um resolvente é a cláusula vazia ( ) se e só se uma premissa é uma fórmula atómica A e a outra é A.

Para qualquer conjunto inconsistente de cláusulas de Horn, a cláusula vazia pode ser inferida como resolvente. Por causa desta propriedade chamamos à resolução refutation-complete (completa com a refutação).

A resolução pode ser usada unicamente com frases lógicas na forma clausal.

Elsa Carvalho





A forma habitual de usar a resolução para a programação com cláusulas de Horn é:

assumimos que P é um conjunto de cláusulas definidas

a resposta desejada A é formulada como uma cláusula negativa A

aplica-se a resolução com o objectivo de obter uma prova de ou seja, refutação.

Elsa Carvalho





Assim temos

P╞ A se e só se P {A} é inconsistente

então P╞ A se e só se P {A}├ por refutação

uma vez que a resolução é correcta e completa com a refutação.

Elsa Carvalho





Exemplo com cláusulas de Horn

1. A2. A B C3. B C4. C Por resolução temos

de 1. e 2. infere-se 5. B Cde 3. e 5. infere-se 6. C Cde 4. e 6. infere-se 7. Cde 4. e 7. infere-se 8.

Note-se que existem outras refutações alternativas e podem ser obtidas por resolução.

Elsa Carvalho





A representação em árvore é mais habitual

A A B C B C C

B C

C C

C

Documents

Elsa Carvalho 163 Universidade da Madeira Departamento de Matemática Programação em Lógica e Funcional (2000/01) (Actualizado em 2004/05) Teoria dos Modelos