Horns clause and Backchaining most of the logic is done but how to implement it?

The problem that I am having is that I can not wrap my mind around how to implement this logic into a program such as c++, just the logic and I can code. For example, I have the logic that I reduced to Horn form:

1 a => b = ~a V b

2 c ^ d => a = ~(c ^ d) V a = ~c V ~d V a

3 e ^ c => d = ~(e ^ c) V d = ~e V ~c V d

4 f ^ a => c = ~(f ^ a) V c = ~f V ~a V c

5 f ^ e => c = ~(f ^ e) V c = ~f V ~e V c

6 f = f

7 e = e

So there are seven statements here. I want to know if I queried "b" if it is true or not. I am unsure of how to implement this in to code other than in Prolog... Any ideas? I found a small psuedo algorithm but have yet to dicipher its meaning so that I can implement it.

Backward_Chaining(in P0 : negated goal; GAMMA : set of facts and rules;)

{ if P0 = null then succeed;

pick a literal L in P0;

choose a clause C in GAMMA whose head resolves with L;

P := resolve(P0,GAMMA);

bc(P,GAMMA)

}

So I can guess that P0 is proposition 0 but don't know where to go from there...

Any ideas?

Thank you very much for any thoughts.

Brian