Статья 2465

Чтобы применить метод резолюции, нужно сначала представить доказываемое утверждение в рамках логического формализма, называемого исчислением предикатов. Затем утверждение отрицается и его отрицание разрешается совместно с набором аксиом - утверждений заведомо справедливых в данной конкретной области или рассматриваемой ситуации. Если комбинирование отрицания утверждения с аксиомами приводит к противоречию, то отрицание должно быть ложным и, следовательно, исходное утверждение - истинным.
В 1964 г. А. Робинсон доказал, что метод резолюции обладает свойством полноты, если исходное утверждение истинно, то в любом случае рано или поздно этот метод приведет к противоречию. Если же исходное утверждение ложно, то нет гарантии в том, что процесс вывода при помощи резолюции не окажется бесконечным. Выводы Робинсона положили начало активным исследованиям, связанным с применением метода резолюции и других родственных ему методов в области автоматического доказательства теорем. Однако у метода резолюции есть один крупный недостаток, он подвержен явлению комбинаторного взрыва, когда число резолюций, проводимых программой, растет экспоненциально как функция сложности задачи. Программы, успешно применяющие метод резолюции на небольших пробных задачах, как правило, не справляются с более интересными задачами реального мира, масштабы которых значительно шире.
С той же трудностью сталкиваются и программы, основанные на другом - логическом методе, называемом структурной индукцией. Такие программы получают на входе большое количество данных об объектах, принадлежащих рассматриваемой в задаче области, и на их основании они должны построить дерево принятия решений для того, чтобы различать объекты. Проблема, возникающая при применении алгоритмов структурной индукции, заключается, однако, в том, что данные не содержат никакой информации, позволяющей решать, какие переменные важны, а какие нет, или указывающей, что делать с данными, содержащими шум, или как поступать в исключительных случаях.