Model Elimination is the name attached to a pair of

proof procedure In logic, and in particular proof theory, a proof procedure for a given logic is a systematic method for producing proofs in some proof calculus of (provable) statements. Types of proof calculi used There are several types of proof calculi. The mos ...

s invented by

Donald W. Loveland Donald W. Loveland (born December 26, 1934, in Rochester, New York)Loveland, D.W.; Stickel, M.E."A Hole in Goal Trees: Some Guidance from Resolution Theory" In Proceedings of IEEE Trans. Computers. 1976, 335-341. is a professor emeritus of compu ...

, the first of which was published in 1968 in the Journal of the ACM. Their primary purpose is to carry out

automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was ...

, though they can readily be extended to

logic programming Logic programming is a programming paradigm which is largely based on formal logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of log ...

, including the more general disjunctive logic programming. Model Elimination is closely related to resolution while also bearing characteristics of a Tableaux method. It is a progenitor of the SLD resolution procedure used in the

Prolog Prolog is a logic programming language associated with artificial intelligence and computational linguistics. Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily a ...

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.

References

* Loveland, D. W. (1968
Mechanical theorem-proving by model elimination
Journal of the ACM, 15, 236—251. Automated theorem proving Logical calculi Logic in computer science