Lógica para Computação - Lógica Proposicional: Métodos de prova, método da resolução, tableaux, - aula9

Prévia do material em texto

IF673 – Engenharia da Computação 
Cin/UFPE – Anjolina Grisi de Oliveira 
2 
Exemplo 
 φ = ( ((X^Y)v((¬X)^Y)) v ((X^(¬Y))v((¬X)^(¬Y))) ) 
Verifique se φ é tautologia 
 
 Tente desenvolver esse exemplo . Você verá que, como no 
exemplo do unicórnio, a árvore gerada será muito grande, 
mostrando que nem sempre o método do tableaux é a melhor 
solução para problemas SAT. 
 Existem valores onde o número de operações (no 
tableaux) é igual à do método da tabela-verdade, tornando 
esse método ineficiente. 
3 
Considerações sobre o Tableaux 
 Vantagens 
• Mais eficiente que a tabela-verdade em 
alguns casos (quais?) 
• Mais intuitivo 
 Desvantagem principal 
• Não há uma maneira de se determinar em 
que casos o método é eficiente 
4 
O Método da Resolução 
 Consolidado num artigo de 1965 por John Alan 
Robinson, o método da resolução foi concebido com 
o propósito claro de tornar computacionalmente 
viável a solução algorítmica do problema SAT (e 
correlatos), mesmo que para uma classe restrita (e 
computacionalmente reconhecível) de sentenças. 
5 
O Método da Resolução 
 Forma Normal Conjuntiva (FNC) 
 
Literal: Um literal é uma fórmula atômica ou a negação de 
uma fórmula atômica. 
 
Cláusula: Uma cláusula é uma disjunção de literais. 
 
Forma Normal Conjuntiva: Uma fórmula está na forma 
normal conjuntiva se for uma conjunção de cláusulas. 
Ex.: (P  ~Q  R)  (~P  Q) 
6 
O Método da Resolução 
 Equivalências Lógicas: 
 
1) ¬¬φ ≡ φ 2) φ → ψ ≡ ¬φ v ψ 3) ¬(φ ^ ψ) ≡ (¬φ)v(¬ψ) 
 
4) ¬(φ v ψ) ≡ (¬φ)^(¬ψ) 5) φ ^ φ ≡ φ 6) φ v φ ≡ φ 
 
7) φ v (¬φ) ≡ T 8) φ ^ (¬φ) ≡ F 9) φ ^ F ≡ F 
 
10) φ v F ≡ φ 11) φ ^ T ≡ φ 12) φ v T ≡ T 
7 
Forma Norma Conjuntiva 
 
Exemplos: 
 
I) (L→I) ^ (¬L→M) ≡ (¬L v I) ^ (¬¬L v M) ≡ (¬L v I) ^ (L v M) 
 
II) (I v M) → C ≡ ¬(I v M) v C ≡ (¬I ^ ¬M) v C ≡ 
 (C v ¬I) ^ (C v ¬M) 
 
8 
Forma Norma Conjuntiva 
 
Teorema: Para todo φ є PROP, existe φ´ є PROP tal 
que: 
• φ é logicamente equivalente a φ´; 
• φ´ está na FNC (Forma Normal Conjuntiva). 
 
9 
Formas Normal Disjuntiva 
Definição: Uma fórmula F é dita estar em uma 
forma normal disjuntiva se e somente se 
tem a forma F1F2...Fn , com n  1, 
onde cada F1,F2,...,Fn é uma conjunção 
de literais. 
Ex.: (P  ~Q  R)  (~P  Q) 
10 
Forma Normal Disjuntiva 
 
Teorema: Para todo φ є PROP, existe φ´ є PROP tal 
que: 
• φ é logicamente equivalente a φ´; 
• φ´ está na FND (Forma Normal Disjuntiva). 
 
11 
Formas Normais 
Passo 1: Eliminar os conectivos  e . 
Qualquer fórmula proposicional pode ser transformada 
em uma forma normal. 
 
Procedimento: 
(P  Q)  (P  Q)  (Q  P) 
(P  Q)  ~P  Q 
(Chang e Lee) 
12 
Formas Normais 
Passo 2: Trazer o sinal da negação para imediatamente 
antes dos átomos usando a substituição da dupla 
negação e as Leis de Morgan. 
~~P  P 
 ~(P  Q)  ~P  ~Q 
~(P  Q)  ~P  ~Q 
(Chang e Lee) 
Passo 3: Obter a forma normal utilizando as regras 
distributivas e as outras. 
P  (Q  R)  (P  Q)  (P  R) 
P  (Q  R)  (P  Q)  (P  R) 
13 
Formas Normais 
(P  ~Q)  R 
 ~(P  ~Q)  R Impl. 
 (~P  ~~Q)  R Morgan 
 (~P  Q)  R Dupla neg. 
Exemplo: Obter a forma normal disjuntiva para a fórmula a seguir 
(P  ~Q)  R 
 (~P  Q)  R (...continuação) 
 R  (~P  Q) Comut. 
 (R  ~P)  (R  Q) Distrib. 
Exemplo: Obter a forma normal conjuntiva para a fórmula a seguir 
14 
Formas Normais 
1. (A  ~B)  C 
2. (~A  B)  C 
3. ~((~X  A)  B) 
4. (P  (Q  R))  S 
5. ~B  X 
 Obter as formas normais disjuntiva e 
conjuntiva das seguintes fórmulas 
15 
Método de Resolução: observações 
importantes 
Para uma fórmula na FNC ser insatisfatível, é suficiente 
que uma de suas cláusulas seja insatisfatível. 
Para toda φ E PROP: 
 - φ é insatisfatível sse φ não é satisfatível. 
- φ é insatisfatível sse ¬φ é uma tautologia. 
- φ é insatisfatível sse ¬φ não é refutável. 
Um conjunto S de sentenças é satisfatível sse S não é 
insatisfatível. 
φ é uma conseqüência lógica de {ψ1, ψ2, ..., ψn} sse 
 ψ1 ^ ψ2 ^ ... ^ ψn ^ ¬φ é insatisfatível. 
16 
Método de Resolução: observações 
importantes 
Um conjunto S de sentenças é satisfatível sse S não é 
insatisfatível. 
φ é uma conseqüência lógica de {ψ1, ψ2, ..., ψn} sse 
 ψ1 ^ ψ2 ^ ... ^ ψn ^ ¬φ é insatisfatível. 
Teorema da dedução: Dadas fórmulas F1,F2,...,Fn e uma fórmula 
G, G é dita ser consequência lógica de F1,F2,...,Fn (ou 
segue logicamente de F1,F2,...,Fn ) se e somente se a 
fórmula ((F1  F2 ...  Fn )  G) é uma tautologia. 
Teorema: Dadas fórmulas F1,F2,...,Fn e uma fórmula G, G é 
consequência lógica de F1,F2,...,Fn (ou segue logicamente 
de F1,F2,...,Fn ) se e somente se a fórmula (F1  F2 ...  Fn 
 ~G) é insatisfatível. 
17 
Método de Resolução: observações 
importantes 
Teorema da dedução: Dadas fórmulas F1,F2,...,Fn e uma fórmula G, G é dita ser 
consequência lógica de F1,F2,...,Fn (ou segue logicamente de 
F1,F2,...,Fn ) se e somente se a fórmula ((F1  F2 ...  Fn )  G) é uma 
tautologia. 
Teorema: Dadas fórmulas F1,F2,...,Fn e uma fórmula G, G é consequência 
lógica de F1,F2,...,Fn (ou segue logicamente de F1,F2,...,Fn ) se e 
somente se a fórmula (F1  F2 ...  Fn  ~G) é insatisfatível. 
• Os teoremas acima são muito importantes. Mostram que provar 
que uma fórmula é consequência lógica de um conjunto finito 
de fórmulas é equivalente a provar que uma certa fórmula é 
uma tautologia ou é insatisfatível. 
 
• Se G é consequência lógica de F1,F2,...,Fn então a fórmula ((F1 
 F2 ...  Fn )  G) é chamada teorema, e G é chamada de 
conclusão do teorema. 
18 
Método de Resolução 
No exemplo do unicórnio: 
 
B é conseqüência lógica do conjunto 
S = {((L → I) ^ (¬L → M)), ((I v M) → C), (C → B)}? 
Essa pergunta equivale a: 
((L → I) ^ (¬L → M)) ^ ((I v M) → C) ^ (C → B) ^ (¬B) é 
insatisfativel? 
O primeiro passo é mexer com a sentença até chegar na FNC, 
e então nomeamos todas as cláusulas. 
19 
Método de Resolução 
((L → I) ^ (¬L → M)) ^ ((I v M) → C) ^ (C → B) ^ (¬B) 
≡ ((¬L v I) ^ (¬¬L v M)) ^ (¬(I v M) v C) ^ (¬C v B) ^ (¬B) 
≡ (¬L v I) ^ (L v M) ^( (¬I ^ ¬M) v C) ^ (¬C v B) ^ (¬B) 
≡ (¬L v I) ^ (L v M) ^ (¬I v C) ^ (¬M v C) ^ (¬C v B) ^ (¬B) 
 C1 C2 C3 C4 C5 C6 
O segundo passo é criar novas cláusulas para ver 
alguma contradição é gerada. 
- C1 ^ C2 ≡ (I v M) (C7) 
- C7 ^ C4 ≡ (I v C) (C8) 
- C8 ^ C3 ≡ (C v C) ≡ C (C9) 
- C9 ^ C5 ≡ (B) (C10) 
Veja que as cláusulas de número C6 e C10 geram uma 
contradição((¬B) ^ (B)). E geram uma cláusula vazia □ 
20 
O princípio da Resolução 
Para quaisquer duas cláusulas C1 e C2, se existe 
um literal L1 em C1 que é complementar a um 
literal L2 em C2, então apague L1 de C1 e L2 de 
C2, e construa a disjunção das cláusulas restantes. 
A cláusula construída é chamada de resolvente de 
C1 e C2. 
21 
O Método da Resolução 
Teorema: Sejam as cláusulas C1 e C2, um resolvente 
C de C1 e C2 é uma consequência lógica de C1 e C2. 
Se nós temos duas cláusulas unitárias, então o 
resolvente delas, se existe, é a cláusula vazia □. 
Mais importante, se um conjunto S de cláusulas é 
insatisfatível, nós podemos usar o princípio da 
resolução paragerar □ a partir de S. 
22 
O Método da Resolução 
Seja um conjunto S de cláusulas, uma (resolução) 
dedução de C a partir de S é uma sequência finita C1, 
C2, ..., Ck de cláusulas de modo que cada Ci ou é uma 
cláusula de S ou um resolvente de cláusulas que 
precedem Ci, e Ck=C. Uma dedução de □ a partir de S é 
chamada de refutação ou uma prova de S.