Sistemas de Deducao

Esta é uma pré-visualização de arquivo. Entre para ver o arquivo original

Lógica Proposicional
 Sistemas de dedução
 Sistema axiomático (Axiomatização)
 Sistema de dedução natural
 Tableaux
 Resolução
Sistema axiomático
 Objetivo principal da lógica: estudo de estruturas para 
representação e dedução do conhecimento
 Representação do conhecimento - aplicação na Computação
 A execução de um programa possibilita a dedução de um novo 
conhecimento a partir daquele representado a priori
 Sistemas de dedução
 Sistemas formais que estabelecem estruturas que permitem a 
representação e dedução formal do conhecimento
 Os sistemas axiomático e natural definem métodos que produzem 
ou verificam fórmulas ou argumentos válidos
Sistema axiomático
 Definição (sistema axiomático): o sistema axiomático da 
lógica proposicional é definido pela composição dos quatro 
elementos:
 O alfabeto da lógica proposicional
 O conjunto das fórmulas da lógica proposicional
 Um subconjunto das fórmulas – axiomas
 Um conjunto de regras de dedução
 Objetivo do estudo: representação e dedução do 
conhecimento. Como se deduz um novo conhecimento a partir 
de um outro dado a priori
 Conhecimento a priori: representado pelos axiomas
Sistema axiomático
 Definição (axiomas do sistema): fórmulas da lógica proposicional 
determinadas pelos esquemas a seguir, onde E, G e H são 
fórmulas:
Ax1 = ¬(H ∨ H) ∨ H
Ax2 = ¬H ∨ (G ∨ H)
Ax3 = (¬(¬H ∨ G)) ∨ ((¬(E ∨ H)) ∨ (G ∨ E))
Sistema axiomático
 Infinitos axiomas
 Representação equivalente
 Ax1 = (H ∨ H) → H
 Ax2 = H → (G ∨ H)
 Ax3 = (H → G) → ((E ∨ H) → (G ∨ E))
Fazendo G = ¬E, Ax2 = H → (E → H)
 A validade de Ax3 pode ser demonstrada por uma tabela verdade
Sistema axiomático
 Correspondências
 H → G denota (¬H ∨ G)
 H → false denota ¬H
 (H↔G) denota (H → G) ∧ (G → H) 
 (H ∧ G) denota ¬(¬H ∨ ¬G)
 No sistema axiomático os axiomas representam o conhecimento 
a priori.
 Neste sistema os axiomas são tautologias.
Sistema axiomático
 Fundamentação
 Esquema de regra de inferência denominado Modus Ponens
 Definição: Modus Ponens
 Dadas as fórmulas H e G, o esquema de regra de inferência do 
sistema axiomático, Modus Ponens (MP), é definido pelo 
procedimento: tendo H e (H → G) deduza G
G
G)(HH,MP →=
Modus Ponens
 A regra de inferência Modus Ponens determina:
 a partir de 2 argumentos H e (H→G)
 conclui-se G
 Exemplo
 H = “Está chovendo” e
 G = “A rua está molhada”
 Se H é verdadeira, isto é “está chovendo” e a implicação (H→G) 
também é verdadeira, isto é “se está chovendo então a rua está 
molhada” .
 Então conclui-se que G é verdadeira, pela regra de inferência 
Modus Ponens, ou seja “a rua está molhada”.
Modus Ponens
 Mas, atenção!
 Se somente (H→G) é verdadeira não se pode concluir nada 
sobre a veracidade de H ou G
 Regra de inferência Modus Ponens define um procedimento 
sintático de dedução de conhecimento
 Empregado em linguagens de programação como o Prolog
Consequência lógica
 Representação do conhecimento: axiomas + fórmulas extras 
denominadas hipóteses
 Aplicação das regras de inferência aos axiomas e às hipóteses 
=> argumentos denominados consequências lógicas
 Consequências lógicas representam o conhecimento provado a 
partir de axiomas e hipóteses, empregando regras de inferência
Prova de uma fórmula num sistema axiomático
 Sejam H uma fórmula e β um conjunto de fórmulas 
denominadas hipóteses. Uma prova de H a partir de β, no 
sistema axiomático, é uma seqüência de fórmulas H1, H2, ..., 
Hn, onde se tem:
 H=Hn
E para todo i tal que 1≤i≤n,
 Hi é um axioma ou
 Hi ∈ β ou
 Hi é deduzida de Hj e Hk, utilizando a Regra Modus Ponens, onde 
j<i e k<i. Isto é, 
 Necessariamente Hk = Hj → Hi
i
kj 
H
HH
:MP
Exemplo de prova
 Dado o conjunto de hipóteses β = {G1, ..., G9}, apresente a 
sequencia de fórmulas H1, ..., H9 que é uma prova de (S∨P) a 
partir de β, no sistema axiomático.
G1 = (P∧R)→P
G2 = Q→P4
G3 = P1→Q
G4 = (P1∧P2)→Q
G5 = (P3∧R)→R
G6 = P4→P
G7 = P1
G8 = P3→P
G9 = P2
Exemplo de prova de (S∨P)
H1 = G7 = P1
H2 = G3 = P1→Q
H3 = Q {Resultado de MP em H1 e H2}
H4 = G2 = Q→P4
H5 = P4{Resultado de MP em H3 e H4}
H6 = G6 = P4→P
H7 = P {Resultado de MP em H5 e H6}
H8 = Ax2 = P→(S∨P)
H9 = (S∨P) {Resultado de MP em H7 e H8}
G1 = (P∧R)→P
G2 = Q→P4
G3 = P1→Q
G4 = (P1∧P2)→Q
G5 = (P3∧R)→R
G6 = P4→P
G7 = P1
G8 = P3→P
G9 = P2
Ax1 = (H ∨ H) → H
Ax2 = H → (G ∨ H)
Ax3 = (H → G) → ((E ∨ H) → (G ∨ E))
Notação
 A prova no sistema axiomático pode ser representada também da 
seguinte forma:
P1, (P1→Q) MP1
Q, (Q→P4) MP2
P4, (P4→P) MP3
P, P→(S∨P) MP4
(S∨P)
 MP1 – fórmulas do antecedente P1, (P1→Q) pertencentes a β
 MP2 – fórmulas do antecedente Q, (Q→P4), onde Q é o resultado de 
MP1 e (Q→P4) pertence a β
 MP3 
 MP4 – aplicação do axioma Ax2
Consequência lógica e teorema
 Consequencia lógica
 Definição: Dada uma fórmula H e um conjunto de hipóteses β, então 
H é uma consequencia lógica de β no sistema axiomático, se existe 
uma prova de H a partir de β
 Teorema
 Definição: Uma fórmula H é um teorema no sistema axiomático se 
existe uma prova de H que utiliza apenas axiomas. Neste caso o 
conjunto de hipóteses é vazio
 Um teorema é uma fórmula que representa um conhecimento 
derivável no sistema axiomático, a partir de seus axiomas. 
 É uma fórmula H derivável a partir de um conjunto vazio de 
hipóteses
Notação
 Conjunto de hipóteses β = {H1, H2, ..., Hn}
 Se H é consequência lógica de β então 
β├ H ou {H1, H2, ..., Hn} ├ H
 Se β é vazio então a notação empregada é├ H
Exemplo 1
(a) Sabendo-se que β├ (A→B), β├ (C∨A), mostre que β├ (B∨C) 
(b) Mostre que├ (p∨¬p) 
Demonstração:
(a) A partir da implicação queremos chegar na disjunção, logo axioma 3 
Ax3 = (H → G) → ((E ∨ H) → (G ∨ E))
Substituição de “G” por “B” e “E” por “C”
(H → B) → ((C ∨ H) → (B ∨ C))
Substituição de “H” por “A”
(A → B) → ((C ∨ A) → (B ∨ C))
Sabemos que (A → B) chegamos a ((C ∨ A) → (B ∨ C))
Mas, (C ∨ A) é outra hipótese, então (B ∨ C)
Exemplo 2
(b) Mostre que├ (p∨¬p) 
Demonstração:
(a) Queremos chegar na disjunção, logo axioma 3 Ax3 = (H → G) → ((E ∨ H) → 
(G ∨ E))
Substituição de “G” por “p” e “E” por “¬p”
(H → p) → ((¬p ∨ H) → (p ∨ ¬p))
Não tenho hipótese, qual o próximo passo?
Substituição de “H” por “(p ∨ p)”
((p ∨ p) → p) → ((¬p ∨ (p ∨ p)) → (p ∨ ¬p))
Agora o antecedente é o Ax1, portanto verdadeiro
Aplicando MP, o consequente é verdadeiro ((¬p ∨ (p ∨ p)) → (p ∨ ¬p))
Este antecedente pode ser escrito como p → (p ∨ p) que nada mais é do que 
Ax2 e portanto, verdadeiro.
Empregando novamente MP, (p ∨ ¬p) é teorema
Ax1 = (H ∨ H) → H
Ax2 = H → (G ∨ H)
Ax3 = (H → G) → ((E ∨ H) → (G ∨ E))
Ax1 = ¬(H ∨ H) ∨ H
Ax2 = ¬H ∨ (G ∨ H)
Ax3 = (¬(¬H ∨ G)) ∨ ((¬(E ∨ H)) ∨ (G ∨ E))
├ p→¬¬p
Mostre que├ p→¬¬p 
É possível escrever a implicação em termos de {∨,¬} , logo ¬p ∨ ¬¬p
Já foi demonstrado que ├ (p∨¬p)
Fazendo a substituição de ‘p’ por ‘¬p’ a prova é obtida
 
├ (¬p∨¬¬p)
Equivalência – axioma2
├ p→¬¬p 
 Correspondências
 H → G denota (¬H ∨ G)
 H → false denota ¬H
 (H↔G) denota (H → G) ∧ (G → H) 
 (H ∧ G) denota ¬(¬H ∨ ¬G)
Ax1 = (H ∨ H) → H
Ax2 = H → (G ∨ H)
Ax3 = (H → G) → ((E ∨ H) → (G ∨ 
E))
Ax1 = ¬(H ∨ H) ∨ H
Ax2 = ¬H ∨ (G ∨ H)
Ax3 = (¬(¬H ∨ G)) ∨ ((¬(E ∨ H)) ∨ (G ∨ E))
├ p→p
 Mostre que ├ p→p 
 Partindo de Ax3 (H → G) → ((E ∨ H) → (G ∨ E))
Fazendo as substituições G=¬p, E = p
(H → ¬p) → ((p ∨ H) → (¬p ∨ p))
Obtemos (¬p ∨ p) (Demonstrado no exemplo 2)
Substituimos H por ¬p
(¬p → ¬p) → ((p ∨ ¬p) → (¬p ∨ p))
(¬p → ¬p)?
Escrevendo (¬p → ¬p) em termos de {∨,¬} tem-se que 
¬¬p ∨ ¬p, ou seja p ∨ ¬p
Empregando MP, o consequente é verdadeiro
Empregando MP novamente,
consequente do consequente é verdadeiro.
Demonstrado ├ p→p
Comutatividade do conectivo ∨
β├ (A∨B) → (B∨A) 
Na prova anterior chegamos a ((p ∨ ¬p) → (¬p ∨ p))
Se em lugar dos símbolos tivermos as fórmulas, o resultado é 
similar
((A ∨ B) → (B ∨ A)) e os mesmos passos levam ao resultado 
desejado
Transitividade do conectivo →
 Se β├ (A1→ A2) e β├ (A2→ A3) então β├ (A1→ A3) 
 Hipóteses: β├ (A1→ A2) e β├ (A2→ A3) 
 Empregando axioma 3
Ax3 = (H → G) → ((E ∨ H) → (G ∨ E))
 Se G = ¬A1 e E = A3
Ax3 = (H → ¬A1) → ((A3 ∨ H) → (¬A1 ∨ A3))
 Sabemos que (A1→ A2) é equivalente a (¬A1 ∨ A2), que pela 
comutatividade pode ser escrito como (A2 ∨ ¬A1), que é o 
mesmo que (¬A2→ ¬A1)
 Fazendo H = ¬A2
Ax3 = (¬A2 → ¬A1) → ((A3 ∨ ¬A2) → (¬A1 ∨ A3))
Transitividade do conectivo →
 Fazendo H = ¬A2
Ax3 = (¬A2 → ¬A1) → ((A3 ∨ ¬A2) → (¬A1 ∨ A3))
 Se β├ (¬A2→ ¬A1), então por MP tem-se ((A3 ∨ ¬A2) → (¬A1 ∨ 
A3))
 Pela comutatividade, (A3 ∨ ¬A2) pode ser escrita como (¬A2 ∨ A3) 
 Pela equivalência dos axiomas, (¬A2 ∨ A3) pode ser escrito como 
 A2 → A3 
 Por hipótese temos β├ (A2→ A3), logo verdadeiro 
 Então por MP, ¬A1 ∨ A3 é verdadeiro.
 que é o mesmo que (A1→ A3) , como queríamos demonstrar
 β├ (A1→ A3) 
Completude do sistema axiomático
 O sistema axiomático deve ser correto e completo
 Teorema da correção
 Teorema da completude
Teorema da correção
 O sistema axiomático deve ser correto, ou seja, todo 
teorema deve ser uma tautologia
 os argumentos deduzidos a partir dos axiomas, utilizando 
as regras de inferência, devem ser válidos
 Teorema: Seja H uma fórmula da lógica proposicional, se ├ 
H então H é uma tautologia
Teorema da completude
 O sistema axiomático deve ser completo, ou seja, toda 
tautologia deve ser um teorema
 se o sistema é completo, então a tautologia é um teorema
 toda tautologia pode ser derivada no sistema axiomático
 Teorema: Seja H uma fórmula da lógica proposicional. Se H é 
uma tautologia então├ H 
Consistência
 Teoremas centrais da lógica
 Correção
 Completude
 Relacionam sintática e semântica
 Relacionamento: “ ├ H ” e “H é uma tautologia”
 H é um teorema se e somente se H é uma tautologia
 Sistema axiomático é correto e completo
 Consequência: consistência
 Teorema: um sistema axiomático é consistente, se e somente 
se, dada uma fórmula H, não se pode ter ├ H e ├ ¬H. Isto é, H 
e ¬H não podem ser teoremas ao mesmo tempo 
 O sistema axiomático é consistente
Lógica Proposicional
 Sistemas de dedução
 Sistema axiomático (Axiomatização)
 Sistema de dedução natural
 Tableaux
 Resolução
Sistema de dedução natural
 O sistema de dedução natural da lógica proposicional é 
definido pela composição dos três elementos:
 O alfabeto da Lógica Proposicional
 O conjunto de fórmulas da Lógica Proposicional
 Um conjunto de regras de dedução (ou regras de inferência)
Sistema de dedução natural
 Este sistema não contém axiomas
 O conhecimento é representado nas regras de inferência
 Neste sistema as regras de inferência representam a idéia 
intuitiva de dedução de conhecimento do ponto de vista sintático, 
como também o significado construtivo dos conectivos
Axiomatização x Dedução natural
 Método de inferência por axiomatização
 identificar quais axiomas devem ser utilizados, em que ordem e 
com qual substituição é totalmente não-intuitivo
 impraticável em termos de implementação, pois requer uma 
busca de grande complexidade computacional
 Método de inferência por dedução natural
 método que se aproxima mais da forma como as pessoas 
raciocinam
Princípios da dedução natural
 Inferências realizadas por regras de inferência em que 
hipóteses podem ser introduzidas na prova e que deverão ser 
posteriormente descartadas para a consolidação da prova
 Para cada conectivo lógico, duas regras de inferência devem 
ser providas, uma para a inserção do conectivo na prova e outra 
para a remoção do conectivo
Dedução natural
 No sistema de dedução natural:
 ¬H denota H → false
 P ∨ Q denota ¬(¬P ∧ ¬ Q)
 P ↔ Q denota (P → Q) ∧ (Q → P)
 No sistema de dedução natural os conectivos empregados 
são {¬, ∧, →}, que é um conjunto completo.
 Representação
conclusões
premissas
Regras de inferência
 No sistema de dedução natural há duas categorias regras
 regras de introdução
 (∧ I), (∨ I), (¬ I), (↔ I), (→I)
 Introduzem o conectivo correspondente
 regras de eliminação
 (∧ E), (∨ E), (¬ E), (↔ E), (→E)
 Eliminam o conectivo correspondente
Regras de inferência
 Dadas as fórmulas E, H e G, os esquemas de regras de 
inferência do sistema de dedução natural são definidos por:
Introdução e Eliminação da negação
 Introdução e Eliminação da conjunção
false
HHE ¬=¬ ,)(
H
false
H
I
¬
/
=¬ |)(
GH
GHI
∧
=∧
,)(
G
GH
H
GHE ∧∧=∧ ,)(
Se existe uma 
derivação false a 
partir de H então 
conclui-se ¬H
Regras de inferência
 Dadas as fórmulas E, H e G, os esquemas de regras de 
inferência do sistema de dedução natural são definidos por:
Introdução e Eliminação da disjunção
 Introdução e Eliminação da 
implicação (Modus Ponens)
GH
G
GH
HI
∨∨
=∨ )(
E
EEGH
DD
GH
E ∨
//
=∨
21
)(
GH
G
H
I
→
=→ |)(
G
GHHE →=→ ,)(
Se há duas derivações 
de E, uma a partir de 
H e outra a partir de G 
e, além disso, se a 
fórmula H ∨ G é 
também uma 
premissa, então 
conclui-se E
Regras de inferência
 Dadas as fórmulas E, H e G, os esquemas de regras de inferência 
do sistema de dedução natural são definidos por:
 Introdução e Eliminação da equivalência
 false e RAA (redução ao absurdo)
GH
HG
GHI
↔
=↔
||
)(
H
GHG
G
GHHE ↔↔=↔ ,,)(
H
falsefalse =)(
H
false
H
RAA |)(
/¬
=
É possível 
concluir 
qualquer 
fórmula H a 
partir de false
Dedução natural
 Representação:
 Modus Ponens = (→E)
 A fórmula G é concluída a partir das premissas H e H → G
conclusões
premissas
G
GHHE →=→ ,)(
Consequência lógica
 Estrutura para representação e dedução do conhecimento
 Conhecimento dado a priori = regras de inferência + 
hipóteses
 Consequências lógicas = conjunto de fórmulas que 
representam os argumentos obtidos a partir da aplicação das 
regras de inferência sobre as hipóteses
 Derivação no sistema de dedução natural
 Toda fórmula H da Lógica Proposicional é uma derivação no 
sistema de dedução natural
Derivação
 Sejam D1, D2 e D3 derivações no sistema de dedução natural. As 
estruturas a seguir também são derivações neste sistema:
 (¬)
 (∧)
 (∨)
H
false
D
¬
1
false
HH
DD
¬
21
G
GH
D
H
GH
D
GH
GH
DD
∧∧
∧
1121
E
EEGH
DDD
GH
GH
G
D
GH
H
D
∨
//
∨∨
213
21
Derivação
 (→)
 (↔)
 false e RAA
GH
G
D
H
→
/
1
G
GHH
DD
→
21
H
GHG
DD
G
GHH
DD
GH
HG
DD
GH
↔↔
↔
2121
21
H
false
D1
H
false
D
H
1
/
Derivação
 Exemplo: derivação de (P ∧ Q) →(Q ∧ P)
P ∧ Q (∧E) P ∧ Q (∧E)
Q P (∧ I)
 Q Q ∧∧ P ( P (→→ I) I) 
 (P ∧ Q) →(Q ∧ P)
 Aplicação das regras de inferência como no sistema axiomático
árvore
 Numa prova do sistema axiomático tem-se uma sequência de 
fórmulas. A estrutura de derivação no sistema de dedução natural 
é uma árvore
 árvore de derivação 
de (P ∧ Q) →(Q ∧ P)
Definições no sistema de dedução natural
 Prova: sejam H uma fórmula e β um conjunto de fórmulas 
denominadas por hipóteses. Uma prova de H a partir de β, é uma 
derivação onde se tem:
 As regras da derivação
são aplicadas tendo como premissas iniciais, 
fórmulas de β ou fórmulas que são eliminadas pela aplicação de regras 
de derivação
 A última fórmula da derivação é H
 Consequência lógica: dada uma fórmula H e um conjunto de 
hipóteses β, então H é uma consequência lógica de β, se existe 
uma prova de H a partir de β
 Teorema: uma fórmula H é um teorema se existe uma prova de H 
que não utiliza hipóteses
Sistema de dedução natural
 Sistema correto e completo
 Todo teorema é uma tautologia e toda tautologia é um teorema
 Um sistema pode ser completo mesmo na ausência de axiomas, 
apresentando apenas regras de inferência 
Lógica Proposicional
 Sistemas de dedução
 Sistema axiomático (Axiomatização)
 Sistema de dedução natural
 Tableaux semânticos
 Resolução
Lógica proposicional
 Três passos básicos da Lógica Proposicional
 especificação da linguagem
 estudo de métodos de verificação da validade de argumentos
 noções de prova ou demonstrações
 Sistemas axiomático e dedução natural não são adequados para 
implementação em computadores
Tableaux semânticos
 Sequência de fórmulas construída de acordo com regras e 
apresentada na forma de uma árvore
 Elementos básicos
 alfabeto da Lógica Proposicional
 conjunto de fórmulas da Lógica Proposicional
 conjunto de regras de dedução
 Mesma estrutura do sistema de dedução natural
 As regras de dedução do tableau semântico definem o 
mecanismo de inferência
Regras
Prova
 Emprego do método da negação ou absurdo (Sistema de 
refutação), onde para provar A é considerada inicialmente sua 
negação ¬A
 A aplicação das regras de dedução decompõe a fórmula ¬A 
em subfórmulas
Exemplo de construção de um tableau semântico
Aplicação das regras
 A aplicação das regras é feita considerando qualquer uma das 
fórmulas presentes na árvore
 Uma boa heurística na construção de um tableau semântico é 
aplicar inicialmente as regras que não bifurcam a árvore, ou seja, 
postergar a bifurcação
 Heurística: aplique preferencialmente as regras:
 R1, R5, R7 e R8, que não bifurcam o tableau
Definição
 Um tableau semântico na Lógica Proposicional, é construído como se 
segue. Seja {A1, ..., An} um conjunto de fórmulas.
 A árvore a seguir, com apenas um ramo é um tableau associado a 
{A1, ..., An}.
 .1 A1
 .2 A2
.
.
.
 .n An
 Seja Tree um tableau semântico associado a {A1, ..., An}. Se Tree* é a 
árvore resultante da aplicação de uma das regras R1, ..., R9 à árvore 
Tree, então Tree* é também um tableau associado a {A1, ..., An} 
Exemplo de construção do tableau
{(A→B), ¬(A∨B), ¬(C→A)}
Tree1 (árvore de um ramo)
.1 A→B
.2 ¬(A∨B)
.3 ¬(C→A)
Exemplo de construção do tableau
{(A→B), ¬(A∨B), ¬(C→A)}
Tree2 (R7 aplicada a Tree1):
.1 A→B
.2 ¬(A ∨ B)
.3 ¬(C→A)
.4 ¬A R7, .2
.5 ¬B R7, .2
Exemplo de construção do tableau
 {(A→B), ¬(A∨B), ¬(C→A)}
 Tree3 (R3 aplicada a Tree2):
 .1 A→B
 .2 ¬(A∨B)
 .3 ¬(C→A)
 .4 ¬A R7, .2
 .5 ¬B R7, .2
 .6 ¬A B R3, .1
Exemplo de construção do tableau
 {(A→B), ¬(A∨B), ¬(C→A)}
 Tree4 (R8 aplicada a Tree3):
 .1 A→B
 .2 ¬(A∨B)
 .3 ¬(C→A)
 .4 ¬A R7, .2
 .5 ¬B R7, .2
 .6 ¬A B R3, .1
 .7 C C R8, .3
 .8 ¬A ¬A R8, .3
Análise:
 O ramo da esquerda não 
contém fórmula com sua 
negação
 O ramo da direita contém B 
e ¬B
Exemplo de construção do tableau
 Ramo fechado e aberto
 Um ramo em um tableau é fechado se ele contém uma 
fórmula A e sua negação ¬A ou contém o símbolo de 
verdade false. 
 Um ramo é aberto quando não é fechado
 Tableau fechado
 Um tableau é fechado quando todos os seus ramos são 
fechados. Caso contrário ele é aberto
Prova e teorema
Prova: Seja H uma fórmula. Uma prova de H utilizando tableaux 
semânticos é um tableau fechado associado a ¬H. Neste caso, 
H é um teorema do sistema de tableaux semânticos
Exemplo:
Como provar H=¬((P→Q)∧ ¬(P↔Q) ∧(¬¬P))?
Gerar um tableau fechado para ¬H:
¬(¬((P→Q) ∧ ¬(P↔Q) ∧(¬¬P)))
Exemplo de prova
.1 ¬(¬((P→Q) ∧¬(P↔Q) ∧(¬¬P))) ¬H
.2 (P→Q) ∧¬ (P↔Q) ∧(¬¬P) R5, .1
.3 P→Q R1, 2.
.4 ¬(P↔Q) R1, 2.
.5 ¬¬P R1, 2.
.6 P R5, 5.
.7. ¬P Q R3, 3.
 fechado
.8 P ∧¬Q ¬P ∧Q R9, 4.
.9 P ¬P R1, 8.
.10 ¬Q Q R1, 8.
 fechado fechado
Tableau semântico
 Método completo e correto
 Consequência lógica: Dada uma fórmula H e um conjunto de 
hipóteses β = {A1, ..., An}, então H é uma consequencia lógica de 
β, nos tableaux semânticos, se existe uma prova de (A1∧... ∧An) → 
H utilizando tableaux semânticos
 A notação empregada é a mesma dos outros sistemas de 
dedução β├ H
Exercício
Guga é determinado
Guga é inteligente
Se Guga é determinado e atleta, ele não é um perdedor
Guga é um atleta se é amante do tênis
Guga é amante do tênis se é inteligente
A afirmação “Guga não é um perdedor” é conseqüência lógica dos 
argumentos acima??
Uma prova por tableaux semânticos
Correspondências
P = Guga é determinado
Q = Guga é inteligente
R = Guga é atleta
P1 = Guga é um perdedor
Q1 = Guga é amante do tênis
H = (P ∧ Q ∧ ((P ∧ R) → ¬P1) ∧ (Q1→R) ∧(Q→Q1)) → ¬P1 
Guga é determinado
Guga é inteligente
Se Guga é determinado e atleta, ele não é um perdedor
Guga é um atleta se é amante do tênis
Guga é amante do tênis se é inteligente
Guga não é um 
perdedor?
Exercício 1
 Deve-se provar se H é ou não uma tautologia
 Se a prova de ¬H é um absurdo, ou seja, produz um tableau 
fechado, então a consequência lógica ocorre
Exercício 2
 Sejam os argumentos:
Se Guga joga uma partida de tênis, a torcida comparece se o 
ingresso é barato
Se Guga joga uma partida de tênis, o ingresso é barato
“Se Guga joga uma partida de tênis, a torcida compare” é uma 
consequência lógica dos argumentos acima?
 Considere as correspondências
P = Guga joga uma partida de tênis
Q = A torcida comparece
R = O ingresso é barato
Tableaux abertos
 A prova da tautologia pelo método tableau semântico considera 
tableau fechado na prova da negação de H
 E se a prova for feita a partir de H e tableaux abertos forem 
encontrados, o que se pode concluir?
 Nada!!!
Conclusões
 Dada uma fórmula da lógica proposicional H
 H é tautologia  Tableau associado a ¬H é fechado
 H é contraditória ¬H é tautologia  Tableau associado a 
H é fechado
Exemplos
Apresente os tableaux semânticos para H e G
H = (A∨¬A) ∨ (A→B)
G = (B∧¬B) ∨ (A→A)
Lógica Proposicional
 Sistemas de dedução
 Sistema axiomático (Axiomatização)
 Sistema de dedução natural
 Tableaux semânticos
 Resolução
Resolução
 Método de prova desenvolvido nos anos 60
 Base da linguagem de programação Prolog
 Pode ser considerada como dual dos tableaux semânticos
 Nos tableaux semânticos é empregada a heurística:
 Aplique preferencialmente as regras R1, R5, R7 e R8, que não 
bifurcam o tableau
 Isso significa que o tableau é construído de forma eficiente para 
fórmulas que são conjunções de disjunções de literais
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(E1,E2) = {¬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
Expansão por resolução
 Exemplo: {{¬ P,Q}, {P,R},{P, ¬Q},{¬Q, ¬R}}
.1 {¬ P,Q}
.2 {P, R}
.3 {P,¬Q}
.4 {¬Q,¬R} 
.5 {Q, R} Res(.1,.2)
.6 {P, R} Res(.3,.5)
.7 {Q, R} Res(.1,.6)
.8 {R, ¬R} Res(.4,.7)
 A expansão por resolução resultante não contém a cláusula vazia, 
propriedade importante, análogo à obtenção de um tableau fechado.
 Uma expansão por resolução é fechada se ela contém a cláusula vazia
Consequência lógica na resolução
 Forma clausal
 Dada uma fórmula H, a forma clausal associada a H é uma 
fórmula Hc tal que Hc é uma conjunção de cláusulas e Hc é 
equivalente a H
 Prova por resolução
 Seja H uma fórmula e ¬Hc a forma clausal associada a ¬H. 
Uma prova de H por resolução é uma expansão por resolução 
fechada sobre ¬Hc. Neste caso, H é um teorema do sistema 
de resolução.
Exemplo de prova por resolução
H = ((P1∨P2∨P3)∧(P1→P4)∧(P2→P4)∧(P3→P4)) → P4
Passo 1: Determinar forma clausal ¬Hc associada a ¬H
Equivalências
¬H = ¬(((P1∨P2∨P3)∧(P1→P4)∧(P2→P4)∧(P3→P4)) → P4)
¬ (¬((P1∨P2∨P3) ∧ (¬P1∨P4) ∧ (¬P2∨P4) ∧ (¬P3∨P4)) ∨ P4)
(P1∨P2∨P3)∧(¬P1 ∨ P4)∧(¬P2 ∨ P4)∧(¬P3 ∨ P4) ∧ ¬P4)= ¬Hc
¬Hc é uma conjunção de cláusulas e é representada na notação de 
conjunto como
¬Hc={{P1, P2, P3}, {¬P1,P4}, {¬P2,P4}, {¬P3,P4}, {¬P4}}
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
Exemplo de prova por resolução
 G = ((P1∨P2)∧(P1→P4)∧(P2→P4)∧(P3→P4)) → P3
 Passo 1: Determinar forma clausal ¬Gc associada a ¬G
 Equivalências
 ¬G = ¬(((P1∨P2)∧(P1→P4)∧(P2→P4)∧(P3→P4)) → P3)
 ¬ (¬((P1∨P2) ∧ (¬P1∨P4) ∧ (¬P2∨P4) ∧ (¬P3∨P4)) ∨ P3)
 (P1∨P2)∧(¬P1 ∨ P4)∧(¬P2 ∨ P4)∧(¬P3 ∨ P4) ∧ ¬P3)= ¬Gc
 ¬Hc é uma conjunção de cláusulas e é representada na notação de 
conjunto como
 ¬Gc={{P1, P2}, {¬P1,P4}, {¬P2,P4}, {¬P3,P4}, {¬P3}}
Exemplo de prova por resolução
¬Gc={{P1, P2}, {¬P1,P4}, {¬P2,P4}, {¬P3,P4}, {¬P3}}
.1 {P1, P2}
.2 {¬P1,P4}
.3 {¬P2,P4}
.4 {¬P3,P4} 
.5 {¬P3}
.6 {P2, P4} Res(.1,.2)
.7 {P4} Res(.3,.6)
. Expansão não é fechada, logo não se tem prova de G
Exercício
Guga é determinado
Guga é inteligente
Se Guga é determinado e atleta, ele não é um perdedor
Guga é um atleta se é amante do tênis
Guga é amante do tênis se é inteligente
A afirmação “Guga não é um perdedor” é conseqüência lógica dos 
argumentos acima??
Uma prova por resolução
Correspondências
P = Guga é determinado
Q = Guga é inteligente
R = Guga é atleta
P1 = Guga é um perdedor
Q1 = Guga é amante do tênis
H = (P∧Q ∧((P ∧ R)→¬P1) ∧(Q1→R) ∧(Q→Q1)) →¬P1 
Guga é determinado
Guga é inteligente
Se Guga é determinado e atleta, ele não é um perdedor
Guga é um atleta se é amante do tênis
Guga é amante do tênis se é inteligente
Guga não é um 
perdedor?
	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
	Slide 31
	Slide 32
	Slide 33
	Slide 34
	Slide 35
	Slide 36
	Slide 37
	Slide 38
	Slide 39
	Slide 40
	Slide 41
	Slide 42
	Slide 43
	Slide 44
	Slide 45
	Slide 46
	Slide 47
	Slide 48
	Slide 49
	Slide 50
	Slide 51
	Slide 52
	Slide 53
	Slide 54
	Slide 55
	Slide 56
	Slide 57
	Slide 58
	Slide 59
	Slide 60
	Slide 61
	Slide 62
	Slide 63
	Slide 64
	Slide 65
	Slide 66
	Slide 67
	Slide 68
	Slide 69
	Slide 70
	Slide 71
	Slide 72
	Slide 73
	Slide 74
	Slide 75
	Slide 76
	Slide 77
	Slide 78
	Slide 79
	Slide 80
	Slide 81
	Slide 82
	Slide 83