Not logged in. Login

Wang Algorithm

Proving that propositional formulas are tautologies by the truth table method has two disadvantages:

  • The number of truth table entries grows exponentially with the number of distinct propositions.
  • The truth table method gives no insight into the structural reasons making a formula true.

Theorem Proving by Reduction: Wang Algorithm

The Wang algorithm is a method for determining proofs of logical formulas using systematic reduction transformations.

Reduction is a general technique of symbolic computing, in which "higher-level" structures are systematically reduced to combinations of simpler ones.

For example:

\(p \implies q \quad \text{reduces to} \quad (\neg p) \vee q\)

\(p \equiv q \quad \text{reduces to} \quad (p \wedge q) \vee ((\neg p) \wedge (\neg q))\)

Hypothesis and Goal Lists

The basic idea of the Wang algorithm is to work through steps involving hypothesis and goal lists.

  • Hypothesis lists are a set of propositional formulas assumed to be true.
  • Goals are formulas that we want to prove true; if any one of the goals is established, the proof is complete.

Proof Conjectures

Given

  • a list of of hypothesis formulas \(H = h_1, h_2, \ldots, h_m \) and
  • a list of goal formulas, \(G = g_1, g_2, \ldots, g_n\), we say that the theorem we are trying to prove is proof conjecture, written \(H \vdash G \).

In essence, the proof conjecture is equivalent to proving that the following formula is a tautology. \((h_1 \wedge h_2 \wedge \ldots \wedge h_m) \implies (g_1 \vee g_2 \vee \ldots \vee g_n)\)

Ground Rules

The ground rules of the Wang method deal with propositions, allowing us to determine when the the overall proof conjecture is true.

  • Rule 1a: if the goal list has a proposition that is also in the hypothesis list, the conjecture is true.
  • Rule 1b: if both the goal list and hypothesis list contain propositions only, and no common propositions, the conjecture is disproven.

Reduction Rules

The Wang method uses a series of reduction rules that gradually replace composite formulas on the hypothesis and goal lists with new proof conjectures involving reduced formulas.

  • There are two rules for each logical formula type.
    • One rule shows how to reduce such a formula found on the hypothesis list.
    • The other rule shows how to reduce such a formula found on the goal list.

Negations

The two rules for negations are as follows.

Rule 2a: \(H, \neg f \vdash G \quad \text{reduces to} \quad H \vdash G, f\)

Rule 2b: \(H \vdash G, \neg f \quad \text{reduces to} \quad H, f \vdash G\)

Conjunctions

Rule 3a: \(H, f_1 \wedge f_2 \vdash G \quad \text{reduces to} \quad H, f_1, f_2 \vdash G\)

Rule 3b: \(H \vdash G, f_1 \wedge f_2 \quad \text{reduces to} \quad H \vdash G, f_1 \quad \text{and} \quad H \vdash G, f_2 \)

Disjunctions

Rule 4a: \(H, f_1 \vee f_2 \vdash G \quad \text{reduces to} \quad H, f_1 \vdash G \quad \text{and} \quad H, f_2 \vdash G\)

Rule 4b: \(H \vdash G, f_1 \vee f_2 \quad \text{reduces to} \quad H \vdash G, f_1, f_2 \)

Implications

Rule 5a: \(H, f_1 \implies f_2 \vdash G \quad \text{reduces to} \quad H, f_2 \vdash G \quad \text{and} \quad H \vdash G, f_1\)

Rule 5b: \(H \vdash G, f_1 \implies f_2 \quad \text{reduces to} \quad H, f_1 \vdash G, f_2 \)

Equivalences

Rule 6a: \(H, f_1 \equiv f_2 \vdash G \quad \text{reduces to} \quad H, f_1, f_2 \vdash G \quad \text{and} \quad H \vdash G, f_1, f_2\)

Rule 6b: \(H \vdash G, f_1 \equiv f_2 \quad \text{reduces to} \quad H, f_1 \vdash G, f_2 \quad \text{and} \quad H, f_2 \vdash G, f_1\)

Wang Algorithm

A proof conjecture is proven or disproven as follows.

1. We form a list of conjectures to be proven, initially consisting of just the one given conjecture.

2. In each step, we take one conjecture from the list and proceed as follows.

  • If the conjecture is proven by Rule 1a, we remove it from the list of conjectures. If there are no more conjectures, then the process is complete and the proof succeeds.
  • If the conjecture is disproven by Rule 1b, then the process is complete and the proof fails.
  • Otherwise, we choose a composite formula from either the hypothesis or goal lists to apply a reduction step.
  • The reduction step uses one of the rules 2a through 6b to generate one or two new conjectures.
  • The new conjectures are added to the conjecture list and we repeat the overall process.
Updated Tue Nov. 06 2018, 13:18 by cameron.