Exercise 3: Tableau Proof

Overview

This exercise explores a completely different style of proving than the first two. The natural deduction style proofs were building proof systems that imitated natural reasoning by people. In refutation proof the goal is to use semantically sound techniques to conclude that the negation of the goal is not satisfiable. Classically this is the same as proving the goal, but there is no pretense of appealing to natural linguistic arguments.

Learning Objectives

As you work through this exercise we expect you to learn the following:

• Learn to Construct proofs in the refutation style.
• Prepare for normal forms by exploring how tableau proofs can be represented.
• Internalize that logic is mechanizable.
• Learn a little about Haskell programming.

Getting Started

Refutation source files: SimpleTableau.hs TableauExamples.hs

Directions

• Reprove all the examples you have done before in Exercise 1 and 2 with this prover, recasting valid sequents as tautological implications. (That is, phi_1, phi_2 |- psi becomes phi_1 => phi_2 => psi.)
• Show what happens when you attempt to prove a non-tautology (a good source is Exercises 1.4 #13)
• Prove or refute at least two more examples from Exercises 1.4 #16 and #17.
• Take a look at the LK-style source files: L.hs, GentzenEgs.hs. Redo at least two proofs from Exercise 2 in this system.

What To Turn In

• Drop it in the Ex3 folder in the class drop box
• Be prepared to talk about your solution in class.

Optional

1. Can you find any examples where the tableau prover is significantly faster than the tautology checker you are implementing in Problem Set 1? Can you find any where it behaves worse? If you build some big examples please put them someplace where they can be shared with other students.
2. I attempted a more sophisticated tableau prover in tableau.hs. Make it better. Consider making it prefer non-branching reductions (alpha rules in uniform notation) in preference to branching reductions (beta rules in uniform notation). There are several other suggestions in the lecture notes.
3. If you are familiar with a full scale theorem prover, like Coq or Isabelle, automate the soundness and completeness proofs for the tableau prover.
4. Read the Kreiz and Constable notes on extracting computational content from the L-style proofs. Modify Tactics.hs and L.hs to accommodate extraction of computational content. Identify a subset of the rules for which you can extract computational content; implement it.