Resolução

Prévia do material em texto

Lógica de Predicados 
 Resolução
Resolução
 Não é uma simples extensão da resolução da Lógica 
Proposicional
 Recordando...
Resolução
 A resolução se aplica a fórmulas que são conjunções de disjunções 
de literais, representadas na forma de conjunto de cláusulas
 Seja a fórmula H=(P∨¬Q∨R) ∧(P∨¬Q) ∧(P∨P)
 Esta fórmula é representada na forma de conjuntos como
 H={{P, ¬Q,R}, {P, ¬Q}, {P}}
 H é um conjunto de conjunto de literais, onde as vírgulas mais 
internas representam “∨” e as mais externas “∧”
 A disjunção (P∨¬Q∨R) é representada por {P, ¬Q,R} e (P∨P) por {P} 
pois {P, P} = {P} (Não se representa duplicidade)
Cláusula
 Uma cláusula na Lógica Proposicional é uma disjunção de literais. 
Utilizando a notação de conjuntos, uma cláusula é um conjunto finito de 
literais
 Exemplos: C1= {P, ¬Q,R}, C2={P, ¬Q}, C3={P}
 Dois literais são complementares se um é a negação do outro
 Resolvente de duas cláusulas
 C1={A1, ...,An} e C2={B1, ...,Bn} possuem literais complementares
 Suponha λ um literal de C1 tal que seu complementar, ¬λ, pertence a C2
 Res(C1,C2) = (C1- λ) ∪ (C2 - ¬λ)
 Se Res(C1,C2) = { }, tem-se um resolvente vazio ou trivial
Resolução
 Exemplos de resolvente de duas cláusulas
 Considere C1= {P, ¬Q, R} e C2={¬P, R}
 Res(C1,C2) = {¬Q, R} (que é uma cláusula)
 Considere D1= {P} e D2={¬P}
 Res(D1,D2) = { }
 Considere E1= {P, ¬Q} e E2={¬P, Q}
 Res(C1,C2) = {¬Q, Q}
 A regra de resolução não elimina todos os literais das cláusulas mesmo 
eles sendo complementares
Resolução
 Elementos básicos da resolução
 Alfabeto da Lógica Proposicional
 Conjunto de cláusulas da Lógica Proposicional
 Regra de resolução
 Regra de resolução
 C1={A1, ...,An} e C2={B1, ...,Bn}
 A regra aplicada a C1 e C2 é definida pelo procedimento: tendo C1 e C2 
deduza res(C1,C2)
Expansão por resolução
 Exemplo: {{¬ P, Q, R}, {P,R},{P, ¬R}}
.1 {¬ P, Q, R}
.2 {P, R}
.3 {P, ¬R}
.4 {Q, R} Res(.1,.2)
.5 {Q, P} Res(.3,.4)
.6 {P} Res(.2,.3)
 A expansão é obtida por três aplicações da regra de resolução
 Neste caso, não é possível obter a cláusula vazia
Exemplo de prova por resolução
 ¬Hc={{P1, P2, P3}, {¬P1,P4}, {¬P2,P4}, {¬P3,P4}, {¬P4}}
.1 {P1, P2, P3}
.2 {¬P1,P4}
.3 {¬P2,P4}
.4 {¬P3,P4} 
.5 {¬P4}
.6 {P2, P3, P4} Res(.1,.2)
.7 {P3, P4} Res(.3,.6)
.8 {P4} Res(.4,.7)
.9 { } Res(.5,.8)
 Expansão fechada, logo prova de H
Lógica de Predicados - Resolução
 Cláusulas são obtidas skolemizando fórmulas na forma prenex 
 Algoritmo de unificação é empregado para definir o resolvente de 
duas cláusulas
 Resolução
 Alfabeto da Lógica de Predicados
 Conjunto de cláusulas da Lógica de Predicados
 A regra de resolução da Lógica de Predicados
Regra de resolução - resolvente
 Cláusula em lógica de predicados é uma disjunção de literais
 Usando a notação de conjuntos:
 C1={p(x),q(x)}, C2={¬p(x), ¬r(x,y)}
 Dois literais são complementares quando um é a negação do 
outro
Exemplo de resolvente
 C1={p(x),q(x)}, C2={¬p(x), ¬r(x,y)}
 Res (C1,C2) = {q(x),¬r(x,y)}, que também é uma cláusula
 C3={¬p(a), ¬r(x,y)}
 Res (C1,C3) = {p(x),q(x),¬p(a),¬r(x,y)}
 p(x) e ¬p(a) quase são complementares 
 se x fosse interpretado como a
 Res (C1,C3) = {q(a),¬r(a,y)}
 com x substituído por a
Exemplo de resolvente
 C4={r(x,y)} e C5={¬r(y,f(a)}
 Res(C4,C5)=?
 Na verdade, na resolução sobre a lógica de predicados, r(x,y) 
representa (∀x)(∀y)r(x,y) implicitamente
 Isso exige que as cláusulas antes de serem submetidas à resolução 
estejam em outro tipo de forma normal
Forma Prenex
 Uma fórmula está na forma Prenex quando os quantificadores 
estão na frente da fórmula, ou seja, são identificados 
primeiramente os quantificadores, seguidos de uma fórmula 
aberta. 
 (∀x)(∀y)(r(x,y) ∧ p(y))
 Fórmula aberta em lógica de predicados – não contém 
quantificadores
Forma Prenex
 (∀x)((∀y)r(x,y) ∧ p(y)) está na forma prenex?
 Não!!!
 Na forma prenex, além dos quantificadores estarem no início da 
fórmula, o escopo desses quantificadores deve ser a fórmula 
inteira
 Toda fórmula tem um equivalente na forma prenex
 Como transformá-la em Prenex? – algoritmo prenex
 Regras prenex
 Substituição
Regras prenex
Regras prenex
 As regras prenex deduzem fórmulas equivalentes
 Na regra R1 (∀x)A ∧ B equivale a (∀x)(A ∧ B)
 (∀x)(A∨B) não equivale a (∀x)A ∨ (∀x)B e
 (∃x)(A∧B) não equivale a (∃x)A ∧ (∃x)B e
Regras prenex
 Observa-se que em todas as regras obtém-se fórmulas com 
quantificadores no início. Assim, ao aplicar repetidamente as 
regras a uma fórmula, o resultado pode ser uma fórmula com 
quantificadores no início
 Porém não há como aplicar regras prenex em fórmulas do tipo 
(∀x)A ∨ (∀x)B e (∃x)A ∧ (∃x)B 
 Para solucionar este problemas aplica-se a regra de renomeação 
de variáveis
Regra de renomeação
 (∀x)A ∨ (∀x)B em prenex?
 Se H=(Qx)G, a variável x pode ser renomeada para y, (Qy)G{x<-y}
 Se essa substituição for segura
 Exemplo de substituições seguras
 H = (∀x)(p(x) → (∃x)q(x,y)) contém 2 quantificadores na mesma 
variável x. 
 Renomeando x por z, H1 = (∀z)(p(z) → (∃x)q(x,y))
 Renomeando x por w, H2 = (∀x)(p(x) → (∃w)q(w,y))
 Exemplo de substituições inseguras: 
 (∀x)(∀y)(∀z)(r(x,y,z))
 Renomeando x por y
 (∀y)(∀z)(r(x,y,z)) {x<-y}
Regra de renomeação
 H= (∀x)(p(x)→(∃x)q(x,y)) 
 Regra prenex de renomeação
 (∀x) => (∀z)
 (∃x) => (∃w)
 H2=(∀z)(p(z)→(∃w)q(w,y)) 
 x e z são variáveis diferentes da variável livre y
 H = (∀x)p(x) ∨ (∀x)q(x) 
 É possível aplicar alguma regra prenex neste fórmula?
Regra de renomeação
 H = (∀x)p(x) ∨ (∀x)q(x) 
 É possível aplicar alguma regra prenex nesta fórmula?
Regra de renomeação
 H = (∀x)p(x) ∨ (∀x)q(x) 
 É possível aplicar alguma regra prenex nesta fórmula?
 Não. Pois (∀x)p(x) ∨ (∀x)q(x) não equivale a (∀x)(p(x) ∨ q(x))
 Solução: renomeação
 G = (∀z)p(z) ∨ (∀w)q(w)
 Assim é possível aplicar a regra 8, obtendo:
 E = (∀z)(∀w)(p(z) ∨ q(w)), que está na forma prenex
Algoritmo Prenex
 Passo1: substitua as subfórmulas (A→B) por (¬A∨B)
 Passo2: substitua as subfórmulas ¬(A∧B) por (¬A ∨ ¬B)
 Passo3: substitua as subfórmulas ¬(A∨B) por (¬A ∧ ¬B)
 Passo4: substitua as subfórmulas ¬¬A por A
 Passo5: substitua as subfórmulas ¬(∀x)A por (∃x)¬A
 Passo6: substitua as subfórmulas ¬(∃x)A por (∀x)¬A
 Passo7: substitua as subfórmulas (A↔B) por (A→B)∧(B→A). Volte em 
1 se necessário, até que se obtenha subfórmulas com os conectivos 
∧,∨ e ¬
 Passo8: renomeação prenex
 Passo9: regras prenex
Skolemização
 O método de resolução na lógica de predicados é definido a partir 
de fórmulas que estão na forma prenex e que não contém 
quantificadores existenciais
 Método de eliminação dos quantificadores existenciais – método 
de skolem
Algoritmo de skolemização
 Se H é prenex (Qx1)...(Qxn)G e xi ≠ xj quando i ≠ j
 Para cada quantificador existencial, começando pelo mais 
interno, aplique as regras de skolemização
Exemplo
 H = (∀x)(∀y)(∃z)(∃w)(∀x1)(∃y1)(∀z1) (p(x,y,z,w,w3) → q(x2,x1,y1,z1))
 H1 = (∀x)(∀y)(∃z)(∃w)(∀x1)(∀z1) (p(x,y,z,w,w3) → 
q(x2,x1,f(x1,y,x),z1))
 H2 = (∀x)(∀y)(∃z)(∀x1)(∀z1) (p(x,y,z,f2(y,x),w3) → 
q(x2,x1,f(x1,y,x),z1))
 E = (∀x)(∀y)(∀x1)(∀z1) (p(x,y,f3(y,x),f2(y,x),w3) → q(x2,x1,f(x1,y,x),z1))
 A fórmula E está na forma prenex e não contém quantificadores 
existenciais
Exemplo – Prenex e Skolem
 O que os algoritmos prenex e skolem fazem?
 Transformam H em G = (∀*)E, 
 E está em FNC ou FND
 Em FNC, pode transformar-se numa cláusula
 H=(∀x)(∀z)((∀y1) p(y1)∧((∀y2) q(y2)→(∃y3)(r(x,y3,z)))Prenex
 H=(∀x)(∀z) ((∀y1)p(y1) ∧ ((∀y2) q(y2)→(∃y3)(r(x,y3,z)))
 Passo1: (A→B) por (¬A∨B)
 H=(∀x)(∀z) ((∀y1)p(y1) ∧ (¬(∀y2) q(y2) ∨ (∃y3)(r(x,y3,z)))
 Passo5: ¬(∀x)A por (∃x)¬A
 H=(∀x)(∀z) ((∀y1)p(y1) ∧ ((∃y2)¬q(y2) ∨ (∃y3)(r(x,y3,z)))
 Passo9 (regra 8)
 G=(∀x)(∀z)((∀y1) (p(y1) ∧((∃y2)(∃y3) (¬q(y2) ∨ r(x,y3,z)))
 Passo9 (regra 7)
 G=(∀x)(∀z)(∀y1)(∃y2)(∃y3) (p(y1) ∧(¬q(y2) ∨ r(x,y3,z)))
 G=(∀*)(∃y2)(∃y3)(p(y1) ∧(¬q(y2) ∨ r(x,y3,z)))
Skolem
 G=(∀x)(∀z)(∀y1)(∃y2)(∃y3) (p(y1) ∧(¬q(y2) ∨ r(x,y3,z)))
 G=(∀*) (p(y1) ∧ (¬q(g(y1,z,x)) ∨ r(x,f(y1,z,x),z)))
 Forma clausal
 Hc={[p(y1)],[¬q(g(y1,z,x)), r(x,f(y1,z,x),z)]}
Unificação
 2 fórmulas são unificáveis se e somente se existir uma 
substituição que, se aplicada a ambas, torna-as iguais
 Como unificar??
 Fazendo substituições inteligentes de variáveis nas 2 fórmulas 
 Existe um bom algoritmo para isso...
	Slide 1
	Slide 2
	Slide 3
	Slide 4
	Slide 5
	Slide 6
	Slide 7
	Slide 8
	Slide 9
	Slide 10
	Slide 11
	Slide 12
	Slide 13
	Slide 14
	Slide 15
	Slide 16
	Slide 17
	Slide 18
	Slide 19
	Slide 20
	Slide 21
	Slide 22
	Slide 23
	Slide 24
	Slide 25
	Slide 26
	Slide 27
	Slide 28
	Slide 29
	Slide 30