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);

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.