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 é:

Demonstração de A∨B, A→C, B→D ⊢ C∨D

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 é:

Algoritmo para a demonstração de sequentes usando tablôs analíticos

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:

1. T A∨B [premissa]
2. T A→C [premissa]
3. T B→D [premissa]
4. F C∨D [premissa]
5. F C [F∨, 4]
6. F D [F∨, 4]
7. (…)

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.