Apostila de Lgica

Prof. Mrio Benevides

mario@cos.ufrj.br

19 de Maro de 2015

UFRJ

Motivao Prtica

lgebra de Boole

Programao em lgica (PROLOG)

Sistemas especialistas

Especificao de programas

Verificao de programas

Banco de dados:

BDs dedutivos

Hiptese de mundo fechado

Default / prioridades

Ontologias

Sistemas distribudos:

Tempo

Conhecimento e crena

Lei (Lgica dentica)

Linguagens de programao

Livros

Lgica para a Computao - Thomson Learning - Flvio Soares Corra da

Silva, Marcelo Finger e Ana Cristina Vieira de Melo

Lgica para a Cincia da Computao - Ed. Campus - Joo Nunes de Souza

A Mathematical Introduction to Logic - Enderton

Introduction to Mathematical Logic - Mendelson

Introduo Lgica Modal Aplicada a Computao - Marcos Mota Costa

Programao em Lgica e a Linguagem PROLOG - Casanova

Lgica - John Nolt e Linnes Rohatyn

Sumrio

1 Introduo 1

2 Lgica Clssica Proposicional 5

2.1 Linguagem da Lgica Clssica Proposicional . . . . . . . . . . . . . . 6

2.2 Semntica da Lgica Clssica Proposicional . . . . . . . . . . . . . . 9

2.3 Complexidade . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

2.4 Sistemas Dedutivos . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

2.4.1 Deduo Natural . . . . . . . . . . . . . . . . . . . . . . . . . 26

rvores de Prova . . . . . . . . . . . . . . . . . . . . . . . . . 37

2.4.2 Mtodo de Tableaux . . . . . . . . . . . . . . . . . . . . . . . 38

2.4.3 Mtodo de Resoluo . . . . . . . . . . . . . . . . . . . . . . . 41

2.4.4 Provador de Dov Gabbay . . . . . . . . . . . . . . . . . . . . . 43

2.4.5 Sistema Axiomtico . . . . . . . . . . . . . . . . . . . . . . . . 48

2.4.6 Relaes entre Sintaxe e Semntica . . . . . . . . . . . . . . . 52

2.5 Aplicao . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58

3 Logica Clssica de Primeira Ordem 61

3.1 Linguagem da Lgica Clssica de Primeira Ordem . . . . . . . . . . . 62

SUMRIO iv

3.2 Sistemas Dedutivos . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67

3.3 Deduo Natural . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70

3.4 Mtodo de Tableaux . . . . . . . . . . . . . . . . . . . . . . . . . . . 72

3.5 Mtodo Axiomtico . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74

3.6 Semntica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77

3.7 Relao entre Sintaxe e Semntica . . . . . . . . . . . . . . . . . . . . 89

3.8 Tabelas - SQL Lgica . . . . . . . . . . . . . . . . . . . . . . . . . 90

3.9 Estruturas e Teorias . . . . . . . . . . . . . . . . . . . . . . . . . . . 94

Grafos, Ordens e rvores . . . . . . . . . . . . . . . . . . . . . 94

Teoria dos Nmeros . . . . . . . . . . . . . . . . . . . . . . . . 97

4 Lgicas Modais 100

4.1 Linguagem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100

4.1.1 Alfabeto modal sobre . . . . . . . . . . . . . . . . . . . . . 100

4.1.2 Linguagem modal induzida pelo alfabeto modal sobre . . . 101

4.2 Semntica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101

4.2.1 Frames . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101

4.2.2 Modelos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102

4.2.3 Satisfao . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103

4.2.4 Clsses de Frames . . . . . . . . . . . . . . . . . . . . . . . . . 106

Clsse dos Frames Reflexivos Fr . . . . . . . . . . . . . . . . . 106

Clsse dos Frames Simtricos Fs . . . . . . . . . . . . . . . . . 107

Clsse dos Frames Transistivos Ft . . . . . . . . . . . . . . . . 107

SUMRIO v

Clsse dos Frames Seriais Fserial . . . . . . . . . . . . . . . . . 108

Captulo 1

Introduo

LGICA o estudo do raciocnio dedutivo.

2

Histrico

Aristteles leis do discurso;

Idade Mdia lgica filosfica;

Boole (1815-1864) lgebra booleana;

Peano (c.1865) axiomatizao da aritmtica;

Frege (1874)

investigar fundamentos da matemtica

lgica moderna;

Russel-Whitehead (1910)

Princpia Matemtica

lgica moderna;

Hilbert (1925)

formalizao da noo de prova

mecanizao da matemtica;

Gentzen (1935) teoria da prova;

Godel (1931-1935)

completude da lgica

incompletude da aritmtica;

Investigar Fundamentos da Computao.

3

O que lgica?

o estudo do raciocnio dedutivo. (informalmente);

um sistema formal (formalmente)

Lgica:

LINGUAGEM

+

REGRAS DE DEDUO / INFERNCIA

+

SEMNTICA

Linguagem

usada para descrever o conhecimento que se deseja representar.

Regras de Deduo

Servem para tirar concluses a partir do conhecimento representado na lingua-

gem.

Semntica

Serve para dar significado aos objetos descritos na linguagem.

4

Tipos mais comuns de lgica:

Lgica Clssica Proposicional

Lgica Clssica de 1a Ordem

Lgicas Modais: tempo, conhecimento, aes, pogramas e etc.

Lgicas Paraconsistente;

Lgicas Relevantes;

Lgicas Difusas;

Lgicas Probabilistcas.

Hipteses da Lgica Clssica:

proposices atmicas;

proposies mais complexas podem ser (construdas decompostas) de (em)

proposies atmicas;

proposies atmicas so verdadeiras ou falsas (2 valores);

o valor verdade de uma proposio mais complexa somente depende dos valores

das proposies atmicas que a compe.

Ex1: Joo ama Maria. (V ou F)

Ex2: Joo estudante e Joo alto.

o valor verdade s depende de sabermos se:

Joo estudante. (V ou F?)

Joo alto. (V ou F?)

Captulo 2

Lgica Clssica Proposicional

Neste captulo ns apresentaremos a Lgica Clssica Proposicional. Na seo 2.1

ns definimos a linguagem. Na seo 2.2 ns apresentamos a semntica e definimos

a importante noo de conseguncia lgica. Na seo 2.3 apresentamos algoritmos

para verificar conseguncia lgica e satisfabilidade e discutimos a complexidades des-

tes problenas. Na seo 2.4 so apresentados alguns sistemas dedutivos. Finalmente,

na seo 2.4.6, enunciamos e provamos os teoremas de Correo e Completude da

Lgica Clssica Proposicional.

2.1 Linguagem da Lgica Clssica Proposicional 6

2.1 Linguagem da Lgica Clssica Proposicional

A linguagem proposicional uma linguagem formal cujo objetivo representar

trechos de discurso de uma maneira precisa e sem ambigidades. Os seguintes opera-

dores sero usados para formar proposies mais complexas a partir de proposies

mais simples:

e

ou

se ento

no

Para representar proposies atmicas usaremos letras maisculas, por exem-

plo: A, B, C,...

Exemplos A B,A B,A B,A

Scrates um homem.

Se Scrates um homem ento Scrates mortal.

AScrates um homem.

BScrates mortal.

A

A B

2.1 Linguagem da Lgica Clssica Proposicional 7

Definio

Um alfabeto proposicional composto por trs conjuntos de smbolos:

Conectivos/operadores lgicos: ,,,

Smbolos auxiliares: ( e )

Smbolos proposicionais: qualquer letra maiscula um smbolo proposi-

cional (ex: A, B,..., Z).

Podemos acrescentar um subscrito numrico a letras maisculas (A1, A2, ...).

Denotamos este conjunto por P.

Apresentaremos a seguir uma gramtica para definirmos quais so as frmulas

bem formadas da linguagem:

Definio A noo de frmula bem formada, ou simplesmente frmula, definida,

indutivamente, pelas seguintes condies:

Qualquer smbolo proposicional uma frmula.

Se e so frmulas ento ( ), ( ),, ( ) tambm o so;

Nada mais frmula

De uma forma alternativa podemos definir a linguagem proposicional por meio

de uma notao BNF.

::= P | (1 2) | (1 2) | (1 2) |

onde P um smbolo proposicional.

Algumas vezes utilizamos o conectivo se e somente se que definido como:

( ) (( ) ( ))

Exemplo e frmulas bem formadas:

2.1 Linguagem da Lgica Clssica Proposicional 8

A B (no frmula)

(A) (B) (no frmula)

(A B) (B C) D (no frmula)

((A (B A)) (A B)) ( frmula)

(A (B C)) ( frmula)

Exerccios:

Questo 1. Represente as seguintes proposies utilizando a linguagem da lgica

clssica proposicional. Utilize os smbolos proposicionais C (est chovendo) e N (est

nevando).

(a) Est chovendo, mas no est nevando.

(b) No o caso que est chovendo ou nevando.

(c) Se no est chovendo, ento est nevando.

(d) No o caso que se est chovendo ento est nevando.

(e) Est chovendo se e somente se est nevando.

(f) Se est nevando e chovendo, ento est nevando.

(g) Se no est chovendo, ento no o caso que est nevando e chovendo.

Nos exerccios seguintes, represente o texto na linguagem da lgica proposicional,

especificando significado dos smbolos proposicionais utilizados.

Questo 2. Ela no est em casa ou no est atendendo ao telefone. Mas se ela

no est em casa, ento ela foi seqestrada. E se ela no est atendendo ao telefone,

ela est correndo algum outro perigo. Ou ela foi seqestrada ou ela est correndo

um outro perigo.

Questo 3. Hoje fim-de-semana se e somente se hoje sbado ou domingo. Hoje

no sbado. Hoje no domingo. Portanto, hoje no um fim-de-semana.

2.2 Semntica da Lgica Clssica Proposicional 9

Questo 4. A proposta de auxlio est no correio. Se os juzes a receberem at

sexta-feira, eles a analisaro. Portanto, eles a analisaro porque se a proposta estiver

no correio, eles a recebero at sexta-feira.

Observao:

Convenes sobre omisso de parnteses:

> > >

Parnteses mais externos podem ser omitidos:

A (B C) (A (B C))

2.2 Semntica da Lgica Clssica Proposicional

A semntica da lgica clssica proposicional consiste na atribuio de signifi-

cado s frmulas da linguagem.

Isto feito atravs da atribuio de valor verdade.

Para cada frmula atribudo um valor verdadeiro ou falso.

valores-verdade:

V - verdadeiro

F - falso

O valor verdade de uma frmula depende unicamente dos valores verdade

atribudos aos seus smbolos proposicionais.

2.2 Semntica da Lgica Clssica Proposicional 10

Tabela Verdade

Conjuno:

A B A B

V V V

V F F

F V F

F F F

Hoje tem aula e hoje quinta-feira.

Disjuno (no-exclusiva):

A B A B

V V V

V F V

F V V

F F F

Hoje tem aula ou hoje quinta-feira.

Negao:

A A

V F

F V

Hoje no tem aula.

Implicao:

Exemplo: considere o anncio abaixo:

Para pagamento vista, ns damos 25% de desconto na compra de qualquer TV.

Re-escrevendo:Se pagamento vista ento 25% de desconto.

Suponha agora que D. Maria deseja verificar se este anncio honesto ou no.

2.2 Semntica da Lgica Clssica Proposicional 11

Possibilidade Pagamento vista 25% de desconto Anncio

1 V V V

2 V F F

3 F V V

4 F F ?

A B A B

V V V

V F F

F V V

F F V(?)

Existem lgicas que discordam da linha 4 Ex: 3-valores, intuicionista, relevante...

Exerccio:

Construa a tabela verdade de: (A B) C

A B C A (A B) (A B) C

V V V

V V F

V F V

V F F

F V V

F V F

F F V

F F F

2.2 Semntica da Lgica Clssica Proposicional 12

Funo de Atribuio de Valor Verdade

A cada smbolo proposicional ns queremos atribuir um valor verdadeiro ou falso.

Isto feito atravs de uma funo v de atribuio de valor verdade. v:P 7 {V, F},

onde P conjunto dos smbolos proposicionais

Exemplos:v(A) = F , v(B) = V , v(C) = V

Uma vez atribudo valor verdade a cada smbolo proposicional em P, queremos

estender esta atribuio para o conjunto de todas as frmulas da linguagem propo-

sicional, que denotaremos por W . Na definio a seguir e denotam frmulas e

A denota um smbolo proposicional, isto , , W e A P.

Definimos uma funo v de atribuio de valor verdade a frmulas da linguagem

como uma extenso da funo v tal que:

v : W 7 {V, F}, onde v deve satisfazer as seguintes condies:

1. v(A) =v(A), seA P

2. v() =

V se v() = F

F se v() = V

3. v( ) =

V se v() = v() = V

F caso contrrio

4. v( ) =

F se v() = v() = F

V caso contrrio

5. v( ) =

F se v() = V e v() = F

V se caso contrrio

2.2 Semntica da Lgica Clssica Proposicional 13

Exemplo: Ache o valor verdade da seguinte frmula para a valorao

v(A) = V, v(B) = F, v(C) = F :

v(A (B C)) = V

uu

**

v(A) = V

v((B C)) = V

tt

))

v(A) = V v(B) = F

v(C) = V

v(B) = F v(C) = F

v(C) = F

Exemplo: Ache o valor verdade da seguinte frmula para a valorao

v(A) = F, v(B) = F,v(C) = V, v(D) = V :

v((A D) (C B)) = V

rr

++

v((A D)) = F

))

v((C B)) = F

ss

v(A) = F

v(D) = F

v(C) = F

v(B) = F

v(A) = F v(D) = V

v(C) = V

v(B) = F

v(D) = V v(C) = V

2.2 Semntica da Lgica Clssica Proposicional 14

Algoritmo para Construir Tabela Verdade

Quantas linhas possui uma tabela verdade para (A D) (C B) ?

Cada linha corresponde a uma possvel atribuio de valores verdade aos sm-

bolos proposicionais que compe a frmula. Como esta frmula possui 4 smbolos

proposicionais (A,B,C e D), sua tabela verdade deve ter 24 = 16 linhas.

Tabela Verdade computa o valor verdade de uma frmula para todas as possveis

atribuies v a seus smbolos proposicionais.

Logo, o problema de se saber todos os valores verdades de uma frmula na lgica

clssica proposicional, para todas as atribuies v a seus smbolos proposicionais,

decidvel; o algoritmo o seguinte:

passo 1: conte o nmero de smbolos proposicionais;

passo2: monte uma tabela com 2n linhas e com quantas colunas for o nmero de

subfrmulas da fmula;

passo 3: preencha as colunas dos smbolos proposicionais com V ou F alternando

de cima para baixo VFVF para a 1a coluna, VVFF... para a 2a, VVVVFFFF para

a 3a e assim por diante, nas potncias de 2.

passo 4: compute o valor verdade das outras colunas usando as tabelas bsicas

fornecidas.

2.2 Semntica da Lgica Clssica Proposicional 15

Exemplo: (A B) C

23 = 8

A B C A (A B) (A B) C

V V V F V V

V V F F V V

V F V F V V

V F F F V V

F V V V V V

F V F V V V

F F V V F V

F F F V F F

Tautologias, Contradies, Frmula Equivalentes

Existem frmulas onde todas as linhas da Tabela Verdade do verdade. Elas so

verdadeiras no importando os valores verdade que atribumos aos seus smbolos

proposicionais. Estas frmulas so chamadas tautologias. Da mesma forma, exis-

tem frmulas que so sempre falsas, independente dos valores verdade atribudos

aos seus smbolos proposicionais. Estas so chamadas contradies. Alm disso,

existem frmulas que, embora diferentes, tm tabelas verdade que coincidem linha

a linha. Tais frmulas so ditas equivalentes.

Exemplos:

A A A

V V

F V

A A uma tautologia.

2.2 Semntica da Lgica Clssica Proposicional 16

A B B A A (B A)

V V V V

V F V V

F V F V

F F V V

A B (B A) (A B) A (A B)

V V V F F

V F V F F

F V V F F

F F F V F

A (A B) uma contradio.

A B B A (A B)

V V V F

V F F V

F V F V

F F F V

A B A B A B

V V F F F

V F F V V

F V V F V

F F V V V

(A B) equivalente a A B.

2.2 Semntica da Lgica Clssica Proposicional 17

Definio 1 Tautologia e Contradio:

Uma frmula uma tautologia se e somente se, para toda atribuio v,

v() = V .

Uma frmula uma contradio se e somente se, para toda atribuio v,

v() = F .

Exemplos de tautologias famosas:

A A

A A

(A ((A B) B)

A B A

A B B

A A

A A B

B A B

((A B) B) A

Exemplos de contradies:

A A

(A A)

A (A B) B

Exerccio

Verificar se estas frmulas so realmente tautologias e contradies.

2.2 Semntica da Lgica Clssica Proposicional 18

Definio 1 Equivalncia entre Frmulas:

Duas frmulas e so ditas equivalentes, , se e somente se, para toda

atribuio v, v() = v().

Intuitivamente, duas frmulas so equivalentes se, linha a linha, elas tem a mesma

tabela verdade.

Exemplos de equivalncias:

A A

(A B) A B

Exerccio: Verificar se as seguintes frmulas so equivalentes:

1. (A B) A B

2. (P Q) (P Q)

3. P (Q R) (P Q) (P R)

4. P Q Q P

5. P (Q R) (P Q) (P R)

Observao:

Utilizando a noo de equivalncia, possvel definir alguns dos conectivos a par-

tir de outros. Por exemplo, utilizando a negao () e mais um conectivo qualquer

( , ou ) podemos definir todos os outros. Assim:

Definimos e usando e

P Q P Q

P Q (P Q)

Definimos e usando e

P Q (P Q)

2.2 Semntica da Lgica Clssica Proposicional 19

P Q (P Q)

Definimos e usando e

P Q (P Q)

P Q P Q

Exerccio: Verificar as equivalncias acima.

Na verdade todos os conectivos podem ser definido a partir de um nico novo

conectivo chamado. Isto o que vamos ver no exerccio seguinte.

Exerccio: (Sheffer Stroke P/Q)

Suponha P/Q uma frmula com a seguinte Tabela Verdade

P Q P/Q

V V F

V F F

F V F

F F V

Defina ,,, usando / Dica: P (P/P)

P P P/P

V F F

F V V

2.2 Semntica da Lgica Clssica Proposicional 20

Dada uma tabela verdade, como saber a frmula correspondente?

P Q R S

V V V V V

F V V V V

V F V V V

F F V V F

V V F V F

F V F V F

V F F V F

F F F V F

V V V F F

F V V F F

V F V F F

F F V F F

V V F F F

F V F F F

V F F F F

F F F F F

Linhas em que verdadeira:

P Q R S

V V V V V

F V V V V

V F V V V

Logo:

P Q R S

P Q R S

P Q R S

2.2 Semntica da Lgica Clssica Proposicional 21

(P Q R S) (P Q R S) (P Q R S)

Formalizando: Para achar a frmula correspondente a uma tabela verdade, pro-

cedemos da seguinte maneira:

1. Para cada linha da tabela verdade em que a frmula verdadeira, escrevemos

uma frmula correspondendo conjuno ( E ) dos smbolos proposicionais

que forem verdadeiros e das negaes daqueles que forem falsos na linha con-

siderada.

2. A frmula a disjuno ( OU ) das frmulas escritas no passo 1.

Definio 1 tomo e Literal

Uma frmula atmica ou tomo qualquer smbolo proposicional. Ex: A, e

C.

Um literal um tomo ou sua negao. Ex: A,A,B,C.

Forma Normal Disjuntiva(FND):

Uma frmula est na forma normal disjuntiva se e somente se tem a seguinte

forma:

= C1 C2 ... Cn

onde cada Ci = (Q1 Q2 ... Qm), 1 i n, e Qj , 1 j m, so literais,

isto , cada Ci uma conjuno de literais. E um disjuno de conjunes de

literais.

2.2 Semntica da Lgica Clssica Proposicional 22

Forma Normal Conjuntiva(FNC):

Uma frmula est na forma normal conjuntiva se e somente se tem a seguinte

forma:

= D1 D2 ... Dn

onde cada Di = (Q1 Q2 ... Qm), 1 i n e Qj, 1 j m, so literais,

isto , cada Di uma disjuno de literais. E um conjuno de disjunes de

literais.

Algoritmo: Converter frmulas para a FNC:

passo1: elimine o conectivo usando:

( )

( ) ( )

passo 2: mova a negao () para o interior da frmula, usando as seguintes regras:

( ) ( )

( ) ( )

passo3 : mova as conjunes para o exterior da frmula usando:

( ) ( ) ( )

( ) ( ) ( )

Exemplo:

(A B) C passo1 (A B) C passo2

(A B) C passo3 (A C) (B C) FNC

Exerccio:

Fazer um algoritmo para converter frmulas para a forma normal disjuntiva.

2.2 Semntica da Lgica Clssica Proposicional 23

Definio:

Seja uma frmula e um conjunto de frmulas:

1. Uma atribuio de valor verdade v:P 7 {V, F} satisfaz se e somente se

v() = V . E v satisfaz se e somente se v satisfaz cada membro de .

2. satisfatvel se e somente se existe uma atribuio v que satisfaz . Caso

contrrio, insatisfatvel.

Definio:

Uma frmula dita uma consequncia logica de um conjunto de frmulas

= {1, 2, ..., n}, ou uma implicao logica de , 1, 2, ..., n |= , se

somente se para toda valorao v se v(1 2 ... n) = V , ento v() = V .

Teorema:

Uma frmula dita uma consequncia logica de um conjunto de frmulas

= {1, 2, ..., n}, ou seja, 1, 2, ..., n |= se somente se (12 ...n)

uma tautologia.

Exemplo:

(C T ) T C tautologia (C T ) T |= C

2.3 Complexidade 24

2.3 Complexidade

Nesta seo gostariamos de investigar dois problemas distintos:

Problema 1: Dada uma frmula com comprimento n e uma valorao v para

os smbolos proposicionais. Qual a complexidade de se calcular o valor de v() para

a atribuio v? Calcular (,v).

Onde o comprimento de uma frmula o nmero de smbolos da frmula, i.e.,

numero de smbolos proposicionais + nmero de conectivos lgicos.

A seguir especificamos uma funo (,v) que implementa a funo v() para a

atribuio v.

Funo (,v): bool

caso

= P onde P um smbolo proposicional, retorna v(P );

= 1, retornar NOT (1,v);

= 1 2, retornar (1,v) AND (2,v);

= 1 2, retornar (1,v) OR (2,v);

= 1 2, retornar NOT (1,v) OR (2,v);

Complexidade da funo (,v) O(n), pois a funo chamada uma vez para

cada smbolo proposicional e uma vez para cada conectivo lgico.

2.3 Complexidade 25

Problema 2: Dada uma frmula com comprimento n e m smbolos proposi-

cionais. Verificar se existe alguma valorao que satisfaz .

Funo SAT(): bool

para cada valorao v faa

se (,v) ento retorna verdadeiro

retorna falso

Complexidade da funo SAT()

Complexidade da funo SAT nmero de valoraes diferentes complexidade

de (,v)

Complexidade da funo SAT O(2m)O(n) O(2m.n)

Obs.:

1) problema 1 polinomial (linear) no comprimento da frmula;

2) problema 2 NP completo.

2.4 Sistemas Dedutivos 26

2.4 Sistemas Dedutivos

Nas sees anteriores apresentamos a linguagem e a semntica da Lgica Clssica

Proposicional. Voltaremos agora a problema central deste curso. Dado Um banco

de dados (conjunto de frmulas), BD = {1, , n}, e uma pergunta (frmula),

com saber se o banco de dados implica logicamente na pergunta.

Ns j temos um algoritmo para responder BD |= montando a tabela verdade

para 1 2 ... n . Se for uma tautologia responde SIM, seno responde

NO.

A complexidade deste algoritmo da ordem de 2n, onde n o nmero de smbolos

proposicionais em 1 2 ... n .

2.4.1 Deduo Natural

Jakowski(1924) e Gentzen(1935)

Somente regras de inferncia

Para cada conectivo lgico temos 2 regras:

1. Regra de Introduo

2. Regra de Eliminao

3. Regra de Introduo: como uma frmula contendo o conectivo pode ser inferida

4. Regra de Eliminao: que consequncias podemos tirar de uma frmula con-

tendo o conectivo

2.4 Sistemas Dedutivos 27

Queremos escrever regras de inferncia que sejam vlidas, isto , que as premissas

impliquem logicamente nas concluses.

Regras de inferncia:

P 1, P 2, ..., P n

C

Se todas as premissas P 1, P 2, ..., P n forem verdadeiras, ento a concluso C

verdadeira.

P 1, P 2, ..., P n C

Exemplo: A seguintes regras so vlidas?

No, pois no implica logicamente , Pois, sempre falso (con-

tradio).

vlida, pois se v() = V e v( ) = V , ento v() = V porque v() = F e

para v( ) = V , v() = V .

Regras de Inferncia:

Primeiro apresentaremos as regras que no utilizam o conceito de suposio para

em seguida introdizir este conceito e apresentar as regras restantes.

Conjuno

-I

2.4 Sistemas Dedutivos 28

Se BD e BD , ento responda sim para . Isto BD .

-I vlida? Sim, pois se v() = v() = V ento v( ) = V

-E

-E vlida? Sim, pois se v( ) = V ento v() = v() = V

Disjuno

-I

vlida? Sim, pois se v() = V ento v( ) = V

-E Esta regra envolve o conceito de suposio que veremos a seguir. Iremos

apresent-la e seguir.

Implicao

E,

Se v() = V e v( ) = V ento v() = V

Exemplo:

quinta-feira

se quinta-feira ento aula de lgica

aula de lgica

2.4 Sistemas Dedutivos 29

Exemplo 1:

1. A B

2.A C

3.C D

BD D

4. A E(1)

5. C E(2,4)

6. D E(3,5)

I Esta regra envolve o conceito de suposio que veremos a seguir. Iremos

apresent-la em seguida.

Negao:

I

E1

Reduo ao Absurdo: Esta regra envolve o conceito de suposio que veremos

a seguir. Iremos apresent-la em seguida.

Exemplo:

BD = {A B} BD A B ?

1. A B

2. A E1(1)

3. A B I(2)

2.4 Sistemas Dedutivos 30

Vamos introduzir agora o impotante conceito de suposio. Informalmente,

uma suposio uma frmula que supomos ser verdadeira para concluirmos algo

que depende desta suposio. Representamos suposies como frmulas entre [...],

por exemplo, [A B].

Vamos comear com dois exemplos.

No meu banco de dados eu tenho uma axiomatizao das leis da Mecanica Cls-

sica e que eu gostaria de estabelecer a seguinta proposio condicional:

Se corpo solto no ar ento corpo cai

BD = leis da Mecanica Clssica

Suponho que o corpo est solto no ar.

Provo, usando esta suposio e as leis do BD que

o corpo cai

Se corpo solto no ar ento corpo cai

Porm, a suposio que o corpo est solto no ar deve ser descartada (descarre-

gada) aps a proposio condicional ter sido estabelecida.

Um segundo exemplo seria:

No meu banco de dados eu tenho uma axiomatizao da Aritmtica e eu gostaria

de estabelecer a seguinta proposio condicional:

Se n impar ento sucessor de n par

BD = axiomatizao da Aritmtica

Suponho que n impar.

Provo, usando esta suposio e as leis do BD que

sucesor de n e par

Se n impar ento sucessor de n par

2.4 Sistemas Dedutivos 31

De novo, temos que descarrgar a suposio que n impar aps a proposio

condicional ter sido estabelecida.

Introduo da

I[]i

...

i

Onde [] uma suposio

Exemplo:

BD = {A C, C D}

Pergunta: A D

BD A D

1. A C BD

2. C D BD

3. [A]1 Suposio

3.1 C E(3,1)

3.2 D E(3.1,2)

4. A D1 I(3,3.2)

Eliminacao da

-E

[]i

...

[]j

...

ij

Exemplo:

2.4 Sistemas Dedutivos 32

Hoje tera-feira Hoje quinta-feira.

Se Hoje tera-feira ento aula de lgica.

Se Hoje quinta-feira ento aula de lgica.

aula de lgica

Exemplo:

BD = {A B, A C, B C}

Pergunta: C

BD C

1. A B BD

2. A C BD

3. B C BD

4. [A]1 Suposio

4.1 C E(4,2)

5. [B]2 Suposio

5.1 C E(5,3)

6. C1,2 E(1,4.1,5.1)

Reduo ao Absurdo:

A seguir apresentamos as duas ltimas regras de Deduo Natural. A regra ABS

introduz o absurdo a patir de uma contradio qualquer . A regra de Ruduo

ao Absudo, RAA, uma regra fundamental de Deduo Natural, sua intuio que

se supusermos a negao do que queremos provar e chegarmos a um absurdo ento

podemos concluir nossa prova dizendo sim para a pergunta.

-RAA -ABS

[]...

Exemplo:

2.4 Sistemas Dedutivos 33

BD = {A C}

Pergunta: (A C)

BD (A C)

1. A C BD

2. [(A C)]1 Suposio

2.1 (A C) E(2)

2.2 A E(2.1)

2.3 C E(2.1)

2.4 C E(2.2,1)

2.5 C C I(2.3,2.4)

2.6 ABS(2.5)

3. (A C)1 RAA I(2,2.6)

2.4 Sistemas Dedutivos 34

A seguir apresentamos todas as regras de deduo Natural.

Deduo Natural para a Lgica Proposicional Clssica

-I -E

-I -E

[]i

...

[]j

...

ij

-I -E

[]i

...

i

-I -E

-RAA -ABS

[]i

...i

2.4 Sistemas Dedutivos 35

Definio:

1. Uma prova em deduo natural de uma formula a partir de um conjunto de

frmulas BD={1, 2, ..., k} uma sequncia de frmulas rotuladas da seguinte

forma:

i. as frmulas do BD formam o prefixo da sequncia e so rotuladas 1: 1, 2:

2, ..., k: k;

ii. se a ltima frmula da sequncia .r: i (onde pode ser a sequncia vazia),

ento a prxima frmula rotulada ser:

ii.1 .r.1: j se i uma suposio;

ii.2 .r+1: j se j foi obtida pela aplicao de regras do grupo I a frmulas no

escopo igual superior a , onde = .r;

ii.3 .s+1: j se j foi obtida pela aplicao das regras do grupo II e = .s;

iv. n: a ltima frmula da sequncia.

2. A frmula dita um teorema do conjunto de frmulas BD, BD .

3.A frmula dita um teorema lgico se BD vazio.

OBS: Uma prova pode ser chamada algumas vezes de derivao.

Definio:

1. Um conjunto de frmulas = {1, 2, ..., n} inconsistente se somente

se para alguma frmula .

2. Um conjunto de frmulas = {1, 2, ..., n} consistente se somente se

ele no inconsistente.

2.4 Sistemas Dedutivos 36

Notao:

Ns abreviaremos:

por ,

por

Exerccios:

Prove por deduo natural as seguintes afirmaes:

1. BD = {A B C,A B,C D } ; BD A D ?

2. (P Q) (Q P ) ?

3. Q P Q ?

4. P Q R (P Q) (P R) ?

5. P (Q R) (P Q) R ?

6. P Q (P Q) ?

7. P Q R P (Q R) ?

8. B,R S A,R S,A R C,B S C C ?

9. (P Q) (Q R) P R ?

10. P R,Q S P Q R S ?

11. A B, (A B) (R S), (P Q) R,A P Q S ?

12. P Q,Q P ?

13. (P Q) Q,Q P P ?

14. (P Q) P Q ?

2.4 Sistemas Dedutivos 37

rvores de Prova

A forma mais usual de se representar provas em Deduo Natural usando-se

rvores de prova. Informalmente, uma rvore de prova uma rvore finita na qual

na raiz temos a frmula que queremos provar e nas folhas temos as suposies e

frmulas do banco . Cada suposio tem um nmero, e se este nmero aparece

na aplicao de uma regra de inferncia significa que a suposio foi descarregada.

Cada n intermedirio obtido, como concluso, pela aplicao de uma regra de

inferncia aos seus filhos, que so as premissas da regra1.

Ns dizemos que uma frmula segue de um banco de dados (conjunto de

frmulas) , , se existe uma rvore de prova com na raiz e todas as frmulas

de so exatamente a nicas siposies que no foram descarregadas.

Exemplo 2.4.1 : (A (B C)) (A B).

[(A (B C))]1 [A]2

(B C)

B(A B)2

((A (B C)) (A B))1

Exemplo 2.4.2 (A B) (A B).

[(A B)]3

A BB

[A B]2

[(A B)]1

A BA

BB B

(A B)1,3

Exerccios: Faa todos os exerccios do final da seo anterior colocando as

provas em forma de rvores de prova.

1 importante observar que a rvore de prova desenhada com a raiz embaixo e as folhas esto

em cima. Isto no usual em Computao

2.4 Sistemas Dedutivos 38

2.4.2 Mtodo de Tableaux

As dedues so feitas por refutao, i.e., se queremos deduzir a partir de um

banco de frmulas BD, BD , partimos da negao de e tentamos chegar no

absurdo. As dedues tm forma de rvore.

A seguir apresentamos todas as regras de de Tableaux.

Tableaux para a Lgica Proposicional Clssica

R1 R2

R3 R4

R5 R6

( )

( )

R7

( )

2.4 Sistemas Dedutivos 39

Motivao

Se aplicarmos as regras a uma frmula, vamos gerar uma rvore, onde cada ramo

corresponde a uma ou mais valoraes que satisfazem a frmula, por isso chamado

Tableau Semntico.

Lembrando do nosso mtodo semntico para verificar consequncia lgica, i.e.,

dado um BD = {1, , n} e uma pergunta , temos que BD |= se e somente se

(1 n) uma tautologia. Mas verificar se esta frmula uma tautologia

equivalente a verificar se sua negao uma contradio. A intuio do mtodo

de Tableaux aplicar as regras para mostrar que ((1 n) ) no possui

nenhuma valorao que a faa verdadeira, i.e., ela uma contradio. E portanto,

(1 n) uma tautologia.

Definio: Um ramo de um tableaux dito fechado se ele contiver e

para qualquer frmula .

Definio: Um tableaux dito fechado se cada um dos seus ramos for fechado.

E aberto caso contrrio.

Mtodo

1. O ramo inicial deve conter todas as frmulas do BD seguidas da negao da

pergunta;

2. aplique as regras as frmulas no mesmo ramo no mximo uma vez;

3. se o tableaux fechar responda SIM;

4. se , em todos os ramos, todas as frmulas j foram usadas uma vez e mesmo

assim o tableaux no fechou responda NO.

Exemplo 1: {A B, B C} A C

2.4 Sistemas Dedutivos 40

BD A B

BD B C

Neg. perg. (A C)

R7

A

CR3

%%

R3

vv

BR3

''PPP

PPPP

PPPP

PPPP

R3

yysssssssssss

C

A B

Exemplo 2: A B (A B)

BD A B

Neg. perg. (A B)

R4

(A B)

R1

A

BR2

&&

R2

vv

A B

Este tableaux fechado, pois todas as valoraes so contraditrias, logo A B

e (A B) no satisfatvel.

Teorema (Completude): se BD |= ento existe tableaux fechado para BD, .

Teorema (Correo): se existe um tableaux fechado para BD, ., ento BD |= .

2.4 Sistemas Dedutivos 41

O mtodo de Tableaux refutacionalmente completo.

Exerccios:

1. A B,(A B) (C A)

2. (P Q),(P Q) P

3. Guga inteligente. Guga determinado. Se Guga determinado e atleta

ento ele no um perdedor. Guga atleta se ele amante do tnis. Guga

amante do tnis se inteligente. Guga no um perdedor?

4. (P (R Q)), (P R) (P Q)

5. A B,(B C), C D A D

2.4.3 Mtodo de Resoluo

Passo 1: Passar o BD para FNC e quebrar os comjunes em Clusulas;

Passo 2: Negar a pergunta, pass-la para FNC e quebrar os comjunes em Clu-

sulas;

Passo 3: Juntas as clusulas obtidas nos passos 1 e 2 e aplicar as regras at obter

a clusula vazia (contradio).

Regras de Resoluo

L1, , Li, , Li+1, , Ln M1, Mj ,,Mj+1, ,MkL1, Ln,M1, ,Mk

L1, , Li, , Li+1, , Lj , Lj+1, , LnL1, , Li, , Li+1, , Lj , Lj+1, , Ln

Exemplo 1:

BD = {A B, A C, B C}

Pergunta: C

2.4 Sistemas Dedutivos 42

BD C

Negando a pergunta e transformando a pergunta negada e o BD em clusulas

temos:

1. A B BD

2. A C BD

3. B C BD

4. C Negao da pergunta

5. B (3,4)

6. A (2,4)

7. A (5,1)

8. (6,7)

Exemplo 2:

BD = {A B, A B, B A}

Pergunta: A B

BD A B

Negando a pergunta e transformando a pergunta negada e o BD em clusulas

temos:

1. A B BD

2. A B BD

3. B A BD

4. A B Negao da pergunta

5. B B (3,4)

6. B (5)

7. A (6,1)

8. A (6,2)

9. (7,8)

O mtodo de Resoluo refutacionalmente correto e completo. Dado um banco

de dados BD e uma pergunta . Seja o conjunto de clusulas resultante da

2.4 Sistemas Dedutivos 43

transformao do BD e de .

Correo: se Res ento BD |=

Completude: se BD |= ento Res

2.4.4 Provador de Dov Gabbay

Um provador automtico de teoremas dirigido pelo objetivo. Isto , parte da

negao da pergunta.

Objetivo: Dado um banco de dados e uma pergunta (objetivo) , ns quere-

mos responder SIM ou NO para o caso da pergunta seguir ou no do banco

de dados.

2 Mtodos at o momento:

Tabela Verdade BD |= (semanticamente);

Regras de Deduo Natural BD (sintaticamente).

Tabela Verdade mecnico mas pouco eficiente.

Deduo Natural requer criatividade.

Nosso objetivo: Responder BD automaticamente.

Provador Automtico de Teoremas Dirijido pelo Objetivo(pergunta) :

Linguagem:

2.4 Sistemas Dedutivos 44

Linguagem a linguagem da lgica clssica proposicional com , e o smbolo

(absurdo). Ns escreveremos a .

Ns chamamos de clusulas as formulas que podem ocorrer no banco de dados e

objetivo as frmulas que resultam da pergunta.

Definio: Clusula, Objetivo e Banco de Dados.

(i) Qualquer tomo (smbolo proposicional) , incluindo , uma clusula e

tambm um objetivo.

(ii) Se um objetivo e q um tomo, ento q uma clusula e tambm

um objetivo.

(iii) Se 1 e 2 so objetivos, ento 1 2 tambm um objetivo.

(vi) Um banco de dados BD um conjunto de clusulas.

(v) Nenhuma frmula uma clusula a no ser as definidas em (i),(ii),(iii) e (vi).

Resumindo:

Clusula Objetivo

q ou (tomos) q ou (tomos)

q q

- 1 2

Transformao de frmulas em Clusulas e Objetivos:

1. ()

2. ()

3. ( ) ( )

4. ( ) ( ) ( )

2.4 Sistemas Dedutivos 45

5. Se na transformao do BD obtenho 12...n , ns colocamos 1, 2, ..., n

no BD.

Exemplo:

A B B C

(A) B B C (Regra 1)

(A) ) B B C (Regra 2)

(((A) ) B B) (((A) ) B C) (Regra 4)

Toda frmula da lgica proposicional equivalente (pode ser traduzida) a uma

conjuno de clusulas.

Problema Original: BD0 0?

Problema Transformado: BD ?

Regras de Computao:

1. Provar BD , prove BD e BD .

2. Provar BD , prove BD, . Se for uma conjuno =

1 2 ... n, adicione a BD 1, 2,..., n.

3. Provar BD q, onde q um tomo, temos 4 casos:

3.1. q BD, responda SIM.

3.2. BD, responda SIM.

3.3. q BD, pergunte BD .

3.4. BD, pergunte BD .

4. Regra do Reincio (restart)

2.4 Sistemas Dedutivos 46

Nosso problema inicial era mostrar BD . No meio da computao, ns es-

tamos perguntando BD . Se no conseguimos prosseguir deste ponto, podemos

perguntar qualquer pergunta j feita no mesmo ramo, por exemplo , ao banco

de dados atual, isto , BD e continuar a prova.

5. Checagem de LOOP: Nunca pergunte BD pela 2a vez para ao mesmo

BD e mesmo .

Exemplos:

(1) (A B,B C), A C (A B), (B C), A B Regra (3.3) (A

B), (B C), A A Regra (3.3) SIM ! Regra (3.1)

Figura 2.1:

2.4 Sistemas Dedutivos 47

Figura 2.2:

2.4 Sistemas Dedutivos 48

Figura 2.3:

Execcios:

(1) (A B) B (B A) A

(2) (A B) B A B

(3) (A A) A

(4) (A B) (C A) (C B)

(5) A A B

(6) A B,B A

(7) A (A B)

(8) (A B) C A (B C)

2.4.5 Sistema Axiomtico

Outro sistema dedutivo.

2.4 Sistemas Dedutivos 49

Mais antigo e mais utilizado para fins tericos.

Vrios axiomas e uma nica regra de inferncia.

Sejam , e frmulas quaisquer da linguagem proposicional.

Axiomas Lgicos:

Implicao:

(1) ( )

(2)( ( )) (( ) ))

Conjuno:

(3) ( )

(4) ( )

(5) ( ( ))

Disjuno:

(6)

(7)

(8) (( ) )) (( ) )

Negao:

(9)

(10)

(11) ( ) (( ) )

Regra de Inferncia:

2.4 Sistemas Dedutivos 50

Modus Pones (M.P.)

Nosso clculo dedutivo possui um conjunto infinito de axiomas lgicos. Para

cada frmula , e , ns temos axiomas diferentes.

(1),...,(11) so chamadas de axiomas esquema.

A nica regra a Modus Pones (M.P.).

Definio:

Uma frmula dita um teorema de um conjunto de frmulas ( ) se e

somente se existe uma seqncia de frmulas 1, ..., n tal que n = e cada i :

(i) uma instncia de um axioma esquema;

(ii) ou for obtida por M.P. aplicada a l e k e l, k < i.

(iii) ou um membro de .

A seqncia de frmulas 1, ..., n chamada de uma prova de a partir de .

Exemplos:

(1) = {A B,A C} C D ?

1. A B A axioma 3

2. A B

3. A M.P.(1,2)

4. A C

5. C M.P.(3,4)

6. C (C D) axioma 6

2.4 Sistemas Dedutivos 51

7. C D M.P.(5,6)

(2) A A

1. A ((A A) A) axioma 1

2. (A ((A A) A)) ((A (A A)) (A A)) axioma 2

3. (A (A A)) (A A) M.P.(1,2)

4. A (A A) axioma 1

5. A A M.P.(4,3)

Exerccios:

Provar usando o Mtodo Axiomtico:

1) A B,B C A C

2) (A B) C A (B C)

3) A (B C) (A B) (A C)

Observao: importante notar ( e possvel provar ) que os todos mtodos dedu-

tivos estudados para a lgica clssica proposicional so equivalentes, ou seja, uma

frmula que pode ser provada utilizando um deles, sempre poder ser provada utili-

zando qualquer dos outros. Isso importante, na medida em que nos permite provar

uma determinada propriedade dos sistemas dedutivos em geral, provando-a apenas

para o mtodo axiomtico, que embora difcil de ser usado na prtica para provar

um teorema, bastante simples no que diz respeito sua construo, o que facilita

a demonstrao de propriedades tericas, como a completude e a corretude, que

veremos na prxima seo.

2.4 Sistemas Dedutivos 52

2.4.6 Relaes entre Sintaxe e Semntica

Uma das aspectos mais importantes da lgica proposicional a maneira como a

sintaxe se relaciona com a semntica.

SEMNTICA SINTAXE

Valor verdade prova/deduo

valida teorema

implica logicamente |=

tabela verdade clculo dedutivo

Ns queremos relacionar o fato de uma frmula ser um teorema de um conjunto

de frmulas ( ) com a propriedade de implicar logicamente em ( |= ).

Teorema da Corretude

Tudo que o clculo dedutivo prova semanticamente vlido.

Se ento |=

Se uma frmula provada a partir de um conjunto de frmulas ento ela

logicamente implicada por este conjunto de frmulas.

Este teorema nos assegura que tudo que provamos no sistema dedutivo correto

em relao semntica. Isto , nosso sistema dedutivo s prova teoremas que

semanticamente esto corretos.

Como se prova:

1) Prova-se que os axiomas do clculo dedutivo so semnticamente vlidos, isto

, so tautologias;

2) Prova-se que as regras de inferncia sempre derivam concluses verdadeiras a

partir de premissas verdadeiras.

2.4 Sistemas Dedutivos 53

Teorema da Completude

Tudo que semnticamente vlido provado pelo clculo dedutivo.

Se |= ento

Se implica logicamente em ento existe uma prova de a partir de no

sistema dedutivo.

O sistema dedutivo completo em relao semntica pois para toda frmula

que logicamente implicada por existe uma prova a partir de no sistema

dedutivo.

Tudo que semanticamente obtido pode ser tambm obtido no sistema dedutivo.

|= conseqncia lgica de

Toda atribuio de valores verdade que satisfaz tambm satisfaz .

Sendo = { 1, ..., n }

Quero provar que se |= (1 ... n) ento (1 ... n)

A maneira mais usual de se provar Completude usando-se a tcnica de modelo

cannico:

Modelo Cannico

A tcnica do modelo cannico se baseia numa propriedade da Lgica Proposicio-

nal que provar Completude equivalente a provar que qualquer conjunto consistente

satisfatvel. Enunciaremos e provaremos este fato a seguir:

Se |= ento

m

Se {} consistente ento { } satisfatvel

2.4 Sistemas Dedutivos 54

Seja = .

1. Suponha que se |= ento .

2. Suponha que consistente.

3. Suponha, por contradio, que insatisfatvel.

4. Se insatisfatvel, ento, por definio, no existe nenhuma atribuio de

valores verdade que satisfaa todos os membros de . Sendo assim, podemos dizer

que |= e |= , para uma frmula qualquer .

5. Pela suposio em (1), temos que e ;

6. A partir de (5) podemos concluir que

7. Ora, (6) contradiz o fato que consistente.

Assim, por contradio, podemos afirmar que:

Se |= ento

Se {} consistente ento {} satisfatvel

Vamos agora provar a implicao contrria:

1. Suponha que se consistente ento satisfatvel.

2. Suponha |=

3. Suponha, por contradio, que 6

4. Ento { } consistente, j que 6 e portanto no poder ocorrer

que

5. Ento, pela suposio (1), { } satisfatvel.

6. Logo, existe uma valorao que satisfaz {}.

2.4 Sistemas Dedutivos 55

7. Mas isto uma contradio, pois por (2) satisfaz tambm.

Assim, estabelecemos a volta:

Se |= ento

Se {} consistente ento {} satisfatvel

Observaes:

Um conjunto de frmulas consistente se e somente se ( )

Uma valorao s um modelo para = {1, ..., n } se e somente se s(i) = V

para todo i .

Pelo modelo cannico, para provar a completude basta mostrar que todo con-

junto consistente de frmulas satisfatvel.

Prova do Teorema da Completude:

Dado um conjunto de frmulas consistente , ns precisamos construir uma

valorao s e mostrar que s satisfaz .

1o passo: Estender o conjunto consistente para um conjunto satisfazendo

as seguintes condies:

a)

b) maximal e consistente, isto , para toda frmula da linguagem, ou

ou .

2o passo: Seja L a linguagem proposicional e o conjunto dos smbolos propo-

sicionais.

2.4 Sistemas Dedutivos 56

Vamos construir uma valorao que satisfaz a partir de .

s : {V,F} para todo smbolo proposicional A .

s(A) = V se A

s(A) = F se A 6

Ns podemos estender s para um s que valorize frmulas,

s: L {V,F}.( Como definido em aulas anteriores)

Lema da Verdade

Seja um conjunto de frmulas e uma frmula. s() = V

Prova do Lema da Verdade:

Por induo, sobre o comprimento da frmula, isto , no nmero de smbolos

lgicos nela contidos (,, etc).

a) Caso base:

||=0 (Frmula Atmica)

, = A

s(A) = s(A) = V A (pela definio de s)

b) Hiptese de Induo: o lema vale para frmula de tamanho | | n.

c) Queremos mostrar que vale para | |= n+1

Considere | |= n+1

Temos ento vrios casos:

i) =

s() = V sse s( ) = F (definio de s)

2.4 Sistemas Dedutivos 57

sse 6 (pela hiptese de induo)

Logo, (pois maximal)

Logo V sse .

ii) =

s( ) = V sse s()= F s()= V

sse 6

sse

sse

sse , pois ( ) ( )

sse ( ) , pois consistente.

Observao: os casos iii e iv so similares e ficam como exerccio.

iii) =

iv) =

Vamos agora, a partir do lema demonstrado, provar o Teorema da Completude:

1. Suponha consistente.

2. Estenda para maximal e consistente.

3. Construir s e s

4. Seja = {1, ..., n }. Como , i s(i) = V, para todo i (pelo

lema da verdade).

5. Logo, s satisfaz e portanto satisfatvel.

2.5 Aplicao 58

2.5 Aplicao

Suponha que um banco deseja fazer um programa escrito na linguagem da LCP

para decidir o perfil de um dado cliente e decidr qual a plicao que mais apropirida

para ele. O banco classifica o perfil do cliente como: conservador, moderado e

arrojado. As aplicaes so: poupana, aes e mista (metada na poupana e

metade em aes). Um cliente conservador deve aplicar em poupana. Um cliente

moderado deve dividir a aplicao entre poupana e aes. E um cliente arrojado

deve aplicar tudo em aes. Porm, dependendo da renda mensal ele pode ser

aconselhado a aplicar fora do seu perfil. O perfil do cliente identificado fazendo

com que ele responda ao seguinte formulrio:

1. Sua idade maior que 50 anos? ( ) Sim ( ) No

2. Sua idade menor que 30 anos? ( ) Sim ( ) No

3. Casado? ( ) Sim ( ) No

4. Filhos? ( ) Sim ( ) No

5. Renda mensal maior que R$ 10.000,00?

Representao:

I>50 - idade maior que 50 anos

I10K - Renda mensal maior que R$ 10.000,00

Co - perfil conservador

Mo - perfil moderado

2.5 Aplicao 59

Ar - perfil arrojado

Poup - aplicar em poupana

Ac - aplicar em aes

Mx - aplicar em poupana e aes

Regras:

1. (I>50 (I10K Mx

8. Ar Ac

9. Ar R>10K Mx

10. Mo Mx

11. Mo (R>10K lorF ) Ac

12. Mo (R>10K landF ) Poup

Consultas: Dado que um cliente respondeu o questionrio da seguinte forma:

I>50

I

2.5 Aplicao 60

F

R>10K - Renda mensal maior que R$ 10.000,0

Consulta:

1. Poup, i.e., ele deve aplicar em poupana

1. Prove as consultas em Ded. Nat.

2. Prove as consultas em Tableaux

3. Prove as consultas em Resoluo

Observaes:

1. Ser que falta alguma regra? Tem algum caso que no est sendo tratado?

Qual?

2. Suponha que voc deseja guardar todas as respostas de todos os clientes e

gostaria de expressar a seguinte regra: para todo cliente X, X no pode ser

conservador e moderado ao mesmo tempo. Como voc expressaria esta fraze

na linguagem da LCP?

Captulo 3

Logica Clssica de Primeira Ordem

x,EmpUFRJ(x) FuncPub(x)

xy, Suc(y, x)

Lgica Clssica Proposicional

+

Variveis

+

Cosntantes

+

Funes

+

Tabelas (Predicados)

3.1 Linguagem da Lgica Clssica de Primeira Ordem 62

Formaliza o raciocnio dedutivo

Lgica Proposicional um modelo muito restrito:

No podemos descrever propriedades sobre os elementos do universo de dis-

curso: todos os elementos do domnio tm propriedade P; existem elementos do

domnio que tm a propriedade P; no podemos representar relaes e funes.

Ex: Teoria dos Nmeros < 0, suc,

3.1 Linguagem da Lgica Clssica de Primeira Or-

dem

Linguagem: alfabeto + regras gramaticais

Definio 1 Um alfabeto de 1a ordem consiste dos seguintes conjuntos de smbolos:

Smbolos Lgicos:

1. Conectivos lgicos: , , , , , , .

2. Smbolos auxiliares: ( e ).

3. Conjunto enumervel de variveis: V = {v1, v2, ...}

Smbolos no Lgicos:

4. Conjunto enumervel de constantes: C = {c1, c2...}

5. Conjunto enumervel de smbolos de funo: F = {f1, f2, ...} A cada

smbolo funcional est associado um nmero inteiro n > 0, chamado de ari-

dade.

6. Conjunto enumervel de smbolos predicativos (Predicados): P =

{P1, P2, ...}

A cada smbolo predicativo est associado um nmero inteiro n > 0, chamado ari-

dade.

3.1 Linguagem da Lgica Clssica de Primeira Ordem 63

Variveis: representam elementos quaisquer do domnio.

Constantes: do nome a elementos particulares do domnio.

Funes: representam operaes sobre elementos do domnio.

Predicados: representam propriedades ou relaes entre elementos do dom-

nio.

Quantificador universal: para todo elemento do domnio.

Quantificador existencial: existe ao menos um indivduo.

Exemplo: x(y ANCESTRAL(y, x) ANCESTRAL(Joo,Jos))

Definio 1 Os termos da linguagem de 1a ordem so definidos recursivamente

como:

(i) toda varivel e constante um termo;

(ii) se t1, t2, ..., tn so termos e f um smbolo funcional de aridade n, f(t1, t2, ..., tn)

um termo;

(iii) nada mais termo.

Definio 1 As frmulas da lgica de 1a ordem so definidas recursivamente

como:

(i) Se P um predicado de aridade n e t1, t2, ..., tn so termos, ento P (t1, t2, ..., tn)

uma frmula chamada frmula atmica;

(ii) Se e so frmulas, ento (), ( ), ( ), ( ) tambm so

frmulas;

(iii) Se alpha uma frmula e x uma varivel, ento x e x tambm so

frmulas;

3.1 Linguagem da Lgica Clssica de Primeira Ordem 64

(iv) Nada mais frmula

De uma forma alternativa podemos definir a linguagem de primeira ordem por

meio de uma notao BNF.

Termos:

t ::= x | c | f(t1, ..., tn)

Frmulas:

::= P (t1, ..., tn) | (1 2) | (1 2) | (1 2) | | x(x) | x(x)

onde P um smbolo predicativo n-rio e t1, ..., tn so termos.

Observaes:

1. ( ) ( )

2. Convenes:

(i) x, y, z, ... Variveis;

(ii) a, b, c, ... Constantes;

(iii) f, g, h, ... Funes;

(iv) A, B, C, P, U, ... Predicados;

3. x GOSTA(x, collor) xGOSTA(x,collor)

Exerccios: Nos exerccios seguintes, represente cada proposio na linguagem

da lgica de primeira ordem, especificando em cada caso o significado dos smbolos

no lgicos utilizados.

1. Todo cachorro um animal. Todo animal morre. Rex um cachorro.

3.1 Linguagem da Lgica Clssica de Primeira Ordem 65

2. Qualquer pessoa passando nos exames de histria e ganhando na loteria

feliz. Porm qualquer pessoa que estuda ou tem sorte pode passar em todos

os exames. Joo no estudou, mas ele tem sorte. Qualquer pessoa que tem

sorte ganha na loteria. Joo feliz?

3. Toda pessoa que no pobre e esperta feliz. Pessoas que lem no so

burras. Joo sabe ler e rico. Pessoas felizes tm vidas excitantes. Existe

algum que tem vida excitante?

4. Ningum conquistou o mundo. Portanto, todo mundo livre.

5. Todo eltron tem carga negativa. Nenhum psitron tem carga negativa. Por-

tanto, nenhum psitron um eltron.

6. Se Jane est doente, ela no vir trabalhar. Se ela no vier trabalhar, nenhum

de ns ter nada para fazer. Assim, se Jane est doente, nenhum de ns ter

nada para fazer.

Exemplo: Conselheiro Financeiro:

1. Funo: ajuda a decidir se devemos investir em investimentos tipo poupana

ou no mercado de aes.

2. O investimento recomendado depende do ganho mensal da pessoa e quanto ela

tem em poupana.

3. Pessoas com valor inadequado de poupana devem sempre aumentar o valor

da poupana como 1a prioridade, independente do seu ganho.

4. Pessoas com valor adequado de poupana e um ganho adequado devem con-

siderar um investimento mais arriscado, porm mais lucrativo no mercado de

aes.

5. Pessoas com ganho inadequado e com poupana adequada podem considerar

em dividir o valor a ser investido entre poupana e mercado de aes. Isto

aumenta a poupana e tenta aumentar o ganho.

3.1 Linguagem da Lgica Clssica de Primeira Ordem 66

6. Poupana adequada se valor poupado maior do que 5.000 x no de dependentes.

7. Ganho adequado se valor ganho maior do que 15.000 + (4.000 x no de de-

pendentes) e estvel. Um ganho instvel, mesmo que grande, sempre

inadequado.

TOTALPOUP(x): x total na poupana.

DEPEND(y): nmero de dependente

minpoup(y): funo que retorna o valor da poupana mnima (5.000) vezes o

nmero de dependentes

TOTALGANHO(x, estvel): ganho total x e este estvel.

minganho(y): funo que retorna o valor do ganho mnimo mais o acrscimo

por dependente.

MAIOR(x,y): x > y

POUP(status): status uma varivel que indica a situao (adequada/inadequada)

da poupana.

GANHO(status): aqui, status indica a situao (adequada/inadequada) do

ganho.

INVEST(tipo): tipo uma varivel que guarda o tipo de investimento reco-

mendado (poupana/combinado/aes)

Especificao:

1. POUP(inadequado) to INVEST(poupana)

2. POUP(adequado) GANHO(inadequado) INVEST(combinado)

3. POUP(adequado) GANHO(adequado) INVEST(aes)

4. x TOTALPOUP(x) y (DEPEND(y) MAIOR(x, minpoup(y))) POUP(adequado)

onde minpoup(x) = 5.000x

3.2 Sistemas Dedutivos 67

5. x TOTALPOUP(x) y (DEPEND(y) MAIOR(x, minpoup(y))

POUP(inadequado)

6. x TOTALGANHO(x, estvel) y (DEPEND(y) MAIOR(x, minganho(y)))

to GANHO(adequado)

7. x TOTALGANHO(x, estvel) y (DEPEND(y) MAIOR(x, minga-

nho(y))) GANHO(inadequado)

8. x TOTALGANHO(x, instvel) GANHO(inadequado)

Entrada:

9. TOTALPOUP(22.000)

10. TOTALGANHO(25.000, estvel)

11. DEPEND(3)

Exerccio: Qual a sada produzida pela especificao acima para a entrada

dada?

3.2 Sistemas Dedutivos

Sistemas dedutivos para lgica de primeira ordem.

Definio 1 Dizemos que uma varivel x ocorre livre em uma frmula se somente

se:

(i) uma frmula atmica e x ocorre em ;

(ii) uma frmula da forma , , e x ocorre livre em ou ;

(iii) uma frmula da forma e x ocorre livre em ;

(iv) uma frmula da forma y ou y e x ocorre livre em e x 6= y.

3.2 Sistemas Dedutivos 68

Exemplos: x ocorre livre?

1. P(x,y) SIM

2. y( P(x,y) Q(y,x) R(y) ) SIM

3. y( x(P(x) Q(y)) R(x) ) SIM

4. y z ( (xP(x,y) Q(z)) (Q(x) R(x,y)) ) SIM

5. P(z,y) NO

6. y x ( P(x,y) Q(y) ) NO

Definio 1 Uma frmula uma sentena (ou uma frmula fechada) se somente

se no tem nenhuma varivel ocorrendo livre.

Definio 1 Seja uma frmula, x uma varivel e t um termo. Pela substituio

de x por t em ((x/t)) entendemos a expresso resultante da troca de todas as

ocorrncias livres de x por t.

Exemplos:

1. y(P(x, y,f(x, y))) Q(g(x), h(g(x)) x/h(a)

y(P(h(a), y, f(h(a), y)) Q(g(h(a), h(g(h(a))))

2. y( x(Q(x, y, g(z)) P(f(x), y))) R(y(g(x))) x/f(z)

y( x(Q(x, y, g(z)) P(f(x), y))) R(y(g(f(z))))

3. [ y(P(x, y, f(x,y))) Q(y,z) x/g(z) ] z/a

y (P(g(z), y, f(g(z), y)) Q(y, z) z/a

y (P(g(a), y, f(g(a), y)) Q(y, a)

3.2 Sistemas Dedutivos 69

Definio:

Denotaremos por:

(x 1 , x 2 , ..., x n ) (x 1 /t 1 , x 2 /t 2 , ..., x n /t n )

a substituio simultnea (paralelo) de todas as ocorrncias livres de x 1 , ..., x

n por t 1 , ..., t n respectivamente.

OBS: (x 1 /t 1 ) ... (x n /t n ) em srie da esquerda para direita.

(x 1 /t 1 , x 2 /t 2 , ..., x n /t n ) em paralelo.

Exemplos:

1. P(x, f(y), g(x,y)) (x/a, y/b)

P(a, f(b), g(a,b))

2.(yxP (x, y)) Q(g(x)) R(h(y)) (x/f(a), y/z)

(yxP (x, y)) Q(g(f(a))) R(h(z))

3. P(x,y,f(x,z)) (x/g(z), z/y, y/a)

P(g(z), a, f(g(z),y)

4. P(x,y,f(x,z)) (x/g(z)) (z/y) (y/a)

P(g(z),y,f(g(z),z)) (z/y) (y/a)

P(g(y),y,f(g(y),y)) (y/a)

P(g(a),a,f(g(a),a))

Definio:

Uma varivel x substituvel em uma frmula por um termo t se, para cada

varivel y ocorrendo em t, no existe nenhuma subfrmula de da forma y ou

y onde x ocorre livre em .

3.3 Deduo Natural 70

O que queremos evitar com esta condio que o quantificador y ou y capture

alguma varivel de t.

Exemplo:

( y CHEFE(x,y) GERENTE(x)) x/y

( y CHEFE(y,y) GERENTE(y))

3.3 Deduo Natural

Regras para , , , , ABS e RA so as mesmas do caso proposicional.

Regras do Quantificador Universal :

-I

(a)

x(a/x)

Condio: Condio:a no ocorre em

nenhuma frmula do BD e nem em ne-

nhuma suposio em aberto.

-E

x

(x/t)Condio: x substituvel em por t

Regras para o Quantificador Existencial:

-I

(a)

x(a/x)

-E

Condio: a no ocorrem

em , nem no BD e nem em

qualquer suposio na qual

depende, a no ser (x/a).

3.3 Deduo Natural 71

x(x)

[(a)]i

...

i

Exemplo 1: xyP (x, y) yxP (x, y)

1. [xyP (x, y)]1 Suposio

1.1 yP (a, y) -E (1)

1.2 P (a, b) -E(1.1)

1.3 xP (x, b) -I (1.2)

1.4 yxP (x, y) -I (1.3)

2. xyP (x, y) yxP (x, y)1 E(1,1.4)

Exemplo 2: x(Q(y) P (x)) (Q(y) xP (x))

1. [x(Q(y) P (x))]1 Suposio

1.1 Q(y) P (a) -E (1)

1.2 [Q(y)]2 Suposio

1.2.1 P (a) -E (1.1,1.2)

1.2.2 xP (x) -I (1.2.1)

1.3 (Q(y) xP (x)2 -I (1.2,1.2.2)

2. x(Q(y) P (x)) (Q(y) xP (x)) -I (1,1.3)

3.4 Mtodo de Tableaux 72

Exemplo 3:

1. xyP (x, y)

2. xy(P (x, y) Q(x) R(y)) Pergunta: xT(x)?

3. xR(x) xQ(x) x(S(x) T (x))

4. yP (a, y) -E

5, P (a, b) -E(4)

6. y(P (a, y) Q(a) R(y)) -E(2)

7. P (a, b) Q(a) R(b) -E(6)

8. Q(a) R(b) -E(5,7)

9. Q(a) -E(8)

10. xQ(x) -I(9)

11. R(b) -E(8)

12. xR(x) -I(11)

13. xR(x) xQ(x) -I(10,12)

14. x(S(x) T (x)) -E(13,3)

15. [S(a) T (a)]1 Suposio

15.1 T (a) -E(15)

15.2 xT (x) -I(15.1)

16. xT (x)1 -E(14,15,15.2)

3.4 Mtodo de Tableaux

O mtodo de Tableuax apresentado nesta seo foi proposto por Smullian [3] e

pode ser encontrado em [4]. Este se caracteriza por no usar unificao. Existem

outros Tableaux que utilizam unificao mas no sero estudados neste curso.

O mtodo o mesmo da Lgica Clssica Proposicional acrescentando-se quatro

novas regras para tratar dos quantificadores. Comeamos com o ramo incial con-

tendo o BD e a negao da pergunta e aplicamos as regras at obter um Tableaux

fechado ou esgotar todas as possibilidades. A seguir apresentamos as novas regras

3.4 Mtodo de Tableaux 73

para os quantificadores e .

Regras para , , , , so as mesmas do caso proposicional, i.e., R1, R2,

R3, R4, R5, R6 e R7.

Regras do Quantificador Universal :

R8

x

(x/t)Condio: t um termo qualquer

R9

x

(x/t)

Condio: t um termo novo no Table-

aux

Regras para o Quantificador Existencial:

R10

x

(x/t)

Condio: t um termo novo no Table-

aux

R11

x

(x/t)Condio: t um termo qualquer

Condio: nas regras R8 e R11 as frmulas x and x podem ser usadas

mais de uma vez no mesmo ramos.

Exemplo 1: xP (x) xP (x)

3.5 Mtodo Axiomtico 74

1. (xP (x) xP (x)) Negao Perg.

2. xP (x) R7

3. xP (x)) R7

4. P(a) R11

5. P (a) R8

Exemplo 2: {xyP (x, y), xy(P (x, y) Q(x) R(y))} zR(z)

1. xyP (x, y) BD

2. xy(P (x, y) Q(x) R(y)) BD

3. zR(z) Negao Perg.

4. yP (a, y) R10(1)(x/a)

5. P (a, b) R10(4)(y/b)

6. y(P (a, y) Q(a) R(y)) R8(2)(x/a)

7. (P (a, b) Q(a) R(b)) R8(6)(x/a)

8. P (a, b) | (Q(a) R(b)) R7(7)

9. | Q(a) R1(8)

10. | R(b) R1(8)

11. | R(b) R11(3)

3.5 Mtodo Axiomtico

Os conectivos , , , so definidos pelos mesmos axiomas esquema da

Lgica Proposicional.

Axiomas Lgicos:

Implicao:

(1) ( )

(2) ( )) (( ) ))

3.5 Mtodo Axiomtico 75

Conjuno:

(3) ( )

(4) ( )

(5) ( ( ))

Disjuno:

(6)

(7)

(8) (( ) ( )) (( ) )

Negao:

(9)

(10)

(11) ( ) (( ) )

Quantificador Universal:

(12) x (x/t),onde x substituvel por t em ; ( -elim)

(13)( ) ( x ), onde x no ocorre livre em ; ( -introd)

(14) x(x) x(x) por definio

Exemplo 1:

1. xP (x)

2. x((P (x) Q(x)) R(x)) yR(y) ?

3. xQ(x)

3.5 Mtodo Axiomtico 76

4. xP (x) P (y) axioma 12 x/y

5. P(y) MP(1,4)

6. xQ(x) Q(y) axioma 12 x/y

7. Q(y) MP(3,6)

8. P (y) (Q(y) (P (y) Q(y))) axioma 5

9. Q(y) (P (y) Q(y)) MP(5,8)

10. P(y) Q(y) MP(7,9)

11. x((P (x) Q(x)) R(x)) ((P (y) Q(y)) R(y)) axioma12 x/y

12. (P (y) Q(y)) R(y) MP(2,11)

13. R(y) MP(10,12)

14. R(y) (xP (x) R(y)) axioma1

15. xP (x) R(y) MP(13,14)

16. (xP (x) R(y)) (xP (x) yR(y)) axioma13

17. xP (x) yR(y) MP(15,16)

18. yR(y) MP(1,17)

OBS: As noes de prova, teorema e a relao de derivabilidade so

anlogas s da Lgica Proposicional.

3.6 Semntica 77

3.6 Semntica

Nesta seo apresentaremos a semntica da Lgica Clssica de Primeira Ordem

somente para sentenas, isto , frmulas sem ocorrncia de varveis livres.

Reviso da Semntica da Lgica Proposicional:

Maria foi ao cinema. Se ela foi ao cinema ento ela comprou pipoca e assistiu ao

filme. Se ela comprou pipoca ento ela tem dinheiro ou ela pegou emprestado com

Joo. Se ela pegou emprestado com Joo ento Joo tem dinheiro.

C: Maria foi ao cinema.

P: Maria comprou pipoca.

F: Maria assistiu ao filme.

D: Maria tem dinheiro.

E: Maria pegou dinheiro emprestado com Joo.

J: Joo tem dinheiro.

C

C P F

P D E

E J

v(C) = F

v(P ) = V

v(D) = v(E) = F

v(J) = V

3.6 Semntica 78

No um modelo para o conjunto de frmulas, pois no satisfaz todas as frmu-

las.

v(C) = V

v(P ) = V

v(F ) = V

v(D) = F

v(E) = V

v(J) = V

um modelo.

v(C) = V

v(P ) = V

v(F ) = V

v(D) = V

v(E) = F

v(J) = F

um modelo.

A semntica da lgica de primeira ordem tem como objetivo atribuir significados

s frmulas da linguagem.

Uma frmula s tem significado quando uma interpretao dada a seus sm-

bolos no lgicos.

x(Q(x) P (x)) verdadeira ou falsa?

3.6 Semntica 79

Ns s podemos dizer se esta frmula V ou F se interpretarmos seus smbolos

no-lgicos.

Primeiro, precisamos saber qual o universo em que as variveis esto quantifi-

cando. Por exemplo: nmeros inteiros, nmeros reais, pessoas...

Depois, precisamos interpretar os predicados, funes e constantes.

Exemplo: x(Q(x) P (x))

Interpretao:

universo:pessoas

predicados: Q: funcionrio da UFRJ. P: funcionrio pblico.

Figura 3.1:

x(Q(x) P (x)) verdadeira na interpretao acima.

Exemplo 2:

U={Joo, Jos, Pedro}

QI = {< Joao >,< Jose >}

3.6 Semntica 80

P I = {< Jose >,< Pedro >}

x(Q(x) P (x)) falsa nesta interpretao.

Exemplo 3: x(Q(x) P (x))

U = Z (inteiros)

QI = {< 0 >,< 1 >, ...}(naturais)

P I = {... < 2 >,< 1 >,< 0 >,< 1 >,< 2 >, ...} (inteiros)

x(Q(x) P (x)) verdadeira nesta interpretao.

Exemplo 4: x(P (x) Q(x, c))

U = R (reais)

QI = x > c

P I = x racional

cI = 0

Existe algum nmero real que tambm racional e maior do que zero.

Exemplo 5: x(P (x) Q(x) R(x, f(c)))

U = Z (inteiros)

cI = 0

f I = x+ 1

QI = {< 2 >,< 4 >,< 6 >, ...}

P I = {< 1 >,< 2 >,< 3 >, ...}

RI = x > y

Todo nmero inteiro positivo e par maior do que 1. (verdadeiro)

3.6 Semntica 81

Exemplo 6: x(P (x) Q(x) R(x, f(c)))

U = Z (inteiros)

cI = 4

f I = x+ 1

QI = {< 2 >,< 4 >,< 6 >, ...}

P I = {< 1 >,< 2 >,< 3 >, ...}

RI = x > y

Todo nmero inteiro positivo e par maior do que 4. (falso)

Exemplo 7: (yC(x, y)) G(x)

U = {Jos,Joo,Pedro,Paulo}

C : x chefe de y

G : x gerente

CI

Joo Jos

Joo Paulo

Joo Pedro

Joo Joo

Paulo Joo

Paulo Paulo

Paulo Pedro

Paulo Jos

Paulo Jos

GI

Joo

Pedro

3.6 Semntica 82

x = Joo = V

x = Jos = V

x = Pedro = V

x = Paulo = F

Porm, pela nossa definio da linguagem de LPO, podemos ter variveis livres

ocorrendo nas frmulas, por exemplo

xC(x, y)

A varivel y ocorre livre nesta frmula.

Em geral, para sabermos se uma frmula verdadeira ou falsa, ns precisamos

saber o universo e interpretar cada smbolo no-lgico neste universo e dar valor as

variveis livres.

(1) Interpretar variveis livres e constantes em elementos do domnio.

(2) Interpretar predicados em relaes entre elementos do domnio.

(3) Interpretar funes em funes sobre o domnio.

Definio: Definimos uma interpretao como sendo um par ordenado I = onde D um conjunto no-vazio de indivduos chamado domnio. E I

uma funo chamada de funo de interpretao, definida como:

1. I associa a cada varivel livre x um elemento do domnio dI D.

I(x) = dI

2. I associa a cada constante c, um elemento do domnio cI D.

I(c) = cI

3.6 Semntica 83

3. I associa a cada smbolo funcional n-rio f uma funo n-ria f I : Dn D

tal que I(f(t1,...,tn)) = f I(I(t1),...,I(tn)), onde t1,...,tn so termos.

4. I associa a cada smbolo predicativo n-rio P uma relao n-ria sobre D.

I(P ) = P I , P I Dn, ie, P I D D, , ,D, n vezes.

3.6 Semntica 84

Definio:

Seja L uma linguagem de primeira ordem e e , frmulas de L, t1, ..., tn termos,

P um smbolo predicativo n-rio e < D, I > uma interpretao. Definimos a funo

de avaliao de frmulas de L como:

VI :W {V, F}, onde W o conjunto de frmulas, tal que:

(1) VI(P (t1, ..., tn)) = V se somente se < I(t1), ..., I(tn) > P I . F caso contrrio.

(2) VI() = V se VI() = F . F caso contrrio.

(3) VI( ) = V se VI() = V e VI() = V . F caso contrrio.

(4) VI( ) = F se VI() = F e VI() = F . V caso contrrio.

(5) VI( ) = F se VI() = V e VI() = F . V caso contrrio.

(6) VI(x) = V se somente se para todo d D, se I(x) = d ento VI() = V .

F caso contrrio.

(7) VI(x) = V se para algum d D, I(x) = d e VI() = V . F caso contrrio.

3.6 Semntica 85

Definio:

Seja L uma linguagem de 1a ordem. I uma interpretao para L, um conjunto

de frmulas de L e uma frmula.

1. I satisfaz (|=I ) se somente se VI() = V ;

2. I satisfaz se somente se satisfaz cada membro de ;

3. satisfatvel se somente se existe uma interpretao I que satisfaa ;

4. vlida (|= ) se somente se para toda interpretao I, |=I , i.e., VI() = V

para todo I; (*vlida equivalente a tautologia*)

5. implica logicamente em ( |= ) se somente se para toda interpretao

I, se I satisfaz , ento I satisfaz ;

6. insatisfatvel se somente se no satisfatvel, i.e., no existe uma

interpretao I que satisfaz ;

7. Uma interpretao I que satisfaz dita modelo para .

Exemplo1: x(P (x) E(x,s(x))

Esta frmula satisfatvel?

Interpretao: D = { Joo, Jos, Pedro, 0,100, 200}

P : pessoas

E : empregado

s : salrio

Pessoas

Joo

Jos

3.6 Semntica 86

Empregado

Joo 100

Jos 200

Pedro 0

Salrio

Jos 100

Joo 200

... ...

OBS: As funes tm que ser totais,i.e., devem retornar algum valor pertencente

ao domnio a cada elemento do domnio.

VI(x(P (x) E(x, s(x))) = ?

Para todo d D:

d = Joo

VI(P(Joo))= V VI (E(Joo,200)) = F VI(x(P (x) E(x,s(x))) = F

Trocando os valores na tabela de salrio:

Salrio

Jos 200

Joo 100

... ...

Para todo d D:

d = Joo

VI (P(Joo))= V VI (E(Joo,100))= V VI(x(P (x) E(x,s(x))) = V

d = Jos

VI (P(Jos))= V VI (E(Jos,200))= V VI(x(P (x) E(x,s(x))) = V

3.6 Semntica 87

d = Pedro

VI (P(Pedro))= F VI (E(Pedro,...))= ? VI(x(P (x) E(x,s(x))) = V

d = 0

VI (P(0))= F VI (E(0,...))= ? VI(x(P (x) E(x,s(x))) = V

d = 100

VI (P(100))= F VI (E(100,...))= F VI(x(P (x) E(x,s(x))) = V

d = 200

VI (P(200))= F VI (E(200,...))= F VI(x(P (x) E(x,s(x))) = V

Exemplo 2: x(P (x) yQ(x, y))

No Satisfaz Satisfaz

D = {0, 1} D = {0, 1}

P I = {< 0 >} P I = {< 0 >,< 1 >}

QI = {< 0, 1 >} QI = {< 0, 1 >,< 1, 0 >}

Exemplo 3: x(P (x, y) Q(x) R(c))

No Satisfaz Satisfaz

D = {0, 1} D = {0, 1}

yI = 0 yI = 0

cI = 0 cI = 0

P I = {< 1, 1 >} P I = {< 0, 0 >,< 1, 0 >}

QI = {< 1 >} QI =

RI = {< 0 >} RI = {< 1 >}

Exerccio:

Dada a seguinte estrutura:

3.6 Semntica 88

D = {joao, jose, ana,maria}

Filhiacao Homem Mulher Pai

jose joao jose ana joao jose

maria jose jose maria jose maria

joao ana

Interprete a frmula xy(F (y, x)H(x) P (x, y)) e verifique formalmente se

ela verdadeira ou falsa.

3.7 Relao entre Sintaxe e Semntica 89

3.7 Relao entre Sintaxe e Semntica

TEOREMA DA CORRETUDE:

Se ento |= ..

TEOREMA DA COMPLETUDE:

Se |= ento .

3.8 Tabelas - SQL Lgica 90

3.8 Tabelas - SQL Lgica

Nesta seo ilustramos o poder de expresso da LCPO para representar consultas

em SQL.

Dada as seguintes tabelas e as consultas em SQL represente as consultas em

LCPO.

CLIENTE

Cliente Rua Cidade

Joo Monte Rio

Jos Sol Macei

Pedro Flores Curitiba

AGNCIA

Agncia Fundos Cidade

345 100.000,00 Rio

243 340.000,00 Salvador

610 520.000,00 Porto Alegre

EMPRSTIMO

Agncia Emprstimo Cliente Valor

345 107 Joo 2.000,00

243 340 Jos 7.000,00

619 573 Maria 10.000,00

DEPSITO

Agncia Num. C.C, Cliente Saldo

345 10050 Joo 500,00

243 10129 Ana 750,00

619 23040 Maria 200,00

3.8 Tabelas - SQL Lgica 91

Representar as seguintes consultas em lgica. Supondo que as relaes =, 6=, ,, so pr-definidas.

1. Todos os clientes tendo conta na agncia 345.

select Cliente

from DEPSITO

where Agncia = 345

2. Todos os clientes tendo um emprstimo na agncia 345.

select Cliente

from EMPRSTIMO

where Agncia = 345

3. Todos os clientes tendo um emprstimo, uma conta ou ambos na agncia 345.

select Cliente

from DEPSITO

where Agncia = 345

Union

select Cliente

from EMPRSTIMO

where Agncia = 345

4. Todos os clientes tendo um emprstimo e uma conta na agncia 345.

select Cliente

from DEPSITO

where Agncia = 345

Intersect

select Cliente

from EMPRSTIMO

where Agncia = 345

5. Todos os clientes tendo conta na agncia 345 mas no tendo um emprstimo

l.

3.8 Tabelas - SQL Lgica 92

select Cliente

from DEPSITO

where Agncia = 345

Minus

select Cliente

from EMPRSTIMO

where Agncia = 345

6. Todos os clientes e suas cidades que tem emprstimo em alguma agncia.

select CLIENTE.Cliente, CLIENTE.Cidade

from EMPRSTIMO, CLIENTE

where EMPRESTIMO.Cliente=CLIENTE.Cliente

7. Todos os clientes e suas cidades que tem emprstimo na agncia 345.

select CLIENTE.Cliente, CLIENTE.Cidade

from EMPRSTIMO, CLIENTE

where EMPRESTIMO.Cliente=CLIENTE.Cliente and Agncia=345

8. Todos os clientes que tem conta em alguma agncia que Joo tem conta.

select Cliente

from DEPSITO

where Agncia In

select Agncia

from DEPSITO

where Cliente=Joo

9. Ache todas as agncias tem um fundo maior que alguma agncia em Salvador.

select Agncia

from AGNCIA

where Fundos > Any

select Fundos

from AGNCIA

where Agncia = Salvador

10. Ache todas as agncias tem um fundo maior que todas as agncias em Salvador.

3.8 Tabelas - SQL Lgica 93

select Agncia

from AGNCIA

where Fundos > All

select Fundos

from AGNCIA

where Agncia = Salvador

11. Ache todos os clientes tem que conta em agncias em Salvador.

select Cliente

from DEPSITO S

where

select Agncia

from DEPSITO T

where S.Cliente = T.Cliente

Contains

select Agncia

from AGNCIA

where AGNCIA.Cidade = Salvador

3.9 Estruturas e Teorias 94

3.9 Estruturas e Teorias

Nesta seo gostariamos de apresentar alguns exemplos de estruras relacionais

conhecidas e como certas formulas podem ser interpretadas nestas. Achar um con-

junto de frmulas que so verdadeiras exatamente em uma certa clsse de estruturas.

Estudaremos os nmeros naturais, grafos, ordens e rvores.

Quando juntamos um conjunto de frmulas no lgicas a axiomatizao da L-

gica de Primeira ordem obtemos uma Teoria. A partir da teoria podemos deduzir

propriedades (teoremas) sobre a estrutura sendo representada pela teoria.

Grafos, Ordens e rvores

Garfos

Um grafo G = (V,A) uma par onde V um conjunto no vazio de vrtices e

A uma relao binria sobre V , A V V .

Um linguagem, bsica, de primeira ordem para representar grafos dever ter um

smbolo predicativo 2-rio para ser interpretado como A. E o domnio da interpre-

tao deve ser o conjunto de vtices V .

Linguagem: predicado 2-rio R.

Interpretao:

D = V

I(R) = A

Podemos escrever frmulas que impem condies sobre o tipo de grafo. Por

exemplo, a fmula

xR(x, x)

3.9 Estruturas e Teorias 95

verdadeira, na interpretao a cima se e somente se a relao A for refleiva.

Outros exemplos de condies so:

Condio Frmula

Rx. Reflexividade xR(x, x)

IRx. Ireflexividade xR(x, x)

Sm. Simtria xyR(x, y) R(y, x)

Tr. Transitividade xy(z(R(x, z) R(z, y))) R(x, y)

Sl. Serial (Total) xyR(x, y)

Eu. Euclidiana xyz(R(x, z) R(x, y)) R(z, y)

ASm. Anti-Simtrica xyR(x, y) R(y, x) x = y

Tc. Tricotomia xy(R(x, y) x = y R(y, x)

Outra clsse de grafos muito usada em computao clsse dos grafos k-colorveis.

Estes so os grafos que podem ser colorveis com k cores respeitando as seguintes

condies:

1. todo vrtice atribuida uma nica cor;

2. vrtices vizinhos tem cores distintas.

Estes grafos formam uma estrutura com mais k relaes unrias para represen-

tar as cores, G = (V,A, Cor1, , Cork). Para expressar estes grafos precisamos

estender nossa linguagem comok smbolos de predicados C1, Ck e interpret-los

como

I(Ci) = Cori, para todo 1 i k

exerccio: Escreva as frmulas para expressar as condies 1 e 2 para um grafo ser

3-colorvel.

3.9 Estruturas e Teorias 96

Se juntar algumas destas frmulas aos axiomas da Lgica de Primeira Ordem

obteremos uma teoria dos grafos, por exemplo podemos ter a teoria dos grafos

reflexivos e simtricos e etc.

Ordens

Um relao de ordem pode ser vista como um grafo onde o conjunto de aresta

A a prrpria relao de ordem ou < dependendo se a ordem estrita ou no.

Para ter uma ordem algumas condies devem ser impostas:

Ordem Frmulas

Pr Pr-Ordem Rx + Tr

Par. Ordem Parcial Rx + Tr + ASm

Tot Odem Total(linear) Rx + Tr + ASm + Tc

Est. Estrita Subst. Rx por IRx em Pr, Par, Tot

Se juntar algumas destas frmulas aos axiomas da Lgica de Primeira Ordem

obteremos uma teoria das ordens, por exemplo podemos ter a teoria dos grafos

parciais e etc.

rvores

Uma rvore um grafo conexo com um vrtice especial chamado raiz tal que

deste vrtice s existe um nico caminho para qualquer outro vrtice. Uma rvore

pode ser vista como um grafo G = (V,A, raiz). Ns vamos estender a linguagem

dos grafos com uma constante r para denotar a raiz,

I(r) = raiz

exerccio: Escreva as frmulas para expressar que um grafo uma rvore. Dica:

defina um novo smbolo de predicado, na linguagem, para expressar caminho entre

dois vrtices, C(x, y) se exsite um caminho de x para y e/ou use a relao de =.

3.9 Estruturas e Teorias 97

Se juntar estas frmulas aos axiomas da Lgica de Primeira Ordem obteremos

uma teoria das rvores.

Teoria dos Nmeros

Outro exemplo de estrutura so os nmeros Naturais e as operaes bsicas de

aritimtica. Dada a seguinte estrutura AE = IN, 0, S,

3.9 Estruturas e Teorias 98

S1. xS(x) 6= 0

S2. xy(S(x) = S(y) x = y)

L1. xy(x < S(y) x y)

L2. x 6< 0

L3. xy(x < y x = y y < x)

A1. x(x+ 0) = x

A2. xy(x + S(y)) = S(x+ y)

M1. x(x.0) = 0

M2. xy(x.S(y)) = (x.y) + x

E1. x(xE0) = S(0)

E2. xy(xES(y)) = (xEy).x

Um leitor mais familiarizado notar que os seguintes axiomas foram

retirados de AE:

3.9 Estruturas e Teorias 99

S3. y(y 6= 0 x y = S(x))

Induo. ((0) x((x) (S(x)))) x(x)

Se juntarmos estes axiomas com a nossa axiomatixao da Lgica

de Primeira Ordem teremos uma axiomatizao para a aritimtica dos

nmeros naturais, i.e, uma teoria dos nmeros Naturais.

De fato, mesmo sem estes axiomas, ns podemos provar um teorema

muito iteressante:

Teorema 1 Uma relao R recursiva sse R representvel em Cn(AE).

Captulo 4

Lgicas Modais

Este material est sendo construido durante o curso. Faltam vrias

figuras, provas, exemplos e explicaes.

4.1 Linguagem

4.1.1 Alfabeto modal sobre

Dado um conjunto de smbolos proposicionais, = {p, q, ...}, o

alfabeto modal sobre constitudo por: cada um dos elementos de ; o

smbolo (absurdo); os conectivos lgicos (negao), (implicao),

(conjuno) e (disjuno); os operadores modais (necessidade) e

(possibilidade); e os parnteses, como smbolos auxiliares.

4.2 Semntica 101

4.1.2 Linguagem modal induzida pelo alfabeto modal sobre

A linguagem modal induzida pelo alfabeto modal sobre definida

indutivamente da seguinte forma:

::= p | | 1 2 | 1 2 | 1 2 | | |

4.2 Semntica

4.2.1 Frames

Um frame um par F = (W,R) onde W um conjunto no-vazio de

estados e R uma relao binria em W dita relao de acessibilidade.

Diz-se que s2 W acessvel a partir de s1 W se, e somente se,

(s1, s2) R.

No exemplo da figura 4.1 o conjundo de estados W = {s1, s2, s3, s4, s5}

e a relao de acessibilidade R = {(s1, s2), (s1, s3), (s3, s3), (s3, s4), (s2, s4), (s2, s5),

(s4, s1), (s4, s5), (s5, s5)}. O frame F = (W,R).

4.2 Semntica 102

s1 s2

s3 s4

s5

Figura 4.1: Exemplo de um Frame.

4.2.2 Modelos

Um modelo sobre o conjunto um par M = (F, V ) onde F =

(W,R) um frame e V uma funo de no conjunto das partes de

W , que faz corresponder a todo smbolo proposicional p o conjunto

de estados nos quais p satisfeito, i.e., V : 7 Pow(W ).

s1 s2

s3 s4

s5

p

p

p,q

q,r

Figura 4.2: Exemplo de um Modelo.

No exemplo da figura 4.2 o frame o mesmo da figura 4.1 e a funo

V :

4.2 Semntica 103

V (p) = {s3, s4, s5}

V (q) = {s1, s5}

V (r) = {s1}

4.2.3 Satisfao

Seja M = (F, V ) um modelo e w W um estado. A notao

M,w indica que a frmula satisfeita pelo modelo M no estado

w, o que definido indutivamente como:

M,w p sse w V (p)(p )

M,w 6

M,w iff M,w 6 ,

M,w sse M,w 2 ou M,w

M,w sse M,w e M,w

M,w sse M,w ou M,w

M,w sse para todo w W se wRw implica M,w

M,w sse existe w W , wRw e M,w

Ns podemos generalizar a noo de satisfao para conjuntos de

frmulas. Se = {1, , n} ento M,w sse M,w i, para

todo 1 i n.

4.2 Semntica 104

Exemplo: Seja M o modelo da figura 4.2. Queremos verificar se

M, s2 p.

M, s2 p sse para todo w W se s2Rw implica M,w

p, ns precisamos verificar para w {s1, s2, s3, s4, s5}. Como temos

uma implicao, para os no vizinhos de s2 a implicao vacoamente

verdadeira. Ento precisamos verificar somente para

w = s4, M, s4 p sse s4 V (p) o que verdade;

w = s5, M, s5 p sse s5 V (p) o que verdade.

A seguir apresentamos um algoritmo para verificar se uma frmula

modal satisfeita num modelo M = (W,R, V )1 num estado w.1Usaremos no texto M = (W,R, V ) quando na verdade deveriamos usar M = (F, V ) e F =

(W,R).

4.2 Semntica 105

funo Satisfaz(,M , w): booleano

caso :

p: se w V (p) ento retorna verdadeiro

seno retorna falso

: retorna falso

1: retorna not Satisfaz(1,M ,w)

1 2: retorna Satisfaz(1,M ,w) and Satisfaz(2,M ,w)

1 2: retorna Satisfaz(1,M ,w) or Satisfaz(2,M ,w)

1 2: retorna not Satisfaz(1,M ,w) or Satisfaz(2,M ,w)

1: para todo w t. q. wRw faa

se Satisfaz(1,M ,w)ento retorna verdadeiro

retorna falso

1: para todo w t. q. wRw faa

se not Satisfaz(1,M ,w)ento retorna falso

retorna verdadeiro

Complexidade: para cada conectivo booleano so feitas, no pior caso,

duas chamadas e para cada ocorrncia de smbolo proposicional temos

uma chamada. Para os conectivos modais temos que percorrer a lista

de adjacncias, no pior caso, para todos os estados de W. Logo a com-

plexidade O(|| (|W |+ |R|)), isto , linear no tamanho da frmula

e no tamanho do modelo.

Exerccio 1 No modelo da figura 4.2 verifique:

1. M,w (p p)

2. M,w ((p (r s)))

4.2 Semntica 106

3. M,w (p (p r))

4. Satisfaz(r,M, s1)

5. Satisfaz((r p),M, s1)

6. Satisfaz((r (p q)),M, s1)

7. Satisfaz(q,M, s1)

4.2.4 Clsses de Frames

Nesta seo apresentamos algumas clsses de frames que so mais

usuais.

Seja um frame F = (W,R) e F a clsse de todos os frames.

Clsse dos Frames Reflexivos Fr

Composta pelos frames cuja a relao de acessibilidade seja reflexiva.

x W (xRx)

s1 t1

Figura 4.3: Exemplo de Frame Reflexivo

4.2 Semntica 107

Clsse dos Frames Simtricos Fs

Composta pelos frames cuja a relao de acessibilidade seja simtrica.

x, y W (xRy yRx)

s1 t1

Figura 4.4: Exemplo de Frame Simtrico

Clsse dos Frames Transistivos Ft

Composta pelos frames cuja a relao de acessibilidade seja transitiva.

x, y, z W (xRy yRz xRz)

r1

s1

t1

Figura 4.5: Exemplo de Frame Transitivo

4.2 Semntica 108

Clsse dos Frames Seriais Fserial

Composta pelos frames cuja a relao de acessibilidade seja serial.

xy (xRy)

s1 t1

Figura 4.6: Exemplo de Frame Serial

Referncias Bibliogrficas

[1] F. S. C. Silva, M. Finger e A. C. V. Melo. Lgica para a Computa-

o. Thomson Learning, 2006.

[2] H. B. Enderton. A Mathematical Indroduction to Logic. Academic

Press, 1972.

[3] R. M. Smullyan. First Order Logic. Springer-Verlag, 1968.

[4] M. M. C. Costa. Introduo Lgica Modal Aplicada Computa-

o. VIII Escola de Computao. Gramado, 1992.

[5] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. The-

oretical Tracts in Computer Science. Cambridge University Press,

2001.

[6] R. Goldblatt. Logics of Time and Computation. CSLI Lecture

Notes 7,1992.

[7] D. Harel, D. Kozen D. and Tiuryn. Dynamic Logics. MIT Press,

2000.

[8] Chellas, B. (1980). Modal Logic, An Introduction. Cambridge UP,

Cambridge, U.K.