58
Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula.

Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Embed Size (px)

Citation preview

Page 1: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Monitoria de Lógica para Computação – EC

Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala

de aula.

Page 2: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Mini prova 1Lógica aristotélica.

Page 3: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Algum A é B Nenhum H é B-------------------------- O argumento é

valido ? Nenhum A é H

Todo A é B. Nenhum C é B. O conjunto de sentenças é y é C. y é A. consistente ?

Validade x Consistência

Page 4: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Primeiro vamos saber o que é um argumento...

Um argumento é uma sequência de sentenças. Mas não uma sequência qualquer. Essas sentenças

precisam ter uma relação entre si (silogismo). Uma delas é chamada de conclusão (tese) e as

demais são as justificativas que garantem a conclusão, que chamamos de premissa.

Validade

Page 5: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Quando um argumento é válido? Um argumento é válido se toda situação que torne as premissas verdadeiras torne também a conclusão

verdadeira. Ou, de outro modo, um argumento é válido se não existe situação que torne as premissas

verdadeiras e a conclusão falsa. Toda vez que as premissas forem falsas ou

tiverem uma contradição, o argumento será válido.

(P1 ^ P2 ^ P3 ^ ... ^ Pn ) -> C

Validade

Page 6: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Ex.:Todo P é M.Algum S é M.

-----------------Algum S é P.

O argumento é válido?

ValidadeP = M P M

S = M

S M MS M

S

S = M = P S P = M P = M

S P = MS

P S =M P

M S ...

Opa! Há ao menos um caso em que nenhum S é P! Ou seja, há ao menos um caso em que as premissas são verdadeiras e a conclusão, falsa.

Page 7: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

O argumento da questão anterior é válido?Não! Pois há ao menos um caso em que as

premissas são verdadeiras e a conclusão é falsa! Agora que encontramos esse caso, não precisamos

mostrar as demais possibilidades.

Obs.: No caso de um argumento válido, é necessário mostrar que em todos os casos em que as premissas são verdadeiras, a conclusão também é!

Validade

Page 8: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Quando um conjunto de sentenças é consistente?

Um conjunto de sentenças em lógica proposicional é dito consistente se houver um conjunto de valores-verdade para as proposições tal que todas as sentenças sejam verdadeiras simultaneamente.

Consistência

Page 9: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Ou seja, usando o diagrama de venn, basta que encontremos um caso em que todas as sentenças sejam verdadeiras simultaneamente.

Você pode perceber que para um conjunto de sentenças inconsistentes, é impossível achar um caso valido, ou seja, no conjunto de sentenças há algum tipo de contradição, implícita ou explicita.

Consistência

Page 10: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Ex.: Todo A é B. Nenhum C é B. y é C. y é A.

O conjunto de sentenças é consistente?

Consistência

A = B BA

C B

A = B BA

C Cyy y y

Opa! Em todos os casos é impossível

que todas as 4 sentenças sejam

verdadeiras simultaneamente!

Page 11: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

O conjunto de sentenças anterior é consistente? Não! Pois em todos os casos possíveis, não

existe ao menos um caso em que as 4 sentenças sejam verdadeiras simultaneamente!

Obs.: No caso de um conjunto de sentenças consistente, basta que encontremos um caso em que todas as sentenças sejam verdadeiras simultaneamente.

Consistência

Page 12: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Se em um argumento as premissas formarem um conjunto inconsistente então o

argumento será válido independentemente do que seja sua conclusão.

Por quê?

Observação

Page 13: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Se em um argumento as premissas formarem um conjunto inconsistente ...” Premissas inconsistentes? Ou seja, as premissas não podem ser verdadeiras simultaneamente!

“... então o argumento será válido independentemente do que seja sua conclusão.”Argumento válido independentemente da conclusão? Sim, pois se não há caso em que as premissas sejam verdadeiras, então também não há caso em que as premissas são verdadeiras e a conclusão falsa!

(P1 ^ P2 ^ ... ^ Pn ^ ¬Pn ) -> C ou seja zero -> qualquer coisa = Válido.

Vamos Analisar

Page 14: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

João é professor. João não é professor.--------------------------- Logo, a Lua é feita de queijo.

Chamemos:João -> JConjuntos dos professores -> PLua -> LConjunto das coisas feitas de queijo -> Q

Exemplificando J é P J não é P------------ L é Q

P P

jj

Impossível ‘juntar’ as duas premissas! Logo, não há ao menos um

caso em que as premissas sejam verdadeiras e a conclusão falsa!

Portanto, o argumento é válido!

Page 15: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Paradoxo

Page 16: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Exercícios

Page 17: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Mini prova 2 Conjuntos Indutivos

Fechos Indutivos

Page 18: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Seja A um conjunto e X um subconjunto de A (X ⊂ A). Considere F um conjunto de funções cada uma com sua aridade.

Dizemos que um subconjunto Y de A (Y ⊆ A) é indutivo em relação à base X e a F se:1. Y contém a base X. (X ⊂ Y)2. Y é fechado sobre todas as funções de F.

Y é um conjunto indutivo em relação a X e a F.

Conjuntos Indutivos

A X Y

F = { f1, f2, ... }

Page 19: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Como nós chegamos ao menor conjunto indutivo ?

Há duas formas de chegarmos ao fecho indutivo:1. De baixo para cima ( bottom-up )2. De cima para baixo ( top-down )

Fecho Indutivo

Page 20: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Sejam f e g funções de F e a, b e c elementos da base.

Fecho indutivo ( Bottom-up )

f(_,_) g(_)

f(a,b) f(b,a) f(a,c) f(c,a)

f(b,c) (...)

f(c,b) g(a) g(b) g(c)

a b c

Page 21: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

a

b c

f(a,b) f(b,a) f(a,c) f(c,a) f(b,c)

f(c,b) g(a) g(b) g(c)

X+

...

f(a,f(a,b)) f(a,f(b,a)) f(a,f(a,c)) f(a,f(c,a)) f(a,f(b,c)) f(a,f(c,b)) f(a,g(a)) f(a,g(b)) f(a,g(c)) f(f(a,b),a) f(f(b,a),a) f(f(a,c),a)

f(f(c,a),a) f(f(b,c),a) f(f(c,b),a) f(g(a),a) f(g(b),a) f(g(c),a) f(b,f(a,b)) f(b,f(b,a)) f(b,f(a,c)) f(b,f(c,a)) f(b,f(b,c)) f(b,f(c,b)) f(b,g(a)) f(b,g(b))

f(b,g(c)) f(f(a,b),b) f(f(b,a),b) f(f(a,c),b) f(f(c,a),b) f(f(b,c),b) f(f(c,b),b) f(g(a),b) f(g(b),b) f(g(c),b) f(c,f(a,b)) f(c,f(b,a)) f(c,f(a,c)) f(c,f(c,a)) f(c,f(b,c)) f(c,f(c,b)) f(c,g(a)) f(c,g(b)) f(c,g(c)) f(f(a,b),c) f(f(b,a),c) f(f(a,c),c) f(f(c,a),c) f(f(b,c),c) f(f(c,b),c) f(g(a),c) f(g(b),c) f(g(c),c) f(f(a,b),f(a,b)) f(f(a,b),f(b,a)) f(f(a,b),f(a,c)) f(f(a,b),f(c,a)) f(f(a,b),f(b,c)) f(f(a,b),f(c,b)) f(f(a,b),g(a)) f(f(a,b),g(b)) f(f(a,b),g(c)) f(f(b,a),f(a,b)) f(f(a,c),f(a,b)) f(f(c,a),f(a,b))

f(f(b,c),f(a,b)) f(f(c,b),f(a,b)) f(g(a),f(a,b)) f(g(b),f(a,b)) f(g(c),f(a,b)) f(f(b,a),f(b,a)) f(f(b,a),f(a,c)) f(f(b,a),f(c,a)) f(f(b,a),f(b,c)) f(f(b,a),f(c,b)) f(f(b,a),g(a))

f(f(b,a),g(b)) f(f(b,a),g(c)) f(f(a,c),f(b,a)) f(f(c,a),f(b,a)) f(f(b,c),f(b,a)) f(f(c,b),f(b,a))

f(g(a),f(b,a)) f(g(b),f(b,a)) f(g(c),f(b,a)) f(f(a,c),f(a,c)) f(f(a,c),f(c,a)) f(f(a,c),f(b,c)) f(f(a,c),f(c,b)) f(f(a,c),g(a)) f(f(a,c),g(b)) f(f(a,c),g(c)) f(f(c,a),f(a,c)) f(f(b,c),f(a,c)) f(f(c,b),f(a,c)) f(g(a),f(a,c)) f(g(b),f(a,c)) f(g(c),f(a,c)) f(f(c,a),f(c,a)) f(f(c,a),f(b,c)) f(f(c,a),f(c,b)) f(f(c,a),g(a)) f(f(c,a),g(b)) f(f(c,a),g(c)) f(f(b,c),f(c,a)) f(f(c,b),f(c,a)) f(g(a),f(c,a)) f(g(b),f(c,a))

f(g(c),f(c,a)) f(f(b,c),f(b,c)) f(f(b,c),f(c,b)) f(f(b,c),g(a)) f(f(b,c),g(b)) f(f(b,c),g(c)) f(f(c,b),f(b,c)) f(g(a),f(b,c)) f(g(b),f(b,c)) f(g(c),f(b,c)) f(f(c,b),f(c,b)) f(f(c,b),g(a))

f(f(c,b),g(b)) f(f(c,b),g(c)) f(g(a),f(c,b)) f(g(b),f(c,b)) f(g(c),f(c,b)) f(g(a),g(a)) f(g(a),g(b)) f(g(a),g(c)) f(g(b),g(a)) f(g(c),g(a)) f(g(b),g(b)) f(g(b),g(c)) f(g(c),g(b)) f(g(c),g(c))

Page 22: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Uma definição mais formal... Vamos construir o fecho indutivo a partir da

base:

Fecho indutivo ( Bottom-up )

)},...,,({ 211

0

knn xxxfXXXX

Onde aridade (f) = k e x1, x2, ..., xk ∊ Xn e ∊ F

Page 23: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Considere a família C de conjuntos indutivos em relação a X e F.

Perceba que C não é vazia pois contém pelo menos A.

Considere X+= ∩ C o conjunto formado pela intersecção de todos os conjuntos de C.

Temos que X+ é o menor conjunto indutivo em relação a X e F (fecho indutivo)

Fecho Indutivo – Top-down

Page 24: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Definição: Sejam A e X conjuntos, X está contido em A, e

seja F um conjunto de funções que recebem como parâmetro elementos de A: O fecho indutivo de X+ de X sob F será livremente gerado se e somente se: Todas as funções de F forem injetoras. Sejam f e g funções de F sobre X+, o conjunto imagem de f

e g são disjuntos. Nenhum elemento da base X é resultado de aplicações de

f sobre o fecho de X.Todo CLG tem a propriedade de leitura única, ou seja, só existe uma forma de, aplicando funções de F, se “chegar” a elementos do conjunto CLG. f(a,b) != g(a,b) != f(g(a),f(a,b)) !=(...)

Conjuntos Livremente Gerados

Page 25: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Exercícios1. Dê uma definição indutiva para os conjuntos abaixo:a)Conjunto das cadeias binárias de tamanho par.b)Conjunto das cadeias binárias que têm a quantidade de 1’s maior que a quantidade de 0’s e os 0’s aparecem antes dos 1’s;

2)Usando conjuntos indutivos, construa o conjunto de todas as cadeias binárias palíndromas e de tamanho ímpar:

a) Dê a base e as funções de geração desse conjunto:b) O conjunto gerado em a) é livremente gerado?c) Qual o menor conjunto indutivo ?d) Qual o maior conjunto indutivo que satisfaz a propriedade dita na questão?

Page 26: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Mini prova 3Tabela Verdade, recursão e provas por indução

em conjuntos indutivos

Page 27: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

O que vocês precisam saber ?

• Satisfatível• Insatisfatível• Tautologia• Refutável

Como começar?• 2ⁿ número de linhas, onde n = número de variáveis• Estabelecer todas as possibilidades

Quais as vantagens x desvantagens?• É simples (implementação + verificação)• É custoso (o tempo de resposta para verificar é longo)• É limitado (para fórmulas muito grandes, o método é exaustivo)

Tabela Verdade

Page 28: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

y = ((((A→∼B)→C)→((∼D→(∼B v A))→C)) v A) y é Tautologia ?

Exercício

Page 29: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

• Por onde começar?• Defina as funções recursivas que está sendo pedida;

• Faça isso para os três casos: • Atômico• Unário• Binário

• Estabeleça as hipóteses de indução pros dois casos indutivos:• Unário tem uma hipótese de indução• Binário tem duas hipóteses de indução

• Prove por indução estrutural.

Indução sobre FBF

Page 30: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

1) Mostre, por indução, que, para toda fórmula  Φ da lógica proposicional, o numero de subexpressoes de  Φ é no máximo igual a duas vezes o numero de operadores de  Φ mais 1. (Obs.: Defina recursivamente as funções necessárias para a formalização do problema, e use indução para provar o enunciado.)

Exemplo

Page 31: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

1. Para provar algo por indução, precisamos primeiramente definir as funções que estão sendo pedidas no problema. Elas são: o número de subexpressões e o número operadores.

Seja S(x) o número de subexpressões de x, e C(x) o número de conectivos de x:.

Para o caso atômico:S(x) = 1C(x) = 0

Para o caso unário, onde x = ¬p (e p é uma fórmula qualquer)

S(¬p) = 1 + S(p)C(¬p) = 1 + S(p)

Resolução

Page 32: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Para o caso binário, onde x = p#q, onde p e q são fórmulas quaisquer e # é um operador binário.

S(p#q) = 1 + S(p) + S(q) - |S(p)∩ S(q)|C(p#q) = 1 + C(p) + C(q)

Pronto, definimos as funções, qual o próximo passo ?

Precisamos Agora definir nossas hipóteses de indução pro caso unário e binário:

H.I pro unário: S(p) <= 2.C(p) + 1H.I 1 pro binário: S(p) <= 2.C(p) + 1H.I 2 pro binário: S(q) <= 2.C(q) + 1

Continuação

Page 33: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Caso binário:S(p#q) <= 2.C(p#q) + 1Por definição:1 + S(p) + S(q) - |S(p)∩ S(q)| <= 2. (1 + C(p) + C(q) ) + 1S(p) + S(q) - |S(p)∩ S(q)| <= 2 + 2.C(p) + 2.C(q)S(p) + S(q) - |S(p)∩ S(q)| <= 2.C(p) + 1 + 2.C(q) + 1

-Como, por hipótese S(p)<= 2.C(p) + 1 e S(q) <= 2.C(q) + 1, então:S(p) + S(q) <= 2.C(p) + 1 + 2.C(q) + 1 também é verdade.-Porém |S(p)∩ S(q)| é sempre positivo, então, podemos subtrair algo positivo do termo menor, que ainda continuará sendo menor, então: S(p) + S(q) - |S(p)∩ S(q)| <= 2.C(p) + 1 + 2.C(q) + 1 Está provado por H.I.

(...)

Page 34: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Agora, como último passo, iremos provas pros três casos: Caso atômico (base):

S(p) <= 2.C(p) +1 Sendo que S(p) = 1 e C(p) = 0, pro Atômico logo:

1 <= 2.0 +1 [provado pela definição] Caso Unário:

S(¬p) <= 2.C(¬p) +1Por definição, temos:1 + S(p) <= 2.( 1 + C(p) ) + 11+ S(p) <= 2 + 2.C(p)  + 1S(p) <= 2.C(p) + 1 + 1

Como, por hipótese temos que S(p) <= 2.C(p) + 1, então, se adicionarmos +1 ao termo da direita, ainda continuará sendo verdade. Então, provamos por H.I.

Continuação

Page 35: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Mostre, por indução, que, para toda fórmula Φ da lógica proposicional, o posto de Φ é no máximo igual ao número de operadores de Φ. (Obs.: Defina recursivamente as funções necessárias para a formalização do problema, e use indução para provar o enunciado.)

Exercício

Page 36: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Teorema da Extensão Homomórfica Única

A

B

f

g

h(_)

h’(_)

X

Page 37: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Mini Prova 4Método dos Tableaux Analíticos, Resolução, Dedução Natural e Cálculo de Sequentes

Page 38: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Dizemos que uma frase S é consequência lógica de um conjunto de frases T, desde que todas as atribuições de verdade que tornem as frases de T simultâneamente verdadeiras, também tornem S verdadeira.

Consequência Lógica

Page 39: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Vamos considerar o conjunto que tem como membros todas as frases de T mais a frase S, ou seja T {S}.

Dizemos que a frase S é consequência lógica do conjunto T se e só se o conjunto T {S} é um conjunto logicamente falso, ou seja nunca pode ser satisfeito.

“Ou seja, pra S ser consequencia Lógica de T, tudo que satisfazer T também tem que satisfazer S, então T {S} será sempre falso, pois falso e qualquer coisa é falso.”

Page 40: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Estratégia : Montar uma “Árvore de Possibilidades”, onde cada caminho da raiz até uma folha caracteriza um “Mundo Possível”

E pra isso iremos utilizar algumas regras…

Tableaux Analíticos

Page 41: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Regras:

Tableaux Analíticos

Page 42: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

{C → D, ¬(B v D), A → (B v C)}╞ ¬A ?

Tableaux Analíticos - Exercício

Page 43: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

O método da resolução é outra forma para verificarmos se uma sentença é consequência lógica de um conjunto de sentenças.

Podemos definir um algoritmo pra utilizarmos esse método...

Resolução

Page 44: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Primeiro transforme as sentenças na forma: (T1 T2 .... Tn S)

Depois transofme tudo isso na forma normal conjuntiva (FNC). Substituindo os símbolos lógicos “implica” e “se somente se”, e depois usando as leis de De Morgan e a propriedade distribuitiva.

P->Q = ¬P v Q ¬(A ^ B) = (¬A v ¬B) (...)

Resolução

Page 45: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Ao ter uma conjunção de cláusulas, basta adicionarmos novas cláusulas que derivem da junção de duas cláusulas antigas. Ex: (¬r v a) ^ (r v b), gerará a v b. Faremos isso várias vezes, até esgotarmos as possibilidades ou chegarmos a uma cláusula vazia, teremos que todo o conjunto é vazio

Page 46: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Como é uma conjunção de cláusulas, se uma for vazia, todas as outras serão, sendo então consequência lógica.

Se não conseguir, não será consequência lógica. Já que não conseguimos refutar as cláusulas.

Resolução

Page 47: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Vantagens: Não é necessário o uso de equivalências para rearranjar p v q como q v p. Já que tudo é colocado na FNC antes da aplicação do método, e para o método a posição do átomo a ser eliminado é indiferente.

Existe apenas uma regra de inferência para ser lembrada

Fácil de ser mecanizado, porém em provas longas , é possível “andar em círculos”

Linguagem Prolog está baseada no princípio da resolução aplicado a cláusulas de Horn, usando busca em profundidade.

Resolução

Page 48: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Cláusula de Horn: é uma disjunção que contém no máximo um literal positivo, sendo muito importante para a computação, nos ramos de IA, Teoria Lógica, Banco de Dados e Engenharia de Software.

Ex.: ¬q v ¬t v p v ¬s v ¬z

Resolução

Page 49: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

{X v (Y ^ P), ¬(P ^ Q), ¬(X v Y) ^ (Q v S),¬X} |= S

Resolução - Exercício

Page 50: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Estratégia: Utilizar uma árvore de dedução através das regras de introdução e eliminação;

Dedução Natural

Page 51: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Introdução do E (^):

Introdução do OU (v)

Introdução do Implica: Se supormos que A é verdade e através de derivações chegarmos em B, temos A→B;

Introdução da Negação:Se supormos que A é verdade e através de derivações chegarmos em um absurdo, temos ¬A;

Introdução dos Operadores

Page 52: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Eliminação do E: Se temos que A^B é verdade, então A é

verdade e B é verdade; Eliminação do OU: Se temos que AvB é verdade, então um dos

dois deve ser verdade. Então supomos os dois como verdade e dos dois, devemos obter o mesmo resultado;

Eliminação dos Operadores

Page 53: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Eliminação do Implica: Se temos que A→B é verdade, então se A for verdade, B também é. Então supomos A como verdade (se já soubermos que A é verdade, não precisa supor);

Eliminação da Negação: Se temos ¬A como verdade, então forçamos um absurdo para eliminar a negação;

Eliminação dos Operadores

Page 54: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Provar que:

http://www.danielclemente.com/logica/dn.en.html Site com diversos exercícios de dedução Natural

Dedução Natural - Exercício

Page 55: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Estratégia: analisar as hipóteses (esquerda) e suas proposições (direita) através de regras estruturais presentes no símbolo de derivação:

Onde as hipóteses A são “negativas” e as proposições B são “positivas”

Cálculo de Sequentes

Page 56: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Dualidade Importante:

Page 57: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

Regras

Page 58: Monitoria de Lógica para Computação – EC Slides baseados em slides antigos da monitoria e nos slides utilizados pela professora em sala de aula

ⱶ A ˅ ¬A

(A-> B), (C->D) ⱶ (A^C) -> (B^D

Calculo de Sequentes - Exercício