Удаление модели

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

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

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

Ссылки

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