Продемонстрируем этот подход. Для этого представим формулу дизъюнктивной нормальной формой: (P &ШQ) Ъ Q Ъ ШP. Для установления общезначимости F необходимо использовать не только информацию о составе и количестве дизъюнктов, но и дополнительную информацию о составе контрарных пар литер данной формулы. Если представить данную формулу диаграммой (см. ниже), то сам “вид” диаграммы — как показано в [2] — указывает на общезначимость F.

\ /

\ /

----- p ---------- ШQ -----

| | ДИАГРАММА F

| |

----- Шp ------------ Q ------

/ \

/ \

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

1. метод глобальной обработки информации

2. метод временных переменных (метод метапеременных)

Системы, в которых явно представлены средства поиска вывода, можно рассматривать как специальный класс логических исчислений — исчисления поиска вывода, которые могут быть построены следующим образом. Для любого исчисления B любой метод поиска в нем может быть представлен как способ построения по каждому испытуемому на выводимость объекту S специального метаисчисления над B и S — исчисления поиска BS, — выводимость в котором объекта Д эквивалентна выводимости S в исходном исчислении B [1].

Примерами построения таких исчислений поиска вывода являются: исчисление чисел с индексами [3], в котором на базе обратного метода С.Ю.Маслова возможно моделирование известных в ТПВ методов резолюции и расщепления; исчисление "интеллектуального бектрекинга" [4], в котором предложен новый алгоритм унификации, сочетающий идеи методов поиска "в глубину" и "в ширину"; "исчисление поиска вывода с условной дизъюнкцией" [5], позволяющее реализовать различные варианты метода расщепления.

ЛИТЕРАТУРА:

1. Маслов С.Ю. Теория дедуктивных систем и ее применения. — М., Радио и связь, 1986.

2. Давыдов Г.В. Синтез метода резолюций и обратного метода //Записки научных семинаров ЛОМИ, 1971. — Т.20. — С.24 - 35.

3. Катречко С.Л. Моделирование правила расщепления в обратном методе С.Ю. Маслова //Логические методы в компьютерных науках. — М., ИФ РАН, 1992. — С. 125 - 141.

4. Катречко С.Л. Интеллектуальный бектрекинг //Логические исследования. — М., Наука, 1994. — Вып.3.

5. Катречко С.Л. Исчисление поиска вывода с "условной дизъюнкцией" //Материалы XI Международной конференции по логике, методологии и философии науки. — Москва - Обнинск, 1995.
С.Л. Катречко

Обратный метод С.Ю. Маслова *[1]*
В 60-е годы можно говорить о возникновении новой области на стыке логики, эвристики, психологии — теории поиска вывода.

Теория поиска вывода (ТПВ) — это область математической логики, которая изучает возможные способы решения задач в каком-либо исчислении. Более точно, согласно работе С.Ю. Маслова "Теория дедуктивных систем и ее применения", проблематику ТПВ можно определить так: выявление по исчислению и объекту в языке этого исчисления структуры возможных выводов этого объекта, причем выводов интересных в каком-либо отношении. Развитие ТПВ тесно связано с развитием ЭВМ и проблематикой "искусственного интеллекта", так как именно исследования в области "искусственного интеллекта" особенно остро поставили вопрос о том, как протекает процесс решения у человека и как научить этому ЭВМ.

Данная статья будет посвящена области ТПВ, которая получила название автоматическое доказательство теорем [1] и имеет тесную взаимосвязь с логическим программированием [2]. В данной статье внимание будет сосредоточено на одном из важных и интересных результатов в этой области — обратном методе, который был предложен в середине 60-ых годов одним из пионеров разработки теории поиска вывода, российским логиком С.Ю. Масловым (1932 — 1983). Полное представление об обратном методе (ОМ) можно получить в оригинальных работах С.Ю. Маслова [см., например, работу 3].

В настоящее время в ТПВ существует несколько мощных методов автоматического доказательства теорем логических исчислений, среди которых наиболее известными и разработанными являются метод резолюций [4] и метод расщеплений [5]. По своим возможностям обратный метод С.Ю. Маслова является не менее эффективным методом автоматического доказательства теорем, но из-за ряда причин не получил широкого распространения в программировании. Одной из причин такого положения дел является сложность понимания ОМ в оригинальном изложении С.