How to teach Analytic Tableaux?

I am teaching Introduction to Logic for Computing and I’m going to start teaching Analytical Tableaux for Propositional Classical Logic.

I follow the book by Silva, Finger and Melo. The authors use the Analytical Tableaux system with Signed Formulas. I present the rules in this document. The rules are relatively simple to learn. And I do not even require my students to memorize them. I allow them to bring the rules on a paper to class and on test day.

The difficulty, from what I perceive of them, is in executing the “algorithm” to prove a sequent. The objective of the algorithm is, given an input (a sequent such as A∨B, A → C, B → D ⊢ C∨D), to answer if the sequent is valid, that is, if from the premises to left side of “⊢” you can reach the conclusion (to the right side). Also, I want students to draw the proof (demonstration) tree. For the sequent above, the result is that it is valid and the proof tree is:

Proof Tree for A∨B, A→C, B→D ⊢ C∨D

This introduction was to say that I want to develop a program (probably in Elixir) to help students learn to write proofs using analytical tableaux.

My initial idea was to create a DSL for students to represent analytic tableaux proofs. My program would receive something like:

  1. T A∨B [premise]

But the problem is: how to represent the proof bifurcations (see image) in text mode? A friend of mine, Everaldo Gomes, suggested that I take a look at DOT, the graph description language used by GraphViz.

I tried but I was not able (yet?) to fidn a solution, that is, a DSL that was simple enough for my students. The problem is that the process of building a tableaux has many options, bifurcations, branch closures, etc. From what I can see now, it has to be something visual.

My plan B is to allow the student to draw the board on the computer, and the system generates a representation in a DOT-inspired DSL to represent his proof. After that, the system verifies the student’s proof.

Important: I do not want the system to do the demonstration. The student does the demonstration, the system just verifies it. And the student may even request the verification of a partial demonstration.

What I have done so far is at 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.