Resoluo Proposicional Amanda Micoski Lins, Cibele Alves da
Silva Reis, Henrique Petroski Such
Slide 2
Resoluo Proposicional O que Lgica? Lgica a cincia que estuda
princpios e mtodos de inferncia, tendo como objetivo principal de
determinar em que condies certas coisas se seguem(so conseqncia),
ou no de outras. 2
Slide 3
Resoluo Proposicional Lgica Proposicional A lgica estudada em
resoluo proposicional a lgica de proposies, que composta de
proposies, as quais devem possuir um valor verdade. Alm de ser
utilizada para a especificao ou declarao de um programa, pode tambm
ser uma linguagem de programao, idia que foi considerada
revolucionria ao ser sugerida por Kowalski em 1972. 3
Slide 4
Resoluo Proposicional O mtodo da resoluo proposicional uma
regra de inferncia que leva a tcnica de demonstrao por refutao para
frmulas ou teorias proposicionais. Ele um dos mais conhecidos no
ramo de provadores de teorema e tem a habilidade de detectar
satisfatibilidade. As frmulas devem estar no formato clausal.
4
Slide 5
Resoluo Proposicional A resoluo proposicional consiste na
simplificao de clusulas at a obteno de uma clusula menor, ou de um
resultado vazio (inconsistncia lgica). Chega-se no resultado por
inferncia, ou seja, pela passagem, atravs de regras vlidas, do
antecedente ao conseqente de um argumento. Um exemplo de linguagem
que se fundamenta a resoluo a linguagem Prolog. 5
Slide 6
Resoluo Proposicional Exemplos (b b d) pode ser escrito como
apenas (b d), uma vez que o literal b apareceu mais de uma vez na
frmula, podendo ento ser contrado. A inferncia de (p b) e (p c)
resulta em (b c). Sendo as frmulas (p b) e (p c) chamadas de
resolventes, e (b c) chamada de resoluta. 6
Slide 7
Resoluo Proposicional Clusulas Primeiro para entendermos a
resoluo devemos primeiro nos direcionar a pequenos conceitos, como
clusulas. Clusula na lgica proposicional uma disjuno de literais.
Exemplos C = {P, L}, C = {P, Q, R, S, T, V}, C =, C= {P}. 7
Slide 8
Resoluo Proposicional Clusulas Clusula Vazia Uma clusula que
possui tanto o antecedente quanto o conseqente vazios, e deve ser
interpretada como uma contradio. Por possuir somente um literal em
sua clusula. Exemplo C = 8
Slide 9
Resoluo Proposicional Clusulas Clusulas de Horn Tanto as
Clusulas C, como C do exemplo anterior so chamadas de Clusulas de
Horn, por possurem no mximo um literal positivo, porm para C tambm
atribudo o nome de Clusula Objetivo, por no possuir literais
positivos, enquanto C chamada muitas vezes de Clusula de Programa,
por possuir somente um literal positivo. 9
Slide 10
Resoluo Proposicional Clusulas As clusulas de Horn so assim
denominadas em homenagem ao matemtico Alfred Horn, que primeiro
lhes estudou as propriedades, em 1951. Uma de suas mais importantes
caractersticas que qualquer problema solvel capaz de ser
representado por meio delas, pode ser representado de tal forma que
apenas uma das clusulas seja uma clusula objetivo, enquanto que
todas as restantes sero clusulas de programa. 10
Slide 11
Resoluo Proposicional Clusulas Para um grande nmero de aplicaes
da lgica, suficiente empregar o contexto restrito das clusulas de
Horn. Na figura a seguir, posicionamos as clusulas de Horn em sua
relao com a lgica matemtica, o clculo de predicados de primeira
ordem e a forma clausal. 11
Slide 12
Resoluo Proposicional Regras para o mtodo da resoluo No pode
haver smbolos existenciais ou quantificadores. Os smbolos de
implicao devem ser substitudos pelos de conjuno e disjuno. Os
sinais de negao devem estar ao lado de seus respectivos tomos. A
frmula resultante da resoluo, quando for diferente de zero, deve
ser conseqncia lgica da frmula que a gerou. 12
Slide 13
Resoluo Proposicional Conseqncia Lgica Outro conceito muito
importante o conseqncia lgica Uma frmula conseqncia lgica da outra
quando toda valorao que satisfizer a primeira tambm satisfizer a
segunda. 13
Slide 14
Resoluo Proposicional Exemplos: Dada a inferncia: P T S, T S
|-res P S Teremos: ~(P S) = {P,S} resultando, assim, no conjunto {
P T S, T S, P,S} da resoluo. P T SP T ST S S SS 14
Slide 15
Resoluo Proposicional Desafios Computacionais Os maiores
desafios so a escolha dos resolventes a cada passo e a diminuio do
espao de busca, os quais, quando no resolvidos, podem trazer
prejuzos na execuo do mtodo, utilizando um grande tempo de
processamento. 15
Slide 16
Resoluo Proposicional Desafios Computacionais Uma das
estratgias para resolver esse problema a utilizao da resoluo
unitria o mximo de vezes possvel, tcnica tambm chamada de propagao
unitria ou, em ingls, boolean constraint propagation (BCP). 16
Slide 17
Desafios Computacionais Boolean Constraint Propagation Ela
consiste em usar clusulas unitrias como resolventes, simplificando
o processo e gerando frmulas resolutas mais simples. Alm de
auxiliar na escolhas dos resolventes, a resoluo unitria sempre
elimina um resolvente a favor de um resoluto, o que tambm ajuda a
resolver o problema do espao de busca. 17
Slide 18
Resoluo Proposicional Desafios Computacionais Um exemplo de
resoluo unitria: SS R RR 18
Slide 19
Resoluo Proposicional Desafios Computacionais Infelizmente, nem
sempre possvel usar a propagao unitria. Outra estratgia utilizada
para a escolha de resolventes a resoluo linear. Ela uma forma mais
lgica de aplicar o mtodo da resoluo, j que cada formula resoluta
torna- se a frmula resolvente no prximo passo. 19
Slide 20
Resoluo Proposicional Desafios Computacionais uma maneira mais
simples de construir a rvore de prova, transformando-a numa linha
em que os membros direita so frmulas simples. O exemplo anterior
foi desenvolvido atravs da resoluo linear. 20
Slide 21
Resoluo Proposicional Referncias Bibliogrficas Freitas, Fred;
Notas da disciplina Programao em Lgica e Negao por Falha.
Universidade Federal de Pernambuco, 2006. Disponvel em:, acessado
dia 21/03/2009 Moreira, Nelma. Notas de aula da disciplina
Inteligncia Artificial com base em Programao Lgica. Faculdade de
Cincias da Universidade do Porto, 2008. Portugal. Disponvel em:,
acessado dia 21/03/2009. Pereira, Silvio do Lago; Lgica
Proposicional. Material Didtico. Faculdade de Tecnologia de So
Paulo, 2008. Disponvel em:, acessado dia 21/03/2009. 21
Slide 22
Resoluo Proposicional Referncias Bibliogrficas Perez, Anderson
L. F.; Notas de aula da disciplina Lgica Aplicada Computao.
Universidade Federal do Vale do So Francisco, 2008. Disponvel em:,
acessado dia
21/03/2009.http://www.univasf.edu.br/~anderson.perez/ensino/logica/aulas/Pr
ogramacao_logica_2.pdf Ryncn, Mauricio A.; Fundamentos da Programao
Lgica e Funcional. Notas de aula para a disciplina de Lgica para
Computao. Universidade Braslia, 2004. Disponvel em:, acessado dia
21/03/2009. Silva, Flvio S. C. da; Finger, Marcelo; Melo, Ana C.
V.; Lgica Para Computao. So Paulo: Thomson Learning, 2006. p 88
-92. 22
Slide 23
Resoluo Proposicional Referncias Bibliogrficas Souza, Joo Nunes
de. Lgica para Cincia da Computao. Rio de Janeiro: Campus, 2002. p
3 24. Almeida, Carlos B.; Notas de aula da disciplina Lgica
Computacional. Universidade do Minho, 2008. Disponvel em:, acessado
dia 21/03/2009. Universo de Herbrand. Wikipedia, pgina criada em
2006. Disponvel em:, acessado dia 21/03/2009. 23
