Exercise 3: Tableau Proof


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:

Getting Started

Refutation source files: SimpleTableau.hs TableauExamples.hs


What To Turn In


  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.

Back to the class web-page.
Back to the Course Schedule.