Lógica para Computação - Revisão para Miniprova 4 CIN UFPE

Prévia do material em texto

Aula 3 Lógica 
para computação
SATISFABILIDADE, TABELA-VERDADE, TABLEAUX ANALÍTICOS E MÉTODO DA RESOLUÇÃO
ARTHUR JORGE EBRAHIM WANDERLEY – AJEW
WELLINGTON BARBOSA DE ALMEIDA - WBA
Satisfatibilidade:
 Definição:
Seja φ uma proposição pertencente a PROP:
– Φ é satisfatível se existe pelo menos uma valoração W tal 
que: ŵ(φ) = 1
– Φ é refutável se existe pelo menos uma valoração W tal que: 
 ŵ(φ) = 0
– Φ é tautologia se, para toda valoração W: 
 ŵ(φ) = 1
– Φ é insatisfatível se, para toda valoração W: 
 ŵ(φ) = 0
Satisfatibilidade:
 Consequência lógica:
Sejam ɣ e φ pertencentes a PROP:
ɣ é consequência lógica de φ se, para toda valoração W, se W satisfaz φ, 
então W satisfaz também ɣ, ou seja:
ŵ(φ) = 1 -> ŵ(ɣ) = 1
 
* Notação: φ ⊨ ɣ
Métodos para resolver os 
problemas de satisfatibilidade 
(SAT):
 Tabela – verdade;
 Método dos tableaux analíticos;
 Método da resolução;
 Dedução Natural;
Tabela – verdade
 Neste método, faremos uma tabela na qual suas colunas serão 
as subexpressões da expressão dada e as linhas serão as 
possíveis valorações para todas as variáveis
 Vantagens: Simplicidade e confiabilidade
 Desvantagens: Alto custo computacional ( O(2^n) )
- Porém, para sabermos se a expressão é satisfatível, 
precisamos somente de 2K + 1 operações, após termos terminado 
de montar a tabela
Tabela – verdade
 Satisfatibilidade:
 Φ é satisfatível se existe pelo menos uma valoração W tal que: 
 ŵ(φ) = 1
 Φ é refutável se existe pelo menos uma valoração W tal que: 
 ŵ(φ) = 0
 Φ é tautologia se, para toda valoração W: 
 ŵ(φ) = 1
 Φ é insatisfatível se, para toda valoração W: 
 ŵ(φ) = 0
 ɣ é consequência lógica de φ se, para toda valoração W, se W 
satisfaz φ, então W satisfaz também ɣ (φ ⊨ ɣ)
Tabela – verdade (exemplo)
 Seja φ = ( ( x → (y → z) ) → ( ( ¬ z ) v ( x ^ ( ¬ y ) ) ) ) 
- Quais as conclusões que podemos tirar de φ ?
Tabela – verdade (exemplo)
 Tabela – verdade:
 
Tabela – verdade (exemplo)
 Conclusões:
- φ é satisfatível;
- φ é refutável;
- φ não é tautologia;
- φ não é insatisfatível.
Tabela – verdade (exercício)
Tableaux analíticos
 Neste método, usaremos a noção de “mundo possível”. Para tal, 
construiremos uma “árvore de possibilidades” (valorações – 
verdade), onde cada ramo é um mundo possível e cada nó é uma 
valoração. Para tal, usaremos algumas regras de ramificação que 
vão vir a seguir.
 Vantagens: Método mais intuitivo, e, às vezes, mais eficiente (do 
que o da tabela – verdade)
 Desvantagens: Existem casos onde o custo deste método se 
iguala ao da tabela – verdade (exponencial)
Tableaux analíticos
 Regras de ramificação:
OBS: Sempre opte por aplicar as regras que não ramificam, afim 
de evitar uma árvore com várias ramificações logo no início!
Tableaux analíticos
Tableaux analíticos
 Satisfatibilidade:
Seja φ uma proposição pertencente a PROP:
- φ é satisfatível se existe pelo menos um “mundo possível” 
onde não haja contradições (ramo aberto)
- φ é refutável se existe pelo menos um “mundo possível” onde 
haja uma contradição (ramo fechado)
OBS: Assim como na tabela – verdade, podemos ter uma 
sentença satisfatível e refutável ao mesmo tempo.
Tableaux analíticos
- φ é uma tautologia se não existir um “mundo possível” que 
tenha contradição, ou seja, que não contenha ramos fechados
OBS: Em questões assim, prove para a negação de φ ( é mais 
fácil provar 1 erro do que n acertos =D )
- φ é insatisfatível se todos os “mundos possíveis” tiverem 
contradição, ou seja, que só contenham ramos fechados
OBS: Em questões assim, prove para φ mesmo =D 
Tableaux analíticos
- ɣ é consequência lógica de φ se, para toda valoração W, se W 
satisfaz φ, então W satisfaz também ɣ. Porém, como:
 ϕ |= ɣ sse ϕ U {¬ ɣ } for insatisfatível
Devemos valorar todas as expressões de ϕ como 
verdadeiras e ɣ como falsa, aí então aplicar o método dos 
tableaux analíticos
Tableaux analíticos (exemplo)
 Seja ϕ ≡ { ( l ⟶ i ) ∧ ( ¬ l ⟶ m ), ( i ∨ m ) ⟶ c, c ⟶ b } . 
Verifique se b é consequência lógica de ϕ, ou seja ϕ |= b.
- ϕ |= b sse ϕ U {¬b} for ɣ insatisfatível
Tableaux analíticos (exemplo)
Tableaux analíticos (exemplo)
- Logo, como todos os “mundos possíveis” apresentaram 
contradições (todos os ramos estão fechados), portanto ϕ U {¬b} é 
insatisfatível sim, logo ϕ |= b.
Tableaux analíticos (exercício)
Método da resolução
 Neste método, o mentor tentou criar um “teste rápido”. Embora 
não seja mais eficiente do que o Método da Tabela-Verdade para 
todas as instâncias do problema SAT, é garantido que este teste 
será mais eficiente para entradas de baixo custo.
OBS: Este método responde apenas uma pergunta:
 ϕ é insatisfatível?
Método da resolução
 Conceitos básicos:
– Literal: uma fórmula atômica ou a negação de uma fórmula atômica 
 Ex: a , ¬b
– Cláusula: Uma disjunção de literais 
 Ex: ( a v b), (¬x v y v z)
– Fórmula normal conjuntiva (FNC): Uma fórmula está na FNC se ela 
for uma conjunção de cláusulas 
 Ex: ((a v b) (b v c))
– Cláusula de horn: contém no máximo um literal positivo 
 Ex: (¬x v y v z)
** O custo do método da resolução para uma fórmula que só 
contenha cláusulas de horn é O(n)
Método da resolução
 Regra da resolução de Robinson: Uma fórmula do tipo (x ∨ y) ∧ 
(¬y ∨ z) é logicamente equivalente a (x ∨ y) ∧ (¬y ∨ z) ∧ (x ∨ z). 
Portanto :
Se é insatisfatível, então: é insatisfatível, onde C’ é o 
resultado gerado a partir dos literais Ci e Cj.
Método da resolução
 Algumas equivalências lógicas:
Método da resolução
 Satisfatibilidade:
- Φ é satisfatível se Φ não for insatisfatível
- Φ é refutável se ¬Φ não for insatisfatível
- Φ é tautologia se se ¬Φ for insatisfatível
- ϕ |= ɣ sse ϕ U {¬ ɣ } for insatisfatível
Método da resolução
 Passo a passo do método da resolução:
- Passe todas as fórmulas para a FNC, sem esquecer de negar ɣ
- Após chegar na FNC, ir juntando cláusulas, duas a duas, afim 
de formar novas cláusulas (regra da resolução) até chegar em uma 
contradição
- Achada a contradição, podemos dizer que ϕ U {¬ ɣ } é 
insatisfatível, logo ϕ |= ɣ
** Lembrando que ϕ |= ɣ sse ϕ U {¬ ɣ } for insatisfatível 
Método da resolução (exemplo)
 Seja ϕ ≡ { ( l ⟶ i ) ∧ ( ¬ l ⟶ m ), ( i ∨ m ) ⟶ c, c ⟶ b } . 
Verifique se b é consequência lógica de ϕ, ou seja ϕ |= b.
Método da resolução (exemplo)
Método da resolução (exercício)
Dedução Natural
 Em 1934, Gerhard Gentzen, adaptou regras de dedução 
matemáticas em um método algoritmo de resolução de problemas 
de satisfatibilidade;
 Uma regra de dedução possui o seguinte formato:
Premissa1, Premissa2, … , PremissaN
Conclusão
Dedução Natural
 Em 1965, o lógico sueco Dag Piraulitz formalizou, através de duas 
regras simples, o processo de construção de métodos 
matemáticos usando lógica simbólica;
 As regras:
– Regras de Eliminação;
– Regras de Introdução; 
(Modus Ponens)
P ^ Q
Q
P P->Q
Q
P ^ Q
P
P v Q
[P] [Q]
R R
R
: :
Regras de Eliminação
Regras de Introdução
P
Q v P
Q
P v Q
Q
P → Q
[P]
:
A noção de “prova formal”
 Uma prova formal de uma sentença a partirde 
um conjunto de premissas é uma árvore :
– A raiz é a sentença ;
– As folhas são sentenças de ou sentenças 
introduzidas no decorrer do processo dedutivo;
– Cada nó da árvore representa a aplicação de 
uma das regras;
ϕ
ϕ
Γ
A noção de “derivabilidade”
 Se existir uma prova formal (isto é, uma árvore de 
provas) da sentença a parti do conjunto , 
dizemos que é derivável a parti de .
|-ϕ Γ
ϕ Γ
ϕ Γ
Corretude e completude
 Corretude: se |- então |= 
(Se for derivável, então é verdadeiro)
 Completude: se |= então |- 
(Se for verdadeiro então é derivável) 
ϕ ϕ
ϕ ϕ
Γ Γ
Γ Γ
A prática leva à perfeição I
 (A → B) → ((C → A) → (C → B)) é uma tautologia?
 {(A → B)} |= { (C ^ A) → (C ^ B) } ?
 {(A → B) v (A → C)} |= {A → (B v C)} ?
Observações:
θ
[¬ϕ]
ϕ
T:T
(Prova por vacuidade) (Reduction ad Absurdum)
 é logicamente 
equivalente a 
¬ϕ
ϕ→
T
A prática leva à perfeição II
(¬ϕ→(ϕ→ψ))é umatautologia ?
(¬ψ→¬ϕ)→(ϕ→ϕ)é tautologia?
(ϕ∨¬ϕ)é umatautologia?
(ϕ→ψ)→(¬ψ→¬ϕ)é uma tautologia?
DÚVIDAS??
	Slide 1
	Satisfatibilidade:
	Satisfatibilidade:
	Métodos para resolver os problemas de satisfatibilidade (SAT):
	Tabela – verdade
	Tabela – verdade
	Tabela – verdade (exemplo)
	Tabela – verdade (exemplo)
	Tabela – verdade (exemplo)
	Tabela – verdade (exercício)
	Tableaux analíticos
	Tableaux analíticos
	Tableaux analíticos
	Tableaux analíticos
	Tableaux analíticos
	Tableaux analíticos
	Tableaux analíticos (exemplo)
	Tableaux analíticos (exemplo)
	Tableaux analíticos (exemplo)
	Tableaux analíticos (exercício)
	Método da resolução
	Método da resolução
	Método da resolução
	Método da resolução
	Método da resolução
	Método da resolução
	Método da resolução (exemplo)
	Método da resolução (exemplo)
	Método da resolução (exercício)
	Slide 30
	Slide 31
	Slide 32
	Slide 33
	Slide 34
	Slide 35
	Slide 36
	Slide 37
	Slide 38
	Slide 39
	DÚVIDAS??