Каковы были недостатки процедуры разрешения Робинсона?

Question

Полсон и др. От LCF до Isabelle / HOL скажите:

Решение для логики первого порядка, полное в принципе, но часто разочаровывающее на практике.

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

Резолюция - это опровергающий полный метод доказательства теорем: противоречие (т. Е. Пустое предложение) может быть выведено из любого невыполнимого набора предложений.

Из Википедии:

Попытка доказать выполнимую формулу первого порядка как невыполнимую может привести к невыполнимому вычислению.

Почему это разочаровывает?

Answer 1

Хотя «разочарование на практике», конечно, не поддается определению формально, в отличие от «полного» (что действительно означает «может в конечном итоге доказать каждую истинную формулу»), довольно легко найти примеры, где наивное разрешение даже отдаленно неадекватно, т.е. примеры, которые должны легко доказать, но какое разрешение очень медленное.

Известный пример - это кодирование принципа голубятни для$n$ дыры в логике высказываний (что является утверждением "$n+1$ голуби не могут вписаться $n$отверстия без дубликатов). Нет доказательства этого утверждения, использующего только разрешение по времени, субэкспоненциальное в$n$.

Еще хуже обстоит дело с логикой предикатов, где очень легко найти утверждения без каких-либо доказательств быстрого разрешения.

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