Sistemas Dedutivos

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

22/10/2013 08:44

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 ou hipótese 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.

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). Ex. de teorema: o centro da circunferência circunscrita a um triângulo é o ponto de intersecção das mediatrizes desse triângulo. 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

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) ⊢ (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[P:= (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 → 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

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

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: uma para inserção do conectivo na prova e outra para a remoção do conectivo

Dedução Natural

Regras

+

Exemplo

+

Exercício

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

Tableaux Analíticos

É 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 não são decídiveis para LPO (porém, são decidíveis para LP)

DECIDÍVEL

Tableaux Analíticos

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.

Tableaux Analíticos

Prova por refutação Fórmulas marcadas Regras de expansão Provas por tableaux Correção, completude e decidibilidade Algoritmo

FORMAS NORMAIS E CLÁUSULAS DE HORN

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) { [¬q, p, r], [s, ¬r] }

cláusula cláusula

fórmula

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

literal: p ou p

cláusula: disjunção de literais

vazia: sem literais, é igual a constante falsa ⊥

unitária: um só literal

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 é igual a constante falsa ⊥

Forma Normal Conjuntiva

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)

Forma Normal Conjuntiva

Algumas equivalências notáveis

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

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’.

Cláusulas de Horn

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 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 é T) 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)

MÉTODO DE PROVA POR RESOLUÇÃO

Plano

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

– método de prova por refutação

• Resolução em lógica de primeira ordem (LPO)

– Reduzir a resolução em LPO à resolução em LP pela:

• Eliminação/instanciação do universal

• Eliminação do existencial (skolemização)

• Completude e decidibilidade

MÉTODO DA RESOLUÇÃO

RESOLUÇÃO No nosso caso, interessa resolução para uma linguagem mais próxima possível da LPO completa (com quantificadores, negação, predicados n-ários, funções, …). Também nos interessa o método de resolução por redução ao absurdo ou por refutação.

Γ ⊢ sse Γ U { } não é satisfazível (prova por refutação)

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 em outros casos, 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 EM LPO

RESOLUÇÃO EM LPO

Resolução com lógica proposicional está um pouco distante da LPO pois não considera os quantificadores universal e existencial, nem predicados e funções n-ários com n>0.

Para fazer inferência com quantificadores, a idéia básica é reduzi-la à inferência da lógica proposicional

BASTA ELIMINARMOS OS QUANTIFICADORES!!!

RESOLUÇÃO EM LPO

1. Colocar a Γ U { } na FNC 2. Eliminar os quantificadores universais * 3. Aplicar a regra de resolução

*primeiramente, excluiremos somente o quantificador universal , depois veremos como excluir o existencial.

FNC em LPO

• Eliminar implicação lógica

• Mover negações para dentro para que precedam os átomos utilizando as equivalências

• x() substituir por x( )

• x() substituir por x.

• Padronizar as variáveis: cada quantificador deve corresponder a uma variável

• x(p(x)) q(x) substituir por z.(p(z)) q(x)

• Eliminar todos os existenciais (será visto mais tarde)

• Mover universal para fora do escopo do e do utilizando as equivalências: ( x(β)) substituir por x( β) desde que x não seja var. livre em ( x(β)) substituir por x( β) desde que x não seja var. livre em

• Fazer conjunção de disjunções por meio da distributiva e das leis de Morgan

• Não colocar os quantificadores universais na FNC pois todas as fórmulas quantificadas serão universais (desprezar ≠ eliminar)

ELIMINAÇÃO DO UNIVERSAL

X(rei(X) ganancioso(X) perverso(X)) joão constante que denota um objeto do domínio ricardo constante que denota um objeto do domínio pai(X) função que retorna o pai de X que é um objeto do domínio

Pela instanciação universal obtém-se: rei(joão) ganancioso(joão) perverso(joão) rei(ricardo) ganancioso(ricardo) perverso(ricardo) rei(pai(joão) ganancioso(pai(joão)) perverso(pai(joão)) … …

{X/joão} {X/ricardo}

{X/pai(joão)}

sub

stit

uiç

ões

Termos básicos: não apresentam variáveis

Pode-se eliminar o quantificador universal pela instanciação universal ou unificação, i.e. substituir as variáveis por valores concretos.

EXEMPLO RESOLUÇÃO EM LPO

1. X (fund(X) criança(X)) 2. X (criança(X)brinca(X)) 3. fund(maria)

Γ ⊢ ? sendo = brinca(maria)

Γ

1. {[fund (X), criança(X)], 2. [criança (X), brinca(X)], 3. [fund(maria)], 4. [brinca(maria)]}

Γ U {} na FNC

[fund (X), criança(X)] [fund(maria)]

X/maria criança(maria) [criança (X), brinca(X)]

X/maria

[brinca(maria)] [brinca(maria)]

[ ]

Logo, brinca(maria) é uma consequência lógica das fórmulas em Γ

EXEMPLO RESOLUÇÃO EM LPO

(extraído de Brachman e Levesque, 2005)

PREDICADOS RESPOSTA

(extraído de Brachman e Levesque, 2005)

Cada derivação produz uma só resposta. Se tivéssemos Happy(Sue) na KB terímos que fazer outra substituição {x/sue}. Porém, a resposta pode ser uma disjunção →

Negação da query= x(Student(x) or Happy(x))

PREDICADOS RESPOSTA

A resposta é jane ou john. Não há certeza sobre qual deles está feliz.

ELIMINAÇÃO DO EXISTENCIAL

• Para completar a resolução em LPO, é preciso tratar fórmulas com o quantificador existencial

• Para tal, faz-se a instanciação do existencial ou skolemização (do autor, Skolem).

• A idéia básica é exemplificada:

X(coroa(X) naCabeça(X, joão))

Se existe um objeto que é uma coroa e que está sobre a cabeça do João, então podemos supor que este objeto existe e nomêa-lo com um símbolo constante que não exista e nem venha a se repetir na KB. No exemplo, c1 é chamado de constante de skolem.

coroa(c1) naCabeça(c1, joão)

SKOLEMIZAÇÃO

• Se existe um x, chame-o de a (constante)

• Se para todo x existe um y, chame-o de f(x)

x1 yP(x1,y) x1P(x1,f(x1))

x1 x2 yP(x1, x2, y) x1 x2P(x1, x2, f(x1, x2))

x1 x2 … xn yP(x1, x2, …, xn, y) x1 x2P(x1, x2, …, xn, f(x1, …, xn))

f é um novo símbolo de função que não existe em nenhum outro lugar da KB

x mae(x, jose) mae(a, jose)

x1y(pessoa(x1) mae(y, x1)) x1(pessoa(x1) mae(f(x1), x1))

Exemplo

Exemplo de SKOLEMIZAÇÃO

1. X (homem(X) → pessoa(X)) 2. X Y (pessoa(X) → mae(Y, X)]) % y é mãe de x 3. X, Y (mae(X, Y) → ama(X, Y)) 4. homem(platao) Pergunta-se: Y ama(Y, platao) % alguem ama a Platão? X/platao em 1: pessoa(platao) Y/f(X) em 2, skolemizacao: pessoa(platao) -> mae(f(platao), platao) mae(f(platao), platao) -> ama(f(platao), platao) Logo, a query pode ser satisfeita com as instanciações: X/platao Y/f(platao)

Este exemplo foi implementado em ex090-00-skolemizacao.pl

IMPLICAÇÃO DA SKOLEMIZAÇÃO

Quando fazemos instanciação dos existenciais numa KB, a nova KB não é logicamente equivalente à anterior pois x.P(x) P(a) é falso!!!

Porém, a KB antiga e a nova (resultante da skolemização) apresentam equivalência inferencial, i.e. é satisfazível sse ’ é satisfazível, sendo ’ o resultado da skolemização.

Preservar a equivalência inferencial ou a satisfabilidade é suficiente para resolução!

DEPENDÊNCIA DAS VARIÁVEIS

• A ordem de aparecimento dos quantificadores é importante na resolução em LPO.

• Esta ordem gera dependências entre as variáveis o que afeta a skolemização e a satisfabilidade!

x y.R(x, y)╞ y x.R(x, y) é satisfazível

y x.R(x, y) ╞ x y.R(x, y) não é satisfazível

DEPENDÊNCIA DAS VARIÁVEIS

x y.R(x, y)╞ y x.R(x, y)

y x.R(x, y) ╞ x y.R(x, y)

satisfazível não é satisfazível

1. Mostrar que as cláusulas abaixo derivam []

2. {x/a}

3. Negação para dentro e {y/b}

4. Unificar pela substituição {x/a, y/b}

2. {x/f(y)} // x depende de y

3. Negação para dentro e {y/g(x)}

4. Não há unificação

1. Mostrar que as cláusulas abaixo derivam []

DECIDIBILIDADE

• A resolução por derivações não oferece solução geral para o cálculo da consequência lógica (nem com a instanciação dos quantificadores universais e existenciais)

• Há situações onde há infinitas substituições. Por exemplo, se há um símbolo de função, o número de substituições é infinito.

DECIDIBILIDADE KB: X rei(X) ganancioso(X) perverso(X) joão constante que denota um objeto do domínio ricardo constante que denota um objeto do domínio rei(joão) ganancioso(joão) pai(X) função que retorna o pai de X

Pela instanciação universal obtem-se: rei(joão) ganancioso(joão) -> perverso(joão) rei(ricardo) ganancioso(ricardo) -> perverso(ricardo) rei(pai(joão) ganancioso(pai(joão)) -> perverso(pai(joão)) … …

{X/joão} {X/ricardo}

{X/pai(joão)}

{X/pai(pai(joão))}

{X/pai(pai(pai(joão)))}

substituições

Exercício: demonstrar que pode-se fazer infinitas substituições se retirarmos a sentença ganancioso(joão) e quisermos demonstrar que há um rei perverso.

DECIDIBILIDADE • Resoluções geradas pela instanciação universal e

existencial são completas.

• i.e. toda sentença que é consequência lógica da KB pode ser demonstrada. Algum ramo de derivação conterá a cláusula [ ], mesmo que existam outros ramos infinitos. Por isto, deve-se fazer busca breadth-first.

• Porém, se a sentença não é satisfazível, a prova pode prosseguir indefinidamente pelo aninhamento de funções nas substituições

• Nesta situação, não é possível saber se não se pode deduzir a sentença ou se ainda não se chegou a dedução!!!

• Alguns autores dizem que o cálculo da consequência lógica em LPO é semi-decídivel por este motivo.

Melhorias na resolução

• Face as constatações de que não há garantia de terminação da resolução e não maneira de garantir eficiência, há algo a ser feito? Sim…

– É possível reduzir redundâncias nas buscas, fazendo substituições mas genéricas possíveis > most general unifiers

– Escolhas arbitrárias nas substituições podem impedir que um caminho atinja a cláusula []. Não é preciso atribuir um valor específico a uma variável, pode-se deixar este comprometimento para mais tarde

Resolução é difícil

• Resolução em LPO não tem garantias de término

• Na lógica proposicional: – Haken demonstrou em 1995 que sabendo-se que

há cláusulas não satisfazíveis {c1, …, cn} na KB, a derivação mais curta para a cláusula [] é da ordem de 2n

cláusulas.

– Portanto, mesmo se as vezes a cláusula [] pode ser encontrada imediatamente, em alguns problemas a busca pode requerer tempo exponencial.

Resolvedores SAT

• São algoritmos utilizados para encontrar valorações para cláusulas que são satisfazíveis (para lógica proposicional)

Implicações para KR

• Problema: como gerar consequências lógicas em tempo razoável para realizar ações imediatas

– Provadores de teoremas completos podem não ser úteis para KR – Outras opções:

• Dar maior controle ao usuário • Linguagens menos expressivas (ex. cláusulas de Horn)

• Em algumas aplicações, é razoável esperar bastante tempo: provar um teorema matemático pode levar meses!

• Em geral, a melhor alternativa é a utilização do most general unifier para evitar buscas redundantes

• Mas há outras estratégias… – eliminação de cláusulas: ex. que contêm um literal que não aparece em outras cláusulas – Ordenação da resolução: ex. primeiro cláusulas unitárias – Utilizar lógica tipificada (sorted logic): unificar cláusulas somente qdo os tipos forem

compatíveis – …

Referências

• Robinson J. A. "A Machine-Oriented Logic Based on the Resolution Principle." J. Assoc. Comput. Mach. 12, 23-41, 1965.