18-21 Процедуры поиска доказательства(теорем)
Рассмотрим процедуры поиска доказательства(теорем).
Черге, а затем Тьюрингом было доказано, что не существует никаких общеразрешающих процедур, никакого алгоритма, проверяющего
общезначимость формул логики предикатов.
Тем не менее существуют алгоритмы поиска доказательства, которые могут подтвердить, что формула общезначима, если она на
самом деле общезначима. Для необщезначимых формул эти алгоритмы, вообще говоря, не заканчивают свою работу. Это лучшее, на
что можно надеятся.
Очень важный подход к автоматическому доказательству теорем был дан Эрбраном в 1930году. Он предложил рассматривать лишь
определенные интерпретации. В 1965 году Робинсоном была предложена процедура поиска доказательств – метод резолюций,
оказавшийся очень эффективным.
Процедуры поиска доказательств с использованием метода резолюций на самом деле являются процедурой поиска опровержения, то
есть вместо доказательства общезначимости формулы, доказывается, что отприцание формулы противоречиво. Процедура опровержения
применяется к стандартным формам формул.