Model elimination is the name attached to a pair ofproof procedures invented byDonald W. Loveland, the first of which was published in 1968 in theJournal of the ACM. Their primary purpose is to carry outautomated theorem proving, though they can readily be extended tologic programming, including the more generaldisjunctive logic programming.
Model elimination is closely related toresolution while also bearing characteristics of atableaux method. It is a progenitor of theSLD resolution procedure used in theProlog logic programming language.
While somewhat eclipsed by attention to, and progress in, resolution theorem provers, model elimination has continued to attract the attention of researchers and software developers. Today there are several theorem provers under active development that are based on the model elimination procedure.