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:

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.

--

--

Associate Professor at UTFPR. Interested in programming (Elixir), logic and Deep Work.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Adolfo Neto

Associate Professor at UTFPR. Interested in programming (Elixir), logic and Deep Work.