1 Resolução. 2 Equivalências de 1 a Ordem As leis de equivalência lógica permitem simplificar fórmulas da Lógica de 1a Ordem em fórmulas equivalentes,

1

Resolução

2

Equivalências de 1a Ordem

As leis de equivalência lógica permitem simplificar fórmulas da Lógica de 1a Ordem em fórmulas equivalentes, porém mais simples – Forma Normal Prenex.

Na forma Prenex todos os quantificadores encontram-se no início da fórmula. Veremos uma outra forma normal, na qual elimina-se os quantificadores existenciais – Forma Normal de skolem

3

Forma Normal Skolem Essa forma elimina os quantificadores

existenciais de uma forma prenex obtendo uma generalização

A eliminação do existencial é obtida pelo seguinte procedimento proposto por Skolem:

4

Procedimento de Eliminação de Quantificadores Existenciais

Seja uma fórmula na forma normal prenex Q1x1, ..., Qnxn(M), onde M está na forma normal conjuntivae Qr um quantificador existencial no prefixo de Q1x1, ... ,Qnxn, 1 r n.

A eliminação de Qnxn é feita observando-se os quantificadores que o antecedem. Ocorre da seguinte maneira:

5


Se não existir nenhum quantificador universal anterior a Qrxr no prefixo, faça: escolha uma nova constante c diferente de

qualquer outra que ocorre em M, substitua todos os xr ocorrendo em M por c e elimine Qrxr do prefixo.

senão ...

6

... senão .., Se Qs1, ... ,Qsm são os quantificadores

universais anteriores a Qr no prefixo, 1 s1 < s2 < ... < sm < r, faça: escolha um novo símbolo funcional m-ário f

diferente de outros símbolos funcionais ocorrendo em M,

substitua todos os xr ocorrendo em M pelo termo f(s1, ... , sm) e

elimine Qrxr do prefixo.


7

Depois do processo de eliminação (skolemização) ser aplicado a todos os quantificadores existenciais do prefixo, a fórmula obtida está na forma normal de skolem, denotada por skolem().


8

Exemplo: obter skolem() = xyzu(P(x, y, z, u))

1. x não é precedido de quantificador universal, então:

yzu(P(a, y, z, u))

2. u é precedido por yz, então: yz (P(a, y, z, f(y, z)))


9


Observe a semântica da função skolem:

Considere o predicado Mãe definido com o seguinte significado:

Mãe(x,y): x é mãe de y

papel do 1o termo: é mãe papel do 2o termo: é filho

10


Exemplo 1: “Todo mundo tem mãe” significa que “para todo x existe um y que é mãe de x “

= xy(Mãe(y,x))

skolem( = x(Mãe(f(x),x))

a função f expressa que o valor de y: a mãe, depende do valor de x: o filho

11


Exemplo 2: “Existe alguém que é mãe de todos” =“existe um x que para todo y, x é mãe de y “

= xy(Mãe(x,y))

skolem( = y(Mãe(a,y))

a constante a pode ser = “Nossa Senhora”

12


Exemplo: obter skolem() = (xyz((~P(x,y) ^ Q(x,z)) v

R(x,y,z))

xyz((~P(x,y) ^ Q(x,z)) v R(x,y,z))xyz((~P(x,y) v R(x,y,z)) ^ (Q(x,z) v R(x,y,z)))xz((~P(x,f(x)) v R(x,f(x),z)) ^ (Q(x,z) v R(x,f(x),z)))x((~P(x,f(x)) v R(x,f(x),g(x)) ^ (Q(x,g(x)) v

R(x,f(x),g(x))))

13

Forma Normal Skolem Teorema 1: Seja um fórmula de 1a

ordem. Então, é insatisfatível se e somente se skolem() é insatisfatível.

As outras formas normais preservam os modelos das fórmulas originais (são tautologicamente equivalentes)

A forma normal de skolem preserva apenas a condição de insatisfatibilidade da fórmula original.

14

Forma Normal Skolem Exemplo:

Seja = x(P(x)) então, skolem() = P(a)

Seja I a seguinte interpretação :D = {1, 2}aI = 1PI(1) = FPI(2) = V

Então, I satisfaz , mas não satisfaz skolem().

15

Representação Clausal de Fórmulas

Def.2 Um literal é uma fórmula atômica (literal positivo) ou a negação de uma fórmula atômica (literal negativo).

Def.3 Uma cláusula é uma disjunção de literais Exemplo: P(x) Q(a) ~R(y)

16


Por conveniência, uma cláusula pode também ser representada como um conjunto, o conjunto de seus literais.

Exemplo: {P(x), Q(a), ~R(y)}

17


Def.4 A cláusula vazia é uma cláusula sem literais (conjunto vazio) e é representada por e Representa uma fórmula insatisfatível ( ^ ~).

Qualquer fórmula de 1a ordem pode ser transformada em um conjunto de cláusulas.

18

Procedimento de Transformação de Fórmulas em Cláusulas

1. Eliminar usando a “lei” a b |=|(a b)^(b a) 2. Eliminar usando a “lei” a b |=| ~ a b 3. Reduzir escopo de ~ usando a “lei” de De Morgan

e outras “leis” 4. Renomear variáveis 5. Skolemizar 6. Converter para a Forma Normal Prenex 7. Converter matriz para a Forma Normal Conjuntiva 8. Eliminar quantificadores universais 9. Eliminar ^ e obter o conjunto de cláusulas

19

Exemplo:Transformar em cláusula =x(P(x) (y(P(y) P(f(x, y))) ^ ~y(Q(x, y) P(y))))

1. x(~P(x) (y(~P(y) P(f(x, y))) ^ ~y(~Q(x, y) P(y))))2. x(~P(x) (y(~P(y) P(f(x, y))) ^ y(~(~Q(x, y) P(y))))3. x(~P(x) (y(~P(y) P(f(x, y))) ^ y(Q(x, y) ^ ~P(y))))4. x(~P(x) (y(~P(y) P(f(x, y))) ^ w(Q(x, w) ^ ~P(w))))5. x(~P(x) (y(~P(y) P(f(x, y))) ^ (Q(x, g(x)) ^ ~P(g(x)))))6. xy (~P(x) ((~P(y) P(f(x, y)) ) ^ (Q(x, g(x)) ^ ~P(g(x)) )))

8. xy((~P(x) ~P(y) P(f(x, y))) ^ (( ~P(x) Q(x, g(x))) ^ (~P(x) ~P(g(x)))))

9.{ ~P(x) ~P(y) P(f(x, y)), ~P(x) Q(x, g(x)), ~P(x) ~P(g(x)) }

7. xy ( (~P(x) (~P(y) P(f(x, y)))) ^ (~P(x) v (Q(x, g(x)) ^ ~P(g(x)) )))

20

Exemplo: Transformar em cláusula =x(P(x) (y(P(y) P(f(x, y))) ^ ~y(Q(x, y) P(y))))

A fórmula foi transformada em um conjunto, S, de 3 cláusulas :

S= {~P(x) ~P(y) P(f(x, y)), ~P(x) Q(x, g(x)), ~P(x) ~P(g(x)) }

21

Exemplo: Fazer a representação clausal de um estado do “Dicionário”

Exemplo: A transformação da fórmula 12 em cláusulas

xyz((depende(x, z) & depende(z, y)) depende(x, y))xyz(~(depende(x, z) & depende(z, y))v depende(x, y))xyz((~depende(x,z) v ~depende(z,y)) v depende(x,y))

S = {~depende(x,z) v ~depende(z,y) v depende(x,y)}

A fórmula 12 foi transformada em um conjunto S de apenas uma cláusula

22


Representação clausal após as transformações: 1. programa(a, fortran) 2. programa(b, pascal) 3. programa(c, fortran) 4. arquivo(d, sequencial) 5. arquivo(e, direto) 6. chama(a, b) 7. chama(a, c) 8. usa(a, d) 9. usa(b, e) Continua...

Um fórmula atômica é uma cláusula.cada fato (dado) do “Dicionário” já estava representado por uma fórmula atômica.

23


Continuação... 10. ~chama(x, y) depende(x, y) 11. ~usa(x, y) depende(x, y) 12. ~depende(x, z) ~depende(z, y) depende(x, y)

cada regra foi transformada em conj. de cláusulas

As três últimas cláusulas também podem ser representadas por conjunto de literais: 10’. ~chama(x, y), depende(x, y)) 11’. ~usa(x, y), depende(x, y) 12’. ~depende(x, z), ~depende(z, y), depende(x, y)

24

Representação clausal completa: 1. programa(a, fortran) 2. programa(b, pascal) 3. programa(c, fortran) 4. arquivo(d, sequencial) 5. arquivo(e, direto) 6. chama(a, b) 7. chama(a, c) 8. usa(a, d) 9. usa(b, e) 10. ~chama(x, y) depende(x, y) 11. ~usa(x, y) depende(x, y) 12. ~depende(x, z) ~depende(z, y)

depende(x, y)


FATOS

REGRAS

25

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 construída é dita ser um resolvente de C1 e C2.

26

Resolução Considere as seguintes cláusulas C1 e

C2 abaixo: C1: P R C2: ~P Q

R Q é um resolvente de C1 e C2.

27

Resolução Teorema 1: Dado duas cláusulas C1 e C2, um

resolvente C de C1 e C2 é conseqüê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 seqüê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.

28

Resolução Exemplo: Prove que o conjunto de cláusulas

S é insatisfatível: S = {~P Q, ~Q, P}

1. ~P Q C12. ~Q C23. P C34. Q de 1 e 3, R5. de 4 e 2, R

29

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)

30

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)

31

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)

32

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)

33

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} excluindo-se os seguintes elementos:xj/tj para o qual tj = xj e yi/ui tal que yi {x1, ... ,xn}.

34

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 }

35

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.

36

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 = .

37

UnificaçãoExemplo: E = {Q(x), Q(f(y))}

Entre outras possíveis substituições, unifica E = {x/f(a) , y/a} e o umg = {x/f(y)}

Existe uma substituição tal que =

Essa substituição seria: = {y/a} {x/f(a) , y/a} = {x/f(a) , y/a} = {x/f(y)} {y/a} {x/f(a) , y/a} = {x/f(a), y/a}

Para outra substituição = {x/f(f(a)), y/f(a)}, seria {y/f(a)}

38

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.

39

Unificação Exemplo1: Discórdia de E1

E1 = {P(x), P(a)}

Exemplo2: Discórdia de E2 E2 = {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)))}

40

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.

41

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

42

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))}

43

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

44

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.

45

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.

46

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.

47

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

48

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)

49

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.

50

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’’

51


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.

52


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”

53

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

54


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

55


Exemplo 2: A figura que segue representa a maneira que umas caixas estão arrumadas:

CA 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”.

56


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

57


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)

58

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.

59


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.

60

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.

61

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.

62


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:

63

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:

64

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


65


Exemplo 2: Seja S o seguinte conjunto de cláusulas: 1. genitor(pam, bob) 2. genitor(tom, bob) 3. genitor(tom, liz) 4. genitor(bob, ana) 5. genitor(bob, pat) 6. genitor(pat, jim) 7. ~genitor(X,Z) v descendente (X,Z) 8. ~genitor(X,Y) v ~descendente (Y,Z) v descendente(X,Z)

Questão: descendente(tom,pat) ?

A seguinte sequência de cláusulas é uma refutação linear a partir de S:

FATOS

REGRAS

66

1. genitor(pam, bob) 2. genitor(tom, bob) 3. genitor(tom, liz) 4. genitor(bob, ana) 5. genitor(bob, pat) 6. genitor(pat, jim) 7. ~genitor(X,Z) v descendente (X,Z) 8. ~genitor(X,Y) v ~descendente (Y,Z) v descendente(X,Z) 9. ~descendente(tom, pat) (negação da tese)

10. ~genitor(tom,Y) v ~descendente (Y, pat) v descendente(tom, pat) 8. X/tom, Z/pat

11. ~genitor(tom,Y) v ~descendente (Y, pat) 10, 9 R 12. ~genitor(tom, bob) v ~descendente (bob, pat) 11. Y/bob 13. ~descendente (bob, pat) 12, 2 R 14. ~genitor(bob, pat) v descendente (bob, pat) 7, X/bob, Z/pat 15. ~genitor(bob, pat) 14, 13 R 10. 15, 5 R


Documents

1 Resolução. 2 Equivalências de 1 a Ordem As leis de equivalência lógica permitem simplificar fórmulas da Lógica de 1a Ordem em fórmulas equivalentes,