 André Quintiliano Bezerra
 Denyson D. Delgado
 Elder F. de Oliveira
 Kaio H. Dantas
 Pablo A. Chacon
 Vinícius C. de Souza
 Definição
 Motivação
 Conectivos
 Regras de Inferência
 Regras Derivadas
 Validade do Sistema
 Referências
 Sistema 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.
 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
 Negaçã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)
 Eliminação de Conjunção
 Eliminação da Implicação
 Introdução da Conjunção
 Introdução da Implicação
 Introdução da Disjunção
 Eliminação da Disjunção
 Regra do Absurdo
- Absurdo Clássico




- Absurdo Intuicionista
Eliminação da Universal
Eliminação do Existencial
Introdução do Universal
Introdução do Existencial
 Eliminação da Conjunção
 Eliminação da Implicação
 Introdução da Conjunção
 Introdução da Implicação
 Introdução da Disjunção
 Eliminação da Disjunção
 Absurdo Clássico
 Absurdo Intuicionista
 Eliminação do Universal
 Eliminação do Existencial
 Introdução do Universal
 Introdução do Existencial
 Eliminação da Negação
 Introdução da Negação
 Sobre a Bi-Implicação
 Eliminação da Negação
 Introdução da Negação
 Introdução da Bi-Implicação
 As 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
 B.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_natural
 http://criticanarede.com/docs/etlf_dednatural.pdf