geoff@wacsvax.OZ.AU (Geoff Sutcliffe) (11/22/88)
I have been searching (in the wrong places obviously) for a proof that resolution & paramodulation, or resolution & paramodulation & factoring, form a complete input refutation system for sets of Horn clauses, and that the single negative clause in a minimally unsatisfiable set of Horn clauses may be used as the top clause in such refutations. Refutation completeness, without specification of the top clause, is in "Unit Refutations and Horn Sets" [Henschen 1974]. If set-of-support is compatible with input resolution,paramodulation,factoring then it is possible to choose the negative clause as the support set, and the problem is solved. Is this compatibility known? Any help, with this seemingly obvious result, would be appreciated. Geoff Sutcliffe Department of Computer Science, CSNet: geoff@wacsvax.oz University of Western Australia, ARPA: geoff%wacsvax.oz@uunet.uu.net Mounts Bay Road, UUCP: ..!uunet!munnari!wacsvax!geoff Crawley, Western Australia, 6009. PHONE: (09) 380 2305 OVERSEAS: +61 9 380 2305