Dedução Natural

André Quintiliano BezerraDenyson D. DelgadoElder F. de OliveiraKaio H. DantasPablo A. ChaconVinícius C. de Souza

Componentes

DefiniçãoMotivaçãoConectivosRegras de InferênciaRegras DerivadasValidade do SistemaReferências

Conteúdo

DefiniçãoSistema criado por Gentzen e Jàskowski, na

década de 30.Utilizado para construir demonstrações formais

na lógica.As demonstrações seguem uma via sintática e

utilizam árvores de derivação.

Motivação

Serve para verificar a derivabilidade de uma expressão.

Porém, não serve para gerar um contra-modelo, nem para mostrar um conjunto de derivações possíveis, ou seja, a árvore de derivação nos mostra, apenas, uma das várias, derivações existentes para a expressão

ConectivosNegação (¬) Conjunção ().Disjunção ().Implicação ().Bi-implicação ().

No caso da Lógica de Predicados, adicionamos os quantificadores:

- Universal - Existencial

Temos também alguns símbolos auxiliares.|- Derivação|= Consequência Semântica Bottom (Absurdo)Top (Verdade)

Regras de InferênciaEliminação de ConjunçãoEliminação da ImplicaçãoIntrodução da ConjunçãoIntrodução da ImplicaçãoIntrodução da DisjunçãoEliminação da Disjunção

Regras de InferênciaRegra do Absurdo

- Absurdo Clássico- Absurdo Intuicionista

Eliminação da UniversalEliminação do ExistencialIntrodução do UniversalIntrodução do Existencial

Regras de InferênciaEliminação da Conjunção

Regras de InferênciaEliminação da Implicação

Regras de InferênciaIntrodução da Conjunção

Regras de InferênciaIntrodução da Implicação

Regras de InferênciaIntrodução da Disjunção

Regras de InferênciaEliminação da Disjunção

Regra do AbsurdoAbsurdo Clássico

Regra do AbsurdoAbsurdo Intuicionista

Regras de InferênciaEliminação do Universal

Regras de InferênciaEliminação do Existencial

Regras de InferênciaIntrodução do Universal

Regras de InferênciaIntrodução do Existencial

Regras DerivadasEliminação da NegaçãoIntrodução da NegaçãoSobre a Bi-Implicação

Regras DerivadasEliminação da Negação

Regras DerivadasIntrodução da Negação

Regras DerivadasIntrodução da Bi-Implicação

Exemplos

Exemplos

Validade do SistemaAs regras da lógica são formas

argumentativas válidas. Uma demonstração ou derivação é uma maneira de estabelecer a validade de uma forma argumentativa mais complexa, o que se consegue mostrando que se pode chegar à conclusão desejada partindo das premissas em causa e usando as regras delas

ReferênciasB.M. Acióly; B.R.C Bedregal; Introdução à

Lógica Clássica para a Ciência da Computação

http://pt.wikipedia.org/wiki/Dedução_naturalhttp://criticanarede.com/docs/

etlf_dednatural.pdf