Princípio da resolução

Prévia do material em texto

Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Matemática Discreta
Princípio da Resolução
Prof Edjard Mota
edjard@icomp.ufam.edu.br
1
Baseado nas Notas de aula do professor
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Exemplo: p e ¬p
Formas Normais
Definição 2. Uma fórmula 휙 está na Forma Normal Conjuntiva 
(FNC), sss 휙 é uma conjunção de disjunção de literais.
Definição 1. Um literal é um átomo proposicional ou negação dele. 
Assim, se 휙 é um átomo, então ¬휙 é seu complemento. Dizemos 
que 휙 e ¬휙 são literais complementares. E.g. p e ¬p
Exemplo de FNC: (¬p ∨ q ∨ r) ⋀ (¬q ∨ r) ⋀ (¬r)
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Exemplo: p e ¬p
Formas Normais
Definição 2. Uma fórmula 휙 está na Forma Normal Conjuntiva 
(FNC), sss 휙 é uma conjunção de disjunção de literais.
Definição 1. Um literal é um átomo proposicional ou negação dele. 
Assim, se 휙 é um átomo, então ¬휙 é seu complemento. Dizemos 
que 휙 e ¬휙 são literais complementares. E.g. p e ¬p
Exemplo de FNC: (¬p ∨ q ∨ r) ⋀ (¬q ∨ r) ⋀ (¬r)
Não em FNC: (¬p ∨ q ∨ r) ⋀ ((p ⋀ ¬q) ∨ r)) ⋀ (¬r)
Não em FNC: (¬p ∨ q ∨ r) ⋀ ¬(q ∨ r) ⋀ (¬r)
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Formas Normais
Definição 3. Uma fórmula 휙 está na Forma Clausal, ou 
forma de cláusula se
1.휙 for um conjunto de vazio literais (cláusula vazia ou ☐)
2.휙 tem apenas um literal (cláusula unitária)
3.휙 for um conjunto ou uma disjunção de literais 
Exemplos: ☐, {¬p}, {p, q,¬r} ou (p ∨ q ∨ ¬r)
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Resolução
Definição 4. (Resolução) Duas cláusulas α e β pode ser resolvidas
se, e somente se elas contiverem literais complementares, ou seja se
p ∈ α então ¬p ∈ β. Os literais restantes, se houver, formam uma nova
cláusula denominada de cláusula resolvente, e α e β são parentais.
Definição 3. Um literal é um átomo proposicional ou negação dele. 
Assim, se 휙 é um átomo, então ¬휙 é seu complemento. Dizemos 
que 휙 e ¬휙 são literais complementares.
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Exemplos .
Resolução
Definição 4. (Resolução) Duas cláusulas α e β pode ser resolvidas
se, e somente se elas contiverem literais complementares, ou seja se
p ∈ α então ¬p ∈ β. Os literais restantes, se houver, formam uma nova
cláusula denominada de cláusula resolvente, e α e β são parentais.
Definição 3. Um literal é um átomo proposicional ou negação dele. 
Assim, se 휙 é um átomo, então ¬휙 é seu complemento. Dizemos 
que 휙 e ¬휙 são literais complementares.
Resolução entre parentais Gera resolvente
p ¬p ∨ q q
p ∨ ¬q ∨ r ¬s ∨ q p ∨ r ∨ ¬s
p ¬p ☐
Modus Ponens
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Exemplos .
Resolução
Definição 4. (Resolução) Duas cláusulas α e β pode ser resolvidas
se, e somente se elas contiverem literais complementares, ou seja se
p ∈ α então ¬p ∈ β. Os literais restantes, se houver, formam uma nova
cláusula denominada de cláusula resolvente, e α e β são parentais.
Definição 3. Um literal é um átomo proposicional ou negação dele. 
Assim, se 휙 é um átomo, então ¬휙 é seu complemento. Dizemos 
que 휙 e ¬휙 são literais complementares.
Resolução entre parentais Gera resolvente
p ¬p ∨ q q
p ∨ ¬q ∨ r ¬s ∨ q p ∨ r ∨ ¬s
p ¬p ☐
Modus Ponens
!????!
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
● Se C1 e C2 são cláusulas unitárias de literais 
complementares, então o resolvente entre C1 e 
C2 é uma clausula vazia.(☐).
● Se podemos derivar ☐ de um conjunto S de 
clausulas, então S é insatisfazível.
Definição 5. (Dedução) Seja S um conjunto de
cláusulas. Uma dedução (por resolução) de uma cláusula
C a partir de S é uma sequência finita C1, C2, …, Ck em
que cada Ci ∈ S ou é uma clausula resolvente de
clausulas que precedem Ci, e Ck = C.
Resolução e Satisfatibilidade
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Definição 5. (Dedução) Seja S um conjunto de 
cláusulas. Uma dedução (por resolução) de uma cláusula 
C a partir de S é uma sequência finita C1, C2, …, Ck em 
que cada Ci ∈ S ou é uma clausula resolvente de 
clausulas que precedem Ci, e Ck = C.
Resolução e Satisfatibilidade
Definição 6. (Completude) Seja S = {C1, C2, …, Ck} e G
uma formula. Dizemos que G é uma consequência lógica de
S , S ⊨G, sss S ∪ {¬G}, isto é, existe uma dedução de ☐.
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Resolução e Satisfatibilidade
Exemplo1: Seja S = {C1, C2, C3}, C1, = ¬p ∨ q, C2, = p
e C3 = ¬q.
C4 = q (Resolvente de C1 e C2)
C5 = ☐ (Resolvente de C4 e C5)
Exemplo2: Prove, por resolução, que S é insatisfazível
S = {¬q ∨ p, ¬p ∨ ¬q, q ∨ r, ¬q ∨ ¬r, ¬p ∨ ¬r, p ∨ r}.
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Se considerarmos.
P: O congresso se recusa a agir.
Q: Encerrou a greve.
R: O presidente da empresa renuncia.
S: A greve dura mais que um ano.
“Se o congresso se recusar a criar novas leis, então a greve não 
terminará, a menos que dure mais de um ano e o presidente da 
empresa renuncie. Se a greve começou a poucas horas e o congresso 
se recusar, podemos concluir que a greve nunca terminará?”
Resolução e Satisfatibilidade
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Se considerarmos.
P: O congresso se recusa a agir.
Q: Encerrou a greve.
R: O presidente da empresa renuncia.
S: A greve dura mais que um ano.
“Se o congresso se recusar a criar novas leis, então a greve não 
terminará, a menos que dure mais de um ano e o presidente da 
empresa renuncie. Se a greve começou a poucas horas e o congresso 
se recusar, podemos concluir que a greve nunca terminará?”
Teremos
F1: (P → (¬Q ∨ (R ⋀ S))),
F2: P.
F3: ¬S.
G: ¬Q.
Resolução e Satisfatibilidade
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Se considerarmos.
P: O congresso se recusa a agir.
Q: Encerrou a greve.
R: O presidente da empresa renuncia.
S: A greve dura mais que um ano.
“Se o congresso se recusar a criar novas leis, então a greve não 
terminará, a menos que dure mais de um ano e o presidente da 
empresa renuncie. Se a greve começou a poucas horas e o congresso 
se recusar, podemos concluir que a greve nunca terminará?”
Teremos
F1: (P → (¬Q ∨ (R ⋀ S))),
F2: P.
F3: ¬S.
G: ¬Q.
Resolução e Satisfatibilidade
Provar por resolução que
F1⋀ F2⋀ F3⊨ G
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Teremos
F1: (P → (¬Q ∨ (R ⋀ S)))
(P → ((¬Q ∨ R) ⋀ (¬Q ∨ S)) [Distributividade]
(¬P ∨ ((¬Q ∨ R) ⋀ (¬Q ∨ S)) [Condicional]
1. ¬P ∨ ¬Q ∨ R
2. ¬P ∨ ¬Q ∨ S
3. P
4. ¬S
5. Q [Negação de G]
Resolução e Satisfatibilidade
[Distributividade]
Aula 04 Copyright 2018 Instituto de Computação-UFAM - Edjard Mota
Teremos
F1: (P → (¬Q ∨ (R ⋀ S)))
(P → ((¬Q ∨ R) ⋀ (¬Q ∨ S)) [Distributividade]
(¬P ∨ ((¬Q ∨ R) ⋀ (¬Q ∨ S)) [Condicional]
1. ¬P ∨ ¬Q ∨ R
2. ¬P ∨ ¬Q ∨ S
3. P
4. ¬S
5. Q [Negação de G]
Resolução e Satisfatibilidade
[Distributividade]
6. ¬Q ∨ S [Resolvente de 3 e 2]
7. S [Resolvente de 6 e 5]
8. ☐ [Resolvente de 7 e 4]