Upload
internet
View
109
Download
2
Embed Size (px)
Citation preview
1
Resolução
2
Resolução 5.1 O Princípio da Resolução (Lógica
Proposicional)Para quaisquer duas cláusulas C1 e C2, se existe um literal L1 em C1 que seja complementar a um literal L2 em C2, então retire L1 e L2 de C1 e de C2 respectivamente, e construa a disjunção das cláusulas remanescentes. A cláusula assim construida é dita ser um resolvente de C1 e C2.
3
Resolução Considere a seguintes cláusulas C1 e
C2 abaixo: C1: P R C2: ~P Q
R Q é um resolvente de C1 e C2.
4
Resolução Teorema 1: Dado duas cláusulas C1 e C2, um
resolvente C de C1 e C2 é consequência lógica de C1 e C2.
Def.1 Dado um conjunto S de cláusulas, uma resolução (dedução) de uma cláusula C a partir de S é uma sequência finita C1, ... ,Ck de cláusulas tal que cada Ci é uma cláusula em S ou um resolvente de cláusulas precedendo Ci, e Ck = C. Uma dedução de a partir de S é chamada uma refutação de S.
5
Resolução Exemplo: Prove que o conjunto de cláusulas
S é insatisfatível: S = {~P Q, ~Q, ~P}
1. ~P Q2. ~Q3. P4. Q de 1 e 3, R5. de 4 e 2, R
6
Unificação Aplicar o Princípio da Resolução implica
em procurar literais complementares.
Para cláusulas sem variáveis é muito simples.
Para cláusulas com variáveis, é necessário fazer substituições para unificar os literais Exemplo:
C1: P(x) Q(x) C2: ~P(f(y)) R(y)
7
Unificação: Exemplo:C1 (P(x) Q(x)) e C2 (~P(f(y))
R(y)) Aplicando-se as substituições s1 e s2 à C1 e C2,
C1: P(x) Q(x) s1 = {x/f(a) } C2: ~P(f(y)) R(y) s2 = {y/a }
Obtém-se C’1 e C’2, C’1: P(f(a)) Q(f(a)) C’2: ~P(f(a)) R(a)
Aplicando-se o princípio da Resolução à C’1 e C’2 obtém-se o resolvente C: C: Q(f(a)) R(a)
8
Unificação Outras substituições também poderiam ser aplicadas
Exercício: Para s1 = {x/f(f(a))} e s2 = {y/f(a)}, Qual seria o resolvente obtido?
Teria outras possíveis substituições?
Uma substituição mais geral seria substituir x por f(y) em C1 e obter-se:
C1*: P(f(y)) Q(f(y))
e um resolvente mais geral C:
C: Q(f(y)) R(y)
9
Unificação
A cláusula C é a cláusula mais geral no sentido de que todas as outras cláusulas que podem ser obtida pelo processo anterior são instâncias de C. Por exemplo, C’ é uma instância de C.
C: Q(f(y)) R(y) C’: Q(f(a)) R(a)
10
Unificação Def.2 Sejam as substituições
= {x1/t1, ... ,xn/tn } e
= { y1/u1, ... , ym/um}
a composição de com () é a substituição obtida do conjunto
{ x1/t1, ... , xn/tn, y1/u1, ... , ym/um}
pela retirada dos elementos:xj/tj para o qual tj = xj e
yi/ui tal que yi {x1, ... ,xn}.
11
Unificação Exemplo: Sejam as substituições
= {t1/x1, t2/x2} = { x/f(y), y /z }
= { y1/u1, y2/u2, y3/u3 } = { x/a, y/b, z/y }
() = { x1/t1, x2/t2, y1/u1, y2/u2, y3/u3 }
= { x/f(b), y/y, x/a, y/b, z/y }
= { x/f(b), z/y }
12
Unificação Def.3 Uma substituição é chamada um
unificador para um conjunto de expressões
{E1, ... ,En} se e somente se E1 = E2 = ... =
En.
O conjunto {E1, ... ,En} é dito ser unificável se existe um unificador para ele.
13
Unificação
Def.4 Um unificador para um conjunto de expressões {E1, ... ,En} é um unificador mais geral (umg) se e somente se para cada unificador para o conjunto, existe uma substituição tal que = .
14
Unificação Def.5 Um conjunto de termos D é o
conjunto de discórdia de um conjunto de expressões E = {E1, ... ,En} se e somente se: (i) D = , se n = 1 (ii) D = {t1, ... ,tn}, se n > 1 e todas as
expressões em E são idênticas até o i-ésimo símbolo, exclusive, e t1, ... ,tn são os termos ocorrendo em E1, ... ,En que começam na posição i.
15
Unificação Exemplo1:
E = {P(x), P(a)}D = {x, a}
Exemplo2:E = {P(x, f(y, z)), P(x, a), P(x, g(h(k(x))))}D = {f(y, z), a, g(h(k(x)))}
16
Unificação Exemplo1: Discórdia de E1
E1 = {P(x), P(a)}
Exemplo2: Discórdia de E2 E = {P(x, f(y, z)), P(x, a), P(x,
g(h(k(x))))}
D = {x, a}
D = {f(y, z), a, g(h(k(x)))}
17
Algoritmo de Unificação1. Faça k = 0, Ek = E e sk =
2. Se Ek é um conjunto unitário, pare. sk é um unificador mais geral para E. Caso contrário, encontre o conjunto discórdia Dk de Ek.
3. Se existem vk e tk em Dk tal que vk é uma variável que não ocorre em tk, vá para 4. Caso contrário, pare. E não é unificável.
4. Faça sk+1= sk{ vk/tk } e Ek+1= Ek{ vk/tk }
5. Faça k = k+1 e vá para 2.
18
Algoritmo de Unificação
Exemplo: E = {P(a, x, f(g(y))), P(z, f(z), f(u))}
K= 0 S0 =
E0 = {P(a, x, f(g(y))), P(z, f(z), f(u))}
D0 = {a, z}. v0 = z e t0 = a.
S1 = s0 {v0/t0} = {z/a} = {z/a}
E1= E0.{v0/t0} = {P(a, x, f(g(y))), P(a, f(a), f(u))}
D1 = {x, f(a)}. v1 = x e t1 = f(a)
K = 1S2 = s1{v1/t1} = {z/a}{x/f(a)} = {z/a, x/f(a)} E2 = E1. { v1/t1} = {P(a, f(a), f(g(y))), P(a, f(a), f(u))}D2 = {g(y), u} v2 = u e t2 = g(y)
K = 2
19
Algoritmo de Unificação
Exemplo: E = {P(a, x, f(g(y))), P(z, f(z), f(u))}
Continuação ...
S3 = s2 {v2/t2} = {z/a, x/f(a), u/g(y)} E3 = E2.{v2/t2} = {P(a, f(a), f(g(y))), P(a, f(a), f(u))}.{g(y)/u} =
{P(a, f(a), f(g(y))), P(a, f(a), f(g(y)))} = { P(a, f(a), f(g(y)))}K = 3 Visto E3 ser unitário, S3 é um umg
S3 = {z/a, x/f(a), u/g(y)} para E.
E = {P(a, x, f(g(y))), P(z, f(z), f(u))}
20
Resolução: Definições
Def.6 Se dois ou mais literais (com o mesmo sinal) de uma única cláusula C tem um unificador mais geral , então C é chamado um fator de C
21
Resolução: DefiniçõesExemplo: Seja C = P(x) P(f(y)) ~Q(x)
P(x) e P(f(y)) tem um umg = {x/f(y)}
C = P(f(y)) ~Q(f(y)) é um fator de C.
22
Resolução: Definições Def.7 Sejam C1 e C2 duas cláusulas
sem variáveis comuns. Sejam L1 e L2 literais de C1 e C2, respectivamente. Se L1 e ~L2 tem um unificador mais geral , então a cláusula:
(C1 L1) (C2 L2)
é chamada um resolvente binário de C1 e C2.
23
Resolução: DefiniçõesExemplo:
Sejam C1: P(x) Q(x) (C2 não tem x)
C2: ~P(a) R(y) (C1 não tem y)
literais L1 = P(x) L2 = ~P(a), então, ~L2 = P(a).
umg de L1 e L2 é = {x/a}
logo, (C1 L1) (C2 L2) = Q(a) R(y) um resolvente binário de C1 e C2.
24
Resolução: Definições Def.8 Um resolvente de cláusulas C1 e
C2 é um dos seguintes resolventes binários:
(i) um resolvente binário de C1 e C2(ii) um resolvente binário de C1 e um fator de C2(iii) um resolvente binário de um fator de C1 e C2(iv) um resolvente binário de um fator de C1 e um fator de C2
25
Resolução: Definições Exemplo: Sejam
C1 = P(x) P(f(y)) R(g(y))C2 = ~P(f(g(a))) Q(b)
Um fator de C1 é:C1’ = P(f(y)) R(g(y))
Um resolvente binário de C1’ e C2 é: C = R(g(g(a))) Q(b)
26
Resolução: Definições
Teorema 2: Se C é um resolvente de duas cláusulas C1 e C2 então C é consequência lógica de C1 e C2.
27
O Sistema Formal da Resolução
Def.9 O Sistema Formal da Resolução R consiste de: (i) Classe de linguagens
Para cada alfabeto de 1a ordem, o conjunto das cláusulas sobre este alfabeto.
(ii) Axiomas Nenhum.
(iii) Regras de Inferência Regra da Resolução definida como:
Se C’ e C’’ são cláusulas e C é um resolvente de C’ e C’’, então derive C de C’ e C’’
28
O Sistema Formal da Resolução
Observe que a noção de uma dedução (derivação ou prova) em R é formalizada de maneira semelhante à noção de dedução em um sistema formal axiomático, no qual usa-se regras de inferência e axiomas.
29
O Sistema Formal da Resolução
Teorema 3: Teorema da Correção Para todo conjunto S de cláusulas, se
existe uma refutação a partir de S em R, então S é insatisfatível. “tudo que se deriva é semanticamente correto”
Teorema 4: Teorema da Completude Para todo conjunto S de cláusulas, se S é
insatisfatível, então existe uma refutação a partir de S em R. “se é consequência lógica existe uma derivação”
30
Exemplos de Aplicações: Banco de Dados
Exemplo 1: Considere o Banco de Dados que segue a seguinte Questão ou Consulta:
Quem é o chefe de João?
gerente(Vendas, José) lotado(João, Vendas) lotado(y, x) & gerente(x, z) chefe(y, z)
FATOS
REGRA
31
Exemplos de Aplicações: Banco de Dados
Transformando essa descrição para cláusulas e fazendo derivações:1. gerente(Vendas, José)2. lotado(João, Vendas)3. ~lotado(y, x) ~gerente(x, z) chefe(y, z)4. ~lotado(y, Vendas) ~gerente(Vendas, José) chefe(y, José) 5. ~lotado(y, Vendas) chefe(y, José) 1, 3 R6. ~lotado(João, Vendas) chefe(João, José)7. chefe(João, José) 2, 5 R
32
Exemplos de Aplicações: Banco de Dados
Exemplo 2: A figura que segue representa a maneira que umas caixas estão arrumadas:
C
A B chão
Use a Linguagem da Lógica de 1a Ordem para descrever essa arrumação, ou seja, as caixas que estão no topo, no chão e o que está sobre cada caixa.
Uma regra de restrição observada para as caixas que estão no topo é: “as caixas que estão no topo, não têm nenhuma caixa sobre elas”.
33
Exemplos de Aplicações: Banco de Dados
Descrição da situação:1. chão(A)2. chão(B)3. topo(C)4. sobre(C, A)5. x(topo(x) ~y(sobre(y, x))
Questão: tem algum bloco sobre o bloco C?
FATOS
REGRA
34
Exemplos de Aplicações: Banco de Dados
Transformando para cláusulas e fazendo derivações:
1. chão(A)2. chão(B)3. topo(C)4. sobre(C, A)5. ~topo(x) ~sobre(y, x)7. ~topo(C) ~sobre(y, C)8. ~sobre(y, C)
35
Métodos Básicos de Resolução(Refutação)
Método de Resolução por Saturação1. Dado um conjunto finito de cláusulas S,
construa uma sequência S0, S1, ... de conjuntos de cláusulas da forma seguinte:S0 = SSn+1= Sn {C : C é um resolvente de cláusulas em Sn}
2.Pare com SIM quando for gerada.
3.Pare com NÃO quando não houver novos resolventes a derivar.
36
Métodos Básicos de Resolução(Refutação)
Esse procedimento: sempre pára com SIM quando S for
insatisfatível (método é refutacionalmente completo)
nunca pára quando S for satisfatível e existir um conjunto infinito de resolventes obtidos a partir de S
sempre pára com NÃO quando S for satisfatível mas o conjunto de resolventes obtido a partir de S é finito.
37
Exemplo: S = {P Q, ~P Q, P ~Q, ~P ~Q}
S0: 1. P Q
2. ~P Q 3. P ~Q 4. ~P ~Q
S1: 5. Q 1. e 2. 6. P 1. e 3. 7. Q ~Q 1. e 4. 8. P ~P 1. e 4. 9. Q ~Q 2. e 3. 10. P ~P 2. e 3. 11. ~P 2. e 4. 12. ~Q 3. e 4.
38
Exemplo (continuação):
S2:
13. P Q 1. e 7. 14. P Q 1. e 8.
.
.
. 37. Q 5. e 7. 38. Q 5. e 9. 39. 5. e 12.
39
Métodos Básicos de Resolução(Refutação)
Outros métodos com implementações mais eficientes: Método por Saturação com Filtragem Método de Resolução por conjunto de Suporte Método da Resolução Linear
Esses métodos implementam a Resolução visando otimização. Para isso, evitam gerar resolventes (novas cláusulas) que sejam irrelavantes a decisão de insatisfatibilidade do conjunto de cláusulas.
O método mais eficiente é o da Resolução Linear, segue um exemplo:
40
Métodos Básicos de Resolução(Refutação Linear)
Exemplo: Seja S o seguinte conjunto de cláusulas: 1. chama(a, b) 2. usa(b, e) 3. ~chama(x, y), depende(x, y) 4. ~usa(x, y), depende(x, y) 5. ~chama(x, z), ~depende(z, y), depende(x, y)
Questão: depende(a, e) ?
A seguinte sequência de cláusulas é uma refutação linear a partir de S:
41
1. chama(a, b) 2. usa(b, e) 3. ~chama(x, y), depende(x, y) 4. ~usa(x, y), depende(x, y) 5. ~chama(x, z), ~depende(z, y), depende(x,
y) 6. ~depende(a, e) (negação da tese)
7. ~chama(a, z), ~depende(z, e) 6, 5 R 8. ~depende(b, e) 7, 1 R 9. ~usa(b, e) 8, 4 R 10. 9, 2 R
Métodos Básicos de Resolução(Refutação Linear)