Nguyen, Linh AnhGore, Rajeev2015-12-130020-0190http://hdl.handle.net/1885/83144We present a proof of completeness of hyper-resolution based on the fixpoint semantics of disjunctive logic programs. This shows that hyper-resolution can be studied from the point of view of logic programming.Keywords: Decision theory; Functions; Mathematical models; Mathematical operators; Semantics; Theorem proving; Automatic theorem proving; Fixpoint semantics; Herbrand model; Logical calculi; Logic programming Automatic theorem proving; Fixpoint semantics200510.1016/j.ipl.2005.02.0032015-12-12