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 mo ...

s invented by Donald W. Loveland, 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 a ...

, though they can readily be extended to

logic programming Logic programming is a programming paradigm which is largely based on formal logic. Any program written in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic pro ...

, 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 SLD resolution (''Selective Linear Definite'' clause resolution) is the basic inference rule used in logic programming. It is a refinement of resolution, which is both sound and refutation complete for Horn clauses. The SLD inference rule Give ...

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 ...

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