Baixe o app para aproveitar ainda mais
Prévia do material em texto
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çãosã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
Compartilhar