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:
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:
- T A∨B [premise]
- T A → C [premise]
- T B → D [premise]
- F C∨D [premise]
- F C [F∨, 4]
- F D [F∨, 4]
- (…)
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.
