Недостаток процедуры вывода Эрбрана состоит в экспоненциальном росте множества фундаментальных примеров Si при увеличении г. ... - Большая Энциклопедия Нефти и Газа



Выдержка из книги Вагин В.Н. Достоверный и правдоподобный вывод в интеллектуальных системах


Недостаток процедуры вывода Эрбрана состоит в экспоненциальном росте множества фундаментальных примеров Si при увеличении г. Мультипликативный метод, использованный Гилмором при машинной реализации этой процедуры, также неэффективен. Как легко видеть, даже для малого множества из десяти двухлитерных фундаментальных примеров дизъюнктов существует 210 конъюнкций в ДНФ. Робинсон, который ввел принцип резолюции, являющийся теоретической базой для построения большинства методов автоматического доказательства теорем.

(cкачать страницу)

Смотреть книгу на libgen

Недостаток процедуры вывода Эрбрана состоит в экспоненциальном росте множества фундаментальных примеров Si при увеличении г. Мультипликативный метод, использованный Гилмором при машинной реализации этой процедуры, также неэффективен. Как легко видеть, даже для малого множества из десяти двухлитерных фундаментальных примеров дизъюнктов существует 210 конъюнкций в ДНФ. Робинсон, который ввел принцип резолюции, являющийся теоретической базой для построения большинства методов автоматического доказательства теорем.