Wang Algorithm Proof Generation

Consider the task to write a Haskell program to generate proofs or refutations of proof conjectures according to the Wang algorithm.

Following the Wang algorithm in a straightforward manner will result in a binary decision result, either the proof conjecture is proven or it is disproven.

However, a much more useful result is to have a record of the steps of the process, forming either a proof or a refutation of the conjecture.

Symbolic Data Domains: Conjectures, Proofs, Refutations

In order to implement the Wang algorithm theorem prover, we need new data representations for conjectures, proofs and refutations.

A proof conjecture is straightforward. Using the domain of propositional formulas, the following data type suffices.

data ProofConjecture = Conjecture [PF] [PF]

That is, a proof conjecture has two lists of formulas, the first being the hypothesis list and the second being the goal list.

Proofs and refutations are records of the steps applied in the Wang algorithm. The key idea is to structure the proof or refutation as a recursive data domain, so that a proof contains its subproofs and similarly a refutation contains subrefutations.

It is your task to determine a suitable Haskell representation of proofs and refutations and to implement your Wang algorithm prover using these representations.

Proofs and Refutations

A proof of a conjecture of one of three types:

• A simple proof by Rule 1a having two components:
  • the proof conjecture
  • the proposition found to be in common between the hypothesis and goal lists.
• A linear proof by rules 2a, 2b, 3a, 4b or 5b with four components:
  • the proof conjecture
  • the rule
  • the hypothesis or goal formula being reduced
  • the subproof for the reduced proof conjecture
• A double proof by rules 3b, 4a, 5a, 6a, or 6b with five components
  • the proof conjecture
  • the rule
  • the hypothesis or goal formula being reduced
  • the two subproofs for the reduced proof conjectures

Refutations

A refutation of a conjecture of one of two types:

• A simple refutation by Rule 1b having one component:
  • the refuted conjecture (only propositions, none in common)
• A subrefutation consisting of four components
  • the refuted conjecture
  • the rule
  • the hypothesis or goal formula being reduced
  • one subrefutation

Exercise

Write a program to parse a propositional formula from an input file, and generate a printed representation of the proof or refutation to stdout. Make sure to use prettyprinting techniques.