Hispanopedia WikiLa eliminación de modelos es el nombre que se le da a un par de procedimientos de demostración inventados por Donald W. Loveland , el primero de los cuales se publicó en 1968 en el Journal of the ACM . Su propósito principal es llevar a cabo la demostración automatizada de teoremas , aunque se pueden extender fácilmente a la programación lógica , incluida la programación lógica disyuntiva, que es más general .
La eliminación de modelos está estrechamente relacionada con la resolución, a la vez que presenta características de un método de tableaux . Es precursora del procedimiento de resolución SLD utilizado en el lenguaje de programación lógica Prolog .
Aunque algo eclipsada por la atención y los avances en los demostradores de teoremas por resolución, la eliminación de modelos ha seguido atrayendo la atención de investigadores y desarrolladores de software. Actualmente, existen varios demostradores de teoremas en desarrollo que se basan en el procedimiento de eliminación de modelos.
Referencias
- Loveland, DW (1968) Demostración mecánica de teoremas mediante eliminación de modelos . Journal of the ACM, 15, 236—251.
- Demostración automatizada de teoremas
- Cálculos lógicos
- Lógica en informática