Resolução exercício dos cubos - DAINFtacla/logica/slides/LP-02-Sistemas... · Dedução Natural: conjunto de regras para lógica proposicional (inclusão e eliminação para cada

Sistemas Dedutivos

UTFPR/Curitiba Prof. Cesar A. Tacla http://www.pessoal.utfpr.edu.br/tacla

15/06/2015 22:47

http://www.pessoal.utfpr.edu.br/tacla

Fundamentos

CONSEQUÊNCIA SEMÂNTICA c é uma consequência semântica das premissas, se toda interpretação que satisfaz todas as premissas satisfaz também a conclusão c.

p1, p2, …, pn ⊨ c

pi são premissas, c é a conclusão do argumento

Fundamentos

Sobre o símbolo de consequência semântica

No slide anterior, foi usado para falar sobre o que é um argumento válido em lógica clássica juntamente com símbolos não-lógicos (p1, p2, c) e linguagem natural. Observar que não foi feita nenhuma referência ao procedimento para se demonstrar que o argumento é válido.

Este símbolo é utilizado para se falar sobre argumentos válidos em lógicas, então diz-se que é um símbolo metalógico.

⊨

Fundamentos

SISTEMAS DEDUTIVOS ou SISTEMAS DE INFERÊNCIA ou MÉTODOS DE PROVA Procedimento para cálculo de consequência lógica pela aplicação de regras de inferência

Idéia fundamental: raciocínio é manipulação de símbolos

i.e. dada uma teoria Γ={p1, …, pn} um sistema dedutivo permite deduzir que uma fórmula A é consequência lógica de Γ por uma sequência de aplicações de regras de inferência.

Fundamentos

Γ ⊢ A

Se há uma sequência de regras de inferência que permite concluir A de uma teoria Γ então escreve-se

antecedente TEORIA

consequente ou conclusão TEOREMA

Sequente

B1, …, Bn ⊢ A1, …, An

Formulação genérica de sequente

conjunção disjunção

(diz-se A é dedutível de Γ)

Fundamentos

MÉTODO CORRETO DE PROVA (CORRETUDE) diz-se que um método de prova é correto se somente produz

conclusões que são consequências semânticas:

p1, p2, …, pn ⊢ c sse p1, p2, …, pn ⊨ c

Fundamentos

MÉTODO COMPLETO DE PROVA (COMPLETUDE) diz-se que um método de prova é completo se consegue encontrar

uma sequência de aplicações de regras de inferência para toda conclusão válida

p1, p2, …, pn ⊨ c sse p1, p2, …, pn ⊢ c

Fundamentos

*Fonte: Guilherme Bittencourt, http://www.das.ufsc.br/~gb/pg-md/tra-mad-prova.pdf

Métodos de prova corretos e completos (entre outros):

Axiomático (ou de Frege ou de Hilbert): método que pelo uso de um conjunto de axiomas e de regras de inferência (Modus Ponens - MP, Modus Tolens - MT) alcança o teorema (a fórmula a ser demonstrada). Dedução Natural: conjunto de regras para lógica proposicional (inclusão e eliminação para cada conectivo lógico) Método de Tableaux. Por refutação, porém, analítico (em oposição aos de resolução). Lida diretamente com as fórmulas sem recorrer a formas normais. * Resolução: método por refutação (Robinson, 1965) -utilizado pelo PROLOG. Usa as formas normais.

http://www.das.ufsc.br/~gb/pg-md/tra-mad-prova.pdf







AXIOMÁTICO

AXIOMATIZAÇÃO TEM 2 ELEMENTOS

AXIOMAS: fórmulas com status de verdade básica (da onde vêm os axiomas? De verdades experimentais? São simples convenções?)

REGRAS DE INFERÊNCIA: que permitem deduzir novas fórmulas a partir de outras já deduzidas.

Axiomatização

Axiomatização

Hilbert busca uma fundamentação para a geometria Euclidiana, i.e. axiomas completos (permitem a dedução de todas as proposições sobre objetos que denominou de pontos, retas e planos) que sejam o mais simples possível (conjunto mínimo de axiomas). Hilbert pretendia demonstrar que os axiomas escolhidos não são contraditórios (corretude) – isto é, que não permitem demonstrar um teorema e a sua negação.

Sistemas axiomáticos datam principalmente do fim do século XIX (Hilbert – 1889 – Fundamentos da Geometria) e início do XX (C.I. Lewis – Lógicas de 1ª. ordem)

Fonte: Gênios da Ciência: Matemáticos, Luiz Carlos P. Marin (ed)., 2ª ed., SP, Duetto Editorial, 2012

Ex. de teorema: o centro da circunferência circunscrita a um triângulo é o ponto de intersecção das mediatrizes desse triângulo.

Axiomatização: o que são axiomas? Ernst Zermelo em 1908 fundou sua teoria de conjuntos sobre os axiomas abaixo

De Extensionalidade: dois conjuntos são idênticos sse possuem os mesmos elementos Do Conjunto vazio: existe um conjunto que não contém nenhum elemento denominado de conjunto vazio e representado por Do par ... Da união ... De separação ... Do conjunto infinito ... Das partes ... Da substituição ... De fundação (acrescentado por J. Von Neumann em 1929): nenhum conjunto é um dos seus próprios elementos (nenhum conjunto contém a si próprio para evitar paradoxos autorreferenciais)

Axiomatização: ideia básica

Na construção axiomática de uma lógica, o criador da lógica procura selecionar o mínimo de axiomas e de regras de inferência que reflitam suas ideias sobre que princípios de raciocínio devam ser incluídos na lógica. (Girle, R. Possible Worlds, 2003, pg. 31)

Axiomatização: ideia básica

Exemplo: vamos supor que transitividade é um princípio importante para implicação lógica. Portanto, um argumento que apresenta a forma (estrutura) abaixo é válido na lógica do criador da lógica:

P → q q → r Logo, p → r

P → q q → r Logo, p → r

Portanto, o tal criador coloca um axioma na lógica que reflete este princípio:

⊢ (p → q) (q → r) (p → r)

Instanciação de uma fórmula

Exemplo: dado o axioma A = p → (q → p)

a fórmula (r s) → ((t v) → (r s))

é uma instância do axioma A pela substituição dos átomos por fórmulas

i) p por (r s) A[p:= (r s)]

ii) q por (t v) A[q:= (t v)]

Axiomatização

Alguns axiomas da lógica proposicional clássica

(→1) p →(q → p)

(→2) (p →(q → r))→((p → q)→(p→r))

(1) p →(q →(p q))

(2) (p q) → p

(3) (p q) → q

(1) p → (p q)

(2) q → (p q)

(3) (p → r) → ((q → r) → ((p q) → r))

(1) (p → q) → ((p → q) → p)

(2) p → p

Axiomatização Regra de inferência

Modus Ponens

A → B, A

B

Axiomatização: dedução

Então, utilizamos os axiomas e as regras de inferência para fazer deduções. Um Sistema Dedutivo permite deduzir as consequências semânticas de uma teoria.

Logo, uma fórmula A é dedutível de uma teoria Γ: se há uma sequência de fórmulas A1, ..., An que produzem A, tal que, cada fórmula Ai da dedução: 1. É uma fórmula Ai de Γ ou 2. É uma instância de um axioma do sistema lógico ou 3. É obtida de fórmulas anteriores por Modus Ponens (regra de inferência)

Axiomatização: teorema

Um teorema A é uma fórmula, tal que existe uma dedução A1, ..., An que produz A.

Representa-se um teorema por:

⊢ A ⊢ A AX OU

Identifica o método de inferência

Axiomatização: teorema da dedução

A é uma fórmula da teoria e B a fórmula a ser demonstrada

Γ, A⊨B sse Γ⊨ A→B

OU

Γ⊨ A→B sse Γ, A⊨B

No contexto do sistema dedutivo de axiomatização, o teorema fica:

Γ ⊢ A→ B sse Γ, A ⊢ B AX AX

Axiomatização: exemplo de dedução

Exemplo + exercício

Axiomatização na computação

Em termos computacionais, o método da axiomatização é de pouca utilidade, pois é difícil construir um algoritmo que: • Identifique qual axioma utilizar; • Defina a ordem de utilização dos axiomas; • faça as substituições mais adequadas – que conduzam à prova do

teorema/fórmula (substituir átomos por fórmulas)

DEDUÇÃO NATURAL

Sistemas dedutivos: referência

HUTH M. e RYAN M.. Lógica em Ciência da Computação. LTC Livros Técnicos e Científicos Editora, 2008.

Dedução Natural

Criada por Gentzen (1969) e refinada por Prawitz (1965).

Gentzen notou que o pequeno número de axiomas do Sistema de Axiomatização e de regras de inferência (só uma de fato, a Modus Ponens) dificulta o uso deste sistema de prova na prática.

Então, Gentzen propôs um método que se aproximasse mais da maneira como as pessoas raciocinam – daí o nome, dedução natural – permite introduzir/descartar hipóteses e há regras de inferência de introdução/eliminação para cada conectivo lógico.

Dedução Natural

É um método formal de inferência baseado nos princípios: 1) Inferências são realizadas por regras de inferências

em que hipóteses introduzidas na prova devem ser descartadas para a consolidação da prova;

2) Para cada conectivo lógico, há duas regras de inferência: a) uma para inserção do conectivo e b) outra para a remoção do conectivo da prova

Dedução Natural Regras de eliminação dos conectivos

(E)

A B A

B

(I)

A inserção da hipótese

…

B__

A B

(I)

(I)

A B

A B

(E)

A B (e1)

A

A B (e2)

B

(I)

A__

A B

B__

A B

(E)

A B

C

(I2)

(I1)

( I)

A__

A

( E)

A

A

Regras de introdução dos conectivos

A ... C

B ... C

Dedução Natural

Exemplos sem introdução de hipóteses

+

Exercícios

Dedução Natural

MODUS TOLLENS

A B B

A

Não é uma regra primitiva da D.N., mas pode ser derivada de outras regras!

Dedução Natural

Ao fazer introduzir uma implicação lógica, siga as regras: 1. Para concluir A → B, a “caixa” deve iniciar com a hipótese A e terminar com a dedução B; 2. As fórmulas dentro da “caixa” podem ser usadas apenas dentro da caixa, somente dentro do escopo; 3. Qualquer fórmula concluída anteriormente à abertura da caixa pode ser usada dentro da caixa, desde que não pertença a alguma caixa que já foi fechada. 4. A conclusão de A → B é independente da interpretação da hipótese. Por isso, a conclusão é escrita fora da caixa

“caixa”: segundo a notação de Huth e Ryan

Introdução de implicação (I)i

TABLEAUX ANALÍTICOS

Tableaux Analíticos

É um método de prova baseado em refutação. É correto, completo, decidível em LP* e não-determinístico.

*Tableaux-analíticos não são decidíveis para LPO (lógica de primeira ordem)


para provar Γ ⊢ A mostra-se que Γ U {¬A} ⊢ ⊥ i.e. que Γ U {¬A} é insatisfazível.

PROVA POR REFUTAÇÃO

exemplos com tabelas-verdade para entender o conceito


Γ = {p → q, p} // p = é criança, q = estuda no ensino fundamental

A = q Provar que Γ ⊢ A vem a ser

PROVA POR REFUTAÇÃO: EXEMPLO 1

PROVA POR REFUTAÇÃO Provar que Γ U {¬A} ⊢ ⊥ (p → q p q) é insatisfazível

FOI PROVADO FOI PROVADO

PROVA PELA IMPLICAÇÃO (p → q) p → q) é válida


Γ = {p}, A = q

PROVA POR REFUTAÇÃO: EXEMPLO 2

PROVA POR REFUTAÇÃO Provar que Γ U {¬A} ⊢ ⊥ vem a ser provar que (p q) é INSATISFAZÍVEL

PROVA PELA IMPLICAÇÃO provar que (p → q) é VÁLIDA

NÃO FOI PROVADO NÃO FOI PROVADO


É um procedimento de decisão – portanto decidível: capaz de demonstrar conclusões que são consequências lógicas de uma teoria e também aquelas que não são (assim como as tabelas-verdade são capazes).

Dedução natural e axiomatização são completos (capazes de demonstrar todas as consequências lógicas de uma teoria), porém, não são decidíveis. *Tableaux analíticos são decídiveis para LÓGICA PROPOSICIONAL (porém, são decidíveis para Lógica de Primeira Ordem - LPO)

DECIDÍVEL


Não-determinístico: o algoritmo possui (pelo menos) dois pontos onde deve haver uma escolha guiada por uma estratégia – escolher qual regra (alfa ou beta) e em qual fórmula aplicá-la.

As tabelas-verdade, em contraposição, são determinísticas. Não há pontos de escolhas heurísticas.


MÉTODO: FÓRMULAS MARCADAS

Marcam-se as fórmulas com T ou F Exemplo de marcação: TA significa que a fórmula A foi assumida como verdadeira) FB significa que a fórmula B foi assumida como falsa) Cuidado!!! T A → B a fórmula como um todo é verdadeira (e não apenas A)


Dado um sequente B1 , …,Bn ⊢ A1 ,…,Am cria-se o tableau inicial (uma árvore):

MÉTODO: passo 1 – MARCAR AS FÓRMULAS COM T ou F

TB1 … TBn FA1 … FAm

Antecedente é marcado com T

Consequente é marcado com F


Regras α: geram um vértice na árvore de prova Regras β : geram uma bifurcação, logo 2 vértices na árvore

MÉTODO: passo 2 - UTILIZAR REGRAS DE EXPANSÃO α E β

α em 1

α em 1

1.

2.

3.

Aplicação de uma regra α

1.

β em 1

Aplicação de uma regra β

Tableaux Analíticos MÉTODO: REGRAS DE EXPANSÃO α E β


1. Somente fórmulas do tipo alfa ou beta podem ser expandidas; 2. Uma fórmula só pode ser expandida uma vez por ramo; 3. Um ramo está SATURADO quando não há mais fórmulas a serem expandidas. 4. Como as regras alfa e beta sempre geram fórmulas menores, em algum

momento todas as fórmulas serão atômicas e todos os ramos estarão saturados - logo o processo de expansão sempre termina.

MÉTODO: passo 3 – EXPANDIR CADA RAMO ATÉ SATURAÇÃO

α em 1

α em 1

1.

2.

3.

Exemplo de ramo saturado


• Um ramo está FECHADO se possuir um par de fórmulas conjugadas TA e FA • Não é necessário estar saturado para estar fechado!

• Um tableau está FECHADO se todos os ramos estão fechados

• Um sequente B1 , …,Bn ⊢ A1 ,…,Am foi DEDUZIDO pelo método dos tableaux

analíticos se existir um tableau FECHADO para ele;

• Uma dedução de um teorema ⊢ A neste método corresponde a construir um tableau fechado para FA

MÉTODO: passo 4 – tableau está fechado?


Todos os ramos estão fechados, logo foi provado


Todos os ramos estão fechados, logo foi provado


O ramo aberto contém uma valoração que impede a prova (contra-exemplo): v(p)=1 v(r)=0 v(q)=0

O


Sistema dedutivo COMPLETO: se Γ ⊨ 𝐴 então Γ ⊢ 𝐴

Tableaux analíticos para LP são corretos e completos

Sistema dedutivo CORRETO:

se Γ ⊢ 𝐴 então Γ ⊨ 𝐴


Exercícios: Silva, Finger e Melo pg. 55 ex. 2.10 até 2.13 Slides seguintes ...

Tableaux Analíticos Exercício 1: Construa um sequente em Lógica Proposicional e, se for possível, demonstre, usando o sistema de tablôs analíticos que o objeto descrito é um cubo. - Faça a demonstração completa na forma de árvore indicando com

X os ramos fechados e com O, os abertos. - Escreva se demonstrou ou não o consequente e justifique sua

resposta (se conseguiu, explique o porquê, se não foi possível demonstrar, dê TODOS os contraexemplos indicando as valorações dos átomos);

- Na árvore de prova, indique os pontos de indeterminação do método de tablôs analíticos e qual é a indeterminação.

PROPOSIÇÕES Se CUBO então TEM SEIS FACES. Se PIRÂMIDE DE BASE TRIANGULAR então TEM QUATRO FACES. TEM SEIS FACES.

Tableaux Analíticos Exercício 2: Acrescente uma proposição com implicação lógica ao exercício anterior (com exceção de É UM CUBO) que permita deduzir que o objeto em questão é um cubo. Faça a demonstração por tableaux analíticos.

PROPOSIÇÕES Se CUBO então TEM SEIS FACES. Se PIRÂMIDE DE BASE TRIANGULAR então TEM QUATRO FACES. TEM SEIS FACES.

Tableaux Analíticos Exercício 3: Uma das maneiras de resolver o exercício anterior é utilizando a bi-implicação ou bicondicional. Faça as regras tableau para este conectivo (vide exercício 2.12, pg. 10 de Silva, Finger e Melo) e aplique-as na prova.


Algoritmo

Ent: sequente A1, ..., An ⊢ B1, …, Bn Saí: verdadeiro, se A1, ..., An ⊨ B1, …, Bn ou um contra-exemplo

1. Criar um ramo inicial TA1,…,TAn, FB1, FB1,…, FBn

2. Enquanto existir um ramo ABERTO faça

3. Escolher um ramo aberto W

4. Se o ramo W está saturado então

5. encontrar todos os átomos marcados de W

6. retornar a valoração destes átomos marcados

7. Fim se

8. Escolher R (uma das regras aplicáveis em W)

9. Expandir o tableau aplicando R sobre W

10. Verificar se W ou seus sub-ramos fecharam

11.Fim enquanto

12.Retornar verdadeiro

Algoritmo é não-determinístico: onde estão os pontos de indeterminação?


Como resolver as escolhas não-determinísticas? Com estratégias... de escolha de ramos e de escolha de regras



ESTRATÉGIAS PARA ESCOLHA DE RAMOS Profundidade: expandir uma ramo até a saturação (fechado ou saturado) - Ao aplicar uma regra β, a busca continua no ramo contendo β1 - Caso o ramo seja fechado, prossegue-se a busca por β2. Largura: expande-se em sequência cada um dos ramos abertos. Todos os ramos abertos terão mesmo comprimento.


Busca em profundidade é mais eficiente: menos memória e menor tempo (tipicamente menos nós gerados)


ESTRATÉGIAS PARA ESCOLHA DE REGRAS • Regras α primeiro (é uma regra universal)

• Regras β – diversas possibilidades:

• Ordem direta: 1ª. fórmula β do ramo • Ordem reversa: última fórmula β do ramo • Menor tamanho: escolher a menor das fórmulas β • Contém subf: escolher uma fórmula que contenha subfórmulas

presentes no ramo • Combinação das regras anteriores


FORMAS NORMAIS, CLÁUSULAS DE HORN, SAT

REQUISITO PARA RESOLUÇÃO

Formas Normais

• Diversos algoritmos assumem que as fórmulas estão na forma normal que pode ser

– conjuntiva (FNC) ou

– disjuntiva (FND)

• Ex. colocar as fórmulas na FNC é requisito para aplicar o método de prova por resolução – usada por algoritmos SAT em geral

SAT = satisfabilidade

Forma Normal Conjuntiva (FNC)

• FNC: transformar as fórmulas em uma conjunção de disjunções

(¬q p r) (s ¬r) (p) {[¬q, p, r], [s, ¬r], [p]}

Notação clausal (q p r) (r s) p

Forma Normal Conjuntiva (FNC)

FNC: Nomenclatura

{[¬q, p, r], [s, ¬r], [p]}

Literal: é uma fórmula atômica p ou sua negação p Literal positivo: p Literal negativo : q

Cláusula: é uma disjunção de literais. Ex. [¬q, p, r] Cláusula unitária: cláusula com um só literal. Ex. [p] Cláusula vazia: sem literais, é igual a constante falsa ⊥

Forma Normal Conjuntiva

forma geral

⋀ k=1

m

L1 L2 ... Ln k

ATENÇÃO: não confundir fórmula com uma cláusula vazia com fórmula sem cláusula.

Uma fórmula com zero cláusula é igual a constante T por convenção (k=0) Uma cláusula vazia (n=0) é igual a constante falsa ⊥


Teorema: para toda fórmula B da lógica proposicional clássica, há uma fórmula

A na FNC que é equivalente a B

Algoritmo: ENT: uma fórmula B SAI: uma fórmula A na FNC tal que A B Para todas as subfórmulas de X,Y,Z de B faça Redefinir → em termos de e Empurrar as negações para o interior por leis de Morgan Eliminar a dupla negação Aplicar a distributividade de sobre Fim para A fórmula A é obtida quando não mais substituições possíveis

(Silva, Finger e Melo, 2006, pg. 79)


Algumas equivalências notáveis

Problema SAT

SATISFABILIDADE Uma fórmula proposicional é satisfazível se existe uma valoração para seus átomos que a torne verdadeira.

PROBLEMA SAT Dada uma fórmula, provar que existe uma valoração para seus átomos que a torne verdadeira ou provar que não existe tal valoração e que, portanto, a fórmula é insatisfazível.

Cláusulas de Horn

Exemplo (2 cláusulas):

((p q) → r) ((q s) → t) equivalente à (na FNC): (p q r) (q s t)

São cláusulas com no máximo um literal positivo (uso: PROLOG)

Horn

LP

Cláusulas de Horn

Fatos: são cláusulas unitárias em que há um único literal e este é positivo. Ex.: p

Regras: são cláusulas na forma (p1 ⋁ ... ⋁ pn ⋁ q) equivalente à (p1 ⋀ ... ⋀ pn → q)

Consultas ou restrições: são cláusulas de Horn sem átomo positivo (p1 ⋁ ... ⋁ pn)

Tipos de cláusulas

<corpo da regra> → <cabeça>

T→ <cabeça>

<corpo> → ⊥

Cláusulas de Horn: SAT

Propriedades que tornam a manipulação das cláusulas de Horn mais simples do que cláusulas genéricas

LEMA 1 Se C é um conjunto de cláusulas de Horn sem nenhum fato, então C é satisfazível. (considere a situação onde todos os átomos são F)

LEMA 2 C é um conjunto de cláusulas de Horn que contém um fato p. C’ são cláusulas obtidas a partir de C removendo-se o literal p do corpo de todas as cláusulas e todas as cláusulas que contém o literal p (i.e. assume-se que p é true) Então C C’.


Algoritmo de verificação de satisfabilidade em LP

Algoritmo: HornSAT(C) ENT: conjunto de cláusulas C SAI: Verdadeiro se C é satisfazível, Falso, caso contrário. // Casos base 1. Se ⊥ C retorne falso // se cláusula vazia pertence ao cjto C

2. Se C não contém fatos então retorne verdadeiro

// Passos redutores – levam aos casos base 3. Escolha um p C, sendo p um fato (assume-se que p é TRUE) 4. C’ é obtida de C

4.1 removendo-se o literal p de suas cláusulas e 4.2 todas as cláusulas onde o literal p aparece

5. retorne HornSAT(C’)

(Silva, Finger e Melo, 2006)


• Complexidade

– Se n é o número de átomos em C (conjunto de cláusulas) então HornSAT(C) será chamado recursivamente n vezes no máximo

– Portanto, é um algoritmo linear

• Enquanto as tabelas-verdade são exponenciais em função de n: 2n

Problema 2SAT

K-SAT: quando as cláusulas da FNC tem no máximo K literais 2-SAT: podem ser resolvidos em tempo polinomial

Algoritmo 2SAT Algoritmo: 2SAT(C) ENT: conjunto de cláusulas C SAI: Verdadeiro se C é satisfazível, Falso, caso contrário. 1. C := Simplifica(C) 2. Enquanto ⊥ ∉ C e C de faça 2.1 Escolha um átomo p qualquer em C 2.2 C’ := Simplifica (C ⊔ {[p]}) 2.3 Se ⊥ C’ então 2.3.1 C := Simplifica(C ⊔ {[p]}) 2.4 se não 2.4.1 C:=C’ 3. Se ⊥ C então 3.1 retorne FALSO 4. se não 4.2 retorne VERDADEIRO

(Silva, Finger e Melo, 2006) pg. 84

Algoritmo 2SAT

Algoritmo: Simplifica(C) ENT: conjunto de cláusulas C (na notação clausal) SAI: Um conjunto de cláusulas C’ C sem cláusulas unitárias 1. C’ := C 2. Enquanto existe uma cláusula unitária [u] C’ faça 2.1 C’ := C’ – {[c], tal que u é um literal em [c]} // eliminar as cláusulas inteira s contendo u

2.2 Para toda cláusula c =[ u, c’] faça 2.2.1 C’ := C’ ⊔ {[c’]} – {c} // eliminar o literal u de todas as cláusulas

3. Retorne C’

(Silva, Finger e Melo, 2006) pg. 85

Simplificação conhecida como BCP = boolean constraint propagation Para que C seja satisfeito u deve ser satisfeito, portanto C é simplificado em: 2.1 eliminando-se todas as cláusulas contendo u de C (pois já estão satisfeitas) 2.3.1 apagando-se u das demais cláusulas pois u é falso

Problemas >=3SAT

3-SAT: NP-COMPLETO (busca em tempo exponencial em f do tamanho da instância)

Suponha, uma fórmula com n átomos (literais diferentes) que figuram l vezes (negados ou não), então um algoritmo ‘inocente’ que faz todas as valorações possíveis roda em O(2n * l)

2n = número de valorações possíveis para cada um dos literais l = verificar cada valoração de um literal l vezes

MÉTODO DE PROVA POR RESOLUÇÃO

Plano

• Resolução em lógica proposicional (LP)

– método de prova por refutação

• Completude e decidibilidade

MÉTODO DA RESOLUÇÃO

RESOLUÇÃO Método de resolução é feito por redução ao absurdo ou por refutação.

Γ ⊢ sse Γ U { } não é satisfazível

RESOLUÇÃO EM LÓGICA PROPOSICIONAL

Procedimento para lógica proposicional para verificar a se alga é consequência lógica da teoria (Γ ⊢ )

• a teoria Γ aqui será umconjunto de cláusulas na FNC • a ordem dos literais dentro das cláusulas não é importante • a ordem das cláusulas também não é importante

1. Colocar Γ U { } na forma normal conjuntiva (clausal)

2. Verificar se é possível derivar a cláusula ⊥ aplicando-se as regras de resolução

3. Caso seja possível, prova-se por refutação que Γ ⊢

Regras de Resolução • Facilmente entendível pegando-se Modus Ponens

{[p, q], [p]}

{[q]} resoluta: cláusula inferida pela regra

resolventes: cláusulas de entrada REGRA DE RESOLUÇÃO

(p q) (p) conclui-se q em FNC {[p, q], [p]} pode ser resolvida/simplificada para {[q]}

Regras de Resolução • Utilizadas no método de prova por refutação

{[w, q, r], [w, s, r]}

{[w, q, s]} resoluta: cláusula inferida pela regra

resolventes: cláusulas de entrada

{[r], [r]}

{[ ]}

Importante: neste caso, a resoluta é igual [ ] ou ⊥, ou seja, as cláusulas resolventes são insatisfazíveis

regra de RESOLUÇÃO

{[w, w, r]}

{[w, r]}

regra de CONTRAÇÃO

EXEMPLO

a. fund //está no ensino fund.

b. fund criança c. criança masc menino d. jardim criança e. criança fem menina f. fem

Γ ⊢ ? sendo = menina

Γ

1. {[fund], 2. [fund , criança], 3. [criança , masc, menino], 4. [jardim , criança] 5. [criança , fem menina], 6. [fem], 7. [menina]}

Γ U {} na FNC

[fund] [fund , criança]

[criança] [criança, fem, menina]

[fem, menina] [fem]

[menina] [menina]

[ ]

1

5

2

6

7

a cláusula vazia foi derivada, então é deduzível da teoria Γ

RESOLUÇÃO EM LÓGICA PROPOSICIONAL

Método utilizado pelo PROLOG e por provadores de teorema (ex. OTTER) pela simplicidade

Desafios computacionais do método: 1. não-determinístico: é preciso escolher os resolventes a cada passo de

resolução. Qual estratégia? sempre utilizar um resolvente unitário = resolução unitária

2. diminuição do espaço de busca: descartar fórmulas que subsumem outras (englobam). [a, b, c] [a, p] [b, p]

[a, b]

[a, b] está contida em [a,b,c] então [a,b,c] pode ser eliminada diminuindo o espaço de busca para {[a, p], [b, p], [a, b]}

COMPLETUDE

O procedimento de resolução é completo e correto se restrito à refutação, i.e. a derivação da cláusula vazia [ ].

Não é completo se não usarmos refutação, pois é possível demonstrar que uma conclusão é consequência lógica de Γ embora não se consiga derivar a partir de Γ utilizando as regras de resolução.

COMPLETUDE

Exemplo: p ⊢ p q Não é possível aplicar a regra de resolução somente a cláusula [p], mas é trivial ver que [p, q] é consequência lógica de [p]. Sempre que v(p)=1, v(p v q) = 1. Daí, para fins de completude do método de resolução, a idéia de se fazer prova por refutação {[p], [p], [q]} ⊢ [ ]

Método de Resolução

• Exercício 3.15 pg. 92 (Silva, Finger e Melo)

– Resolução linear = a resoluta vira resolvente no passo seguinte.

Documents

Resolução exercício dos cubos - DAINFtacla/logica/slides/LP-02-Sistemas... · Dedução Natural: conjunto de regras para lógica proposicional (inclusão e eliminação para cada