Some theorems

Let T be a closed clause tree rooted at some proposition p, define sub-program S_T as the set of ground clauses from logic program S that were used to construct T. Below are three important theorems relating supporting propositions, clause trees, and sub-programs. The reader is referred to [Fisher96] for the proofs.
Theorem 1. If S is consistent and S |= p then there is a closed clause tree rooted at p constructed using clauses from S.

Theorem 2. If there is a closed clause tree T rooted at p and S_T is consistent, then S_T |= p.

Theorem 3. If p is supported by closed clause tree T, then S_T is consistent and S_T |= p.

For example, consider T2. S_T2 = {(~c <- ~b),(~b <- e, f),(e <- c),(f <- )}. S_T2 is consistent (e.g., assign TRUE to e and f and FALSE to c and b). Next, simply convert T2 to a linear refutation of c from S_T2 to show S_T2 |= ~c.