9. The method of claim 1 , further comprising providing at least one axiom which constrains operation of the theorem prover module.
11. The method of claim 9 , wherein said providing comprises supplying said at least one axiom to the theorem prover module in explicit form, wherein the theorem prover module utilizes said at least one axiom in course of processing said at least one converted predicate.