Como ensinar Tablôs Analíticos?
Estou lecionando Introdução à Lógica para Computação e vou começar a ensinar Tablôs Analíticos para Lógica Clássica Proposicional.
Sigo o livro de Silva, Finger e Melo. Os autores usam o sistema de Tablôs Analíticos com Fórmulas Marcadas. Deixei as regras neste documento. As regras são relativamente simples de aprender. E sequer exijo que meus alunos as memorizem. Permito que as tragam por escrito nas aulas e no dia da prova.
A dificuldade, pelo que percebo deles, está em executar o “algoritmo” de demonstração de um sequente. O objetivo do algoritmo é, dada uma entrada (um sequente como A∨B, A→C, B→D ⊢ C∨D), responder se o sequente é válido, isto é, se a partir das premissas (do lado esquerdo do “⊢”) se pode chegar à conclusão (lado direito). Além disso, quero que os alunos desenhem a árvore de demonstração. Para o sequente acima, o resultado é que ele é válido e a árvore de demonstração é:
Se o sequente não for válido, tem também a questão da valoração contra-exemplo, mas não vou discutir isto aqui.
Um diagrama representando o algoritmo que fiz alguns anos atrás é:
Toda esta introdução foi para dizer que eu quero desenvolver um software (provavelmente em Elixir) para ajudar os alunos a aprenderem a escrever demonstrações com tablôs analíticos.
Minha ideia inicial era criar uma DSL para que os alunos representassem demonstrações em tablôs analíticos. O meu programa receberia algo como:
- T A∨B [premissa]
- T A→C [premissa]
- T B→D [premissa]
- F C∨D [premissa]
- F C [F∨, 4]
- F D [F∨, 4]
- (…)
Mas o problema é: como representar em modo texto as bifurcações da imagem da demonstração? Meu amigo Everaldo Gomes sugeriu que eu desse uma olhada na DOT, a linguagem de descrição de grafos usada pelo GraphViz.
Eu até tentei mas não achei (ainda?) uma solução que fosse suficientemente simples. O problema é que o processo de construção de um tablôs tem muitas opções, bifurcações, fechamento de ramos, etc. Parece que tem que ser algo visual mesmo.
Meu plano B é permitir que o aluno desenhe o tablô no computador, e o sistema gere uma representação numa DSL para representar demonstrações inspirada na DOT. Depois disso, o sistema faz a verificação da demosntração do aluno.
Importante: eu não quero que o sistema faça a demonstração. O aluno faz a demonstração, o sistema apenas verifica. E o aluno pode pedir a verificação até mesmo de uma demonstração parcial.
O que fiz até agora está em https://gitlab.com/adolfont/tableaux.