LÓGICA APLICADA A COMPUTAÇÃO - Aquiles...

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/