Модель устранения

Исключение модели — это название пары процедур доказательства, изобретенных Дональдом У. Лавлендом , первая из которых была опубликована в 1968 году в журнале ACM . Их основная цель — автоматическое доказательство теорем , хотя их можно легко распространить на логическое программирование , включая более общее дизъюнктивное логическое программирование .

Устранение модели тесно связано с разрешением , но также имеет характеристики метода таблиц . Это прародитель процедуры разрешения SLD , используемой в языке логического программирования Prolog .

Хотя метод исключения моделей несколько затмевается вниманием к доказывателям теорем о разрешении и прогрессом в этой области, он продолжает привлекать внимание исследователей и разработчиков программного обеспечения. Сегодня в активной разработке находится несколько доказывателей теорем, основанных на процедуре исключения моделей.

• Лавленд, Д. У. (1968) Доказательство механических теорем методом исключения моделей. Журнал ACM, 15, 236—251.