terça-feira, 6 de setembro de 2016

Tablôs Analíticos para Lógica Proposicional Clássica - Uma aula

Este texto replica o conteúdo de uma aula que ministro para os alunos de Lógica para Computação da UTFPR.

O objetivo desta aula é que os alunos aprendam a fazer demonstrações utilizando o sistema dedutivo chamado Tablôs Analíticos.

Inicialmente relembro as motivações para usar sistemas dedutivos (verificar se uma conclusão vem de um conjunto de premissas).

Utilizo o capítulo 2 de Lógica para Computação, Silva, Finger e Melo. Leia-o antes de continuar.

Depois de ler, assista ao vídeo abaixo (observação: são vídeos experimentais, sem qualidade), que descreve as regras do sistema.



No vídeo, inicialmente apresento a configuração inicial do tablô, uma vez que se trata de um método refutacional e que estamos usando a versão marcada do sistema de tablôs analíticos:

Início, conforme vídeo

Em sala de aula, explico o que são fórmulas marcadas e porque as fórmulas do lado esquerdo do sequente (premissas) recebem T (representando True, ou seja, Verdadeiro) e a fórmula do lado direito recebe F (False, Falso).

Em relação a Silva, Finger e Melo, eu mudei um pouco a apresentação das regras no vídeo. Em primeiro lugar, eu digo que o fechamento é uma regra, como se pode ver na figura abaixo.

Regra de fechamento.
Depois eu defino as regras da figura abaixo como sendo as regras lineares (também chamadas de regras alfa):
Regras Lineares, conforme vídeo.

Por fim, temos as regras que bifurcam (também chamadas de regras beta).
Regras que bifurcam, conforme vídeo.

Neste link você pode ver todas as regras do sistema de tablôs analíticos com fórmulas marcadas.

Depois disso, mostro exemplos de tablôs que fecham, isto é, cuja demonstração indica que o sequente é válido. O vídeo abaixo faz isso incluindo alguns indicadores visuais para as razões das aplicações das regras e do fechamento dos ramos.



Neste momento aplico alguns exercícios para, de acordo com os princípios da Aprendizagem Ativa, verificar se os alunos aprenderam.

Depois de confirmar que os alunos entenderam o necessário até agora, explico o que são árvores, que uma árvore tem a raiz na parte de cima e as folhas em baixo. Explico o que são ramos. Depois, explico o que são ramos abertos, ramos fechados, ramos abertos e saturados usando um vídeo que mostra tablôs que não fecham:



No vídeo anterior e no próximo mostro também a ideia de valoração contra-exemplo.



E por fim aplico mais exercícios para verificar se os alunos realmente entenderam o assunto, isto é, que sabem fazer demonstrações utilizando o sistema dedutivo chamado Tablôs Analíticos.

Façam os exercícios em Trabalho de Tablôs Analíticos.