Model elimination is the name attached to a pair of
proof procedure {{Short description, Systematic method for producing proofs
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 ...
s invented by
Donald W. Loveland, the first of which was published in 1968 in the ''
Journal of the ACM
The ''Journal of the ACM'' (''JACM'') is a peer-reviewed scientific journal covering computer science in general, especially theoretical aspects. It is an official journal of the Association for Computing Machinery. Its current editor-in-chief is ...
''. 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 majo ...
, though they can readily be extended to
logic programming
Logic programming is a programming, database and knowledge representation paradigm based on formal logic. A logic program is a set of sentences in logical form, representing knowledge about some problem domain. Computation is performed by applyin ...
, 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 rule of inference, inference rule used in logic programming. It is a refinement of Resolution (logic), resolution, which is both Soundness, sound and refutation Completen ...
procedure used in the
Prolog
Prolog is a logic programming language that has its origins in artificial intelligence, automated theorem proving, and computational linguistics.
Prolog has its roots in first-order logic, a formal logic. Unlike many other programming language ...
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