Метод резолюций

    Из  работы Ли может быть сделано несколько  выводов. Была составлена программа  для нахождения следствий, получаемых из заданных аксиом. Программа демонстрирует то, что проф. Дж. Маккарти называет «здравым смыслом», т. е. программа может выводить простые логические следствия из того, что ей сообщается. Такая форма здравого смысла является важной составной частью человеческого интеллекта. При этом должна использоваться  более мощная стратегия поиска, чем стратегия «сначала вширь». Большую помощь здесь может оказать использование резолюции единичных элементов. Полезно также отбрасывание вновь порожденного следствия, если оно является единичным элементом, который представляет собой тривиальное следствие некоторой аксиомы или ранее полученного интересного следствия. Это лучше, чем проверка каждого следствия, для определения того, является  ли оно тривиальным следствием некоторой аксиомы  или полученных ранее следствий. Важно снабдить про-

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

    Должны  быть проведены еще значительные исследования, чтобы получить вполне определенное толкование понятия «интересное следствие». Возможно, было бы неплохо изучить, как находит следствия интеллектуально развитый человек. Это помогло бы созданию программ для отыскания следствий, которые обладали бы способностью к индуктивному выводу, могли бы давать определения и выдвигать предположения.  
 
 
 

Заключение 

    Для вычислительных машин могут быть составлены программы, которые доказывают теоремы (находят доказательства и следствия), например первые теоремы в абстрактной теории групп. Создание таких программ имеет важное значение для развития всей теории решения задач, так как дедуктивные построения используются не только в математике, но и при решении большинства типов задач. Разработка механизмов, обеспечивающих возможность использования вычислительных машин для доказательства теорем, способствует также развитию математической логики. В частности, эти работы привели к формулированию принципа резолюции, который оказался эффективным, правильным и полным. Теоремы о полноте были доказаны для нескольких ограниченных форм принципа резолюции, включая резолюцию с «опорным множеством», гиперрезолюцию и семантическую резолюцию.

    Принцип резолюции является более естественным и мощным, чем те правила вывода, которые использовались в программах для нахождения доказательств до его появления. Мощность этого принципа связана с тем, что вычисление термов для получения частных случаев производится при этом автоматически при каждом применении правила. Благодаря этому он становится еще намного более эффективным в смысле сокращения затрат машинного времени и памяти ЭВМ.

    Так как принцип резолюции является весьма естественным, при его использовании сравнительно легко строить дополнительные эвристики (например, резолюцию единичных элементов и стратегию «предпочтение единичным элементам»), которые облегчают действие программ, доказывающих теоремы. Стратегия «опорного множества» хорошо подходит для поиска доказательств. Однако следует продолжить эксперименты с известными эвристиками, включая гиперрезолюцию и семантическую резолюцию. Кроме того, требуется продолжать поиск новых, более совершенных эвристик. Один из путей к этому - изучение способов доказательства теорем человеком.

    Метод резолюции, благодаря работам Робинсона, был положен в основу создания языков программирования Smalltoc и Prolog (Programming in Logic), положившие начало так называемому логическому программированию. В последствии французский математик Колмероэ реализовал первый интерпретатор этих языков на машинах серии IBM. Таким образом, изученный нами метод имеет явную практическую направленность, что полностью подтверждает актуальность выбранной нами темы.