The Resolution Functions
Located in "/grpoof/prf/prf.ML"; Prf.apply_resol_fwd and Prf.apply_resol_bck. Prf.apply_resol_fwd has type: "(gname * gname) -> gname -> DB_Prf.T -> (gname * DB_Prf.T) Seq.seq" and works as follows:
aname, anames |- rname fname ---------------------- fname/aname anames |- rname