Aula08 ComputacaoNaLogicaDePredicados

Prévia do material em texto

LÓGICA APLICADA A COMPUTAÇÃO
Aquiles Burlamaqui2009.3
Ementa
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
2
 Unidade 2
 Lógica de Predicados: Linguagem e Semântica 
 Tradução do português para a Lógica
 Quantificadores e Tipos
 Quantificadores como Conjunções e Disjunções Infinitas
 Linguagem de Primeira Ordem
 Verdade
 A Teoria Formal da Lógica de Predicados 
 Teoria Formal do Calculo de Predicados
 Teorema da Dedução
 Computação na Lógica de Predicados
 Resolução
 Resultados de Completude
Computação na Lógica de Predicados 
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
3
 Resolução
 Resultados de Completude
 Exercícios
Resolução
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
4
 Descrição do esquema de computação para o 
calculo de predicados.
 Lógica proposicional = somente cláusulas básicas. 
(sem variáveis)
 Lógica predicados = cláusulas mais complexas, 
variáveis.
Resolução
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
5
 Uma fbf de LP está na forma clausal se ela é 
sentença como descrita na gramática.
 Na resolução geral queremos que as fbf’s forma 
normal conjuntiva reduzida sem quantificadores
Resolução
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
 Passos:
1. Transformar a fórmula a sua forma normal prenex
2. Realizar o fecho da formula
3. Eliminar quantificadores existências aplicando o processo 
de skolemização
4. Eliminar arbitrariamente todos os quantificadores 
universais
5. Transforma a forma normal conjuntiva reduzida usando o 
algoritmo da proposição 5.1.4
Resolução
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
 Transformar a fórmula a sua forma normal prenex
Resolução
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
8
Resolução
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
10
 Realizar o fecho da formula
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
11
 Eliminar quantificadores existências aplicando o processo de 
skolemização
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
12
 Eliminar quantificadores existências aplicando o processo de 
skolemização
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
 Eliminar arbitrariamente todos os quantificadores universais
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
14
 Transforma a forma normal conjuntiva reduzida usando o 
algoritmo da proposição 5.1.4
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
16
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
17
Resolução
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
 Dominio de Herbrand
 Expansão de Herbrand
 Teorema de Herbrand
 Substituição
 Unificador mais geral
Domínio de Herbrand
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
19
Expansão de Herbrand
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
21
 Forma Clausal
 Forma normal prenex
 Forma normal conjuntiva reduzida
Teorema de Herbrand
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
 Se  for insatisfatível  é universalmente válido 
 Como descobrir se  é insatisfatível?
 Testar todos os valores?
Resolução
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
 Substituição
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
24
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
25
 Substituição
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
26
Refutação de Resolução
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
27
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
28
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
29
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
30
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
31
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
32
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
33
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
34
Resultados de Completude
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
36
Exercícios
Aulas de Lógica Aplicada a Computação - Aquiles Burlamaqui
37
 Exercícios 
Referencias
 Callejas, Bedregal. Acióly, Bendito. Lógica para a 
Ciência da Computação, Natal, 2001.
 http://pt.wikipedia.org/wiki/L%C3%B3gica
 http://www.pucsp.br/~logica/