Suppose one writes a logic program that carries out a resolution inference step. That is, let Resolve (c1, c2, c) succeed if c is the result of resolving cl and c2. Normally Resolve would be used as part of a theorem prover by calling it with c1 and c2 instantiated to particular clauses, thereby generating the re-solvent c. Now suppose instead that we call it with un-instantiated and c1 and c2 un-instantiated. Will this succeed in generating the appropriate results of an inverse resolution step? Would you need any special modifications to the logic programming system for this to work?