Are you familiar with Prolog? While I'm not an experienced Prolog programmer or
anything, I do know something about how it operates and the theory behind resolution
theorem proving. You can't represent just any logical statement in Prolog, the rule format
for Prolog is what is called a Horn Clause. These special class of clauses can be resolved in
Polynomial time, as opposed to the general class of SAT problems. So if you want to build
an expert system theorem prover, first you have to consider what is it you want to prove?
Not everything can be expressed in Prolog, so you should take that into consideration.

-Jeffery

................