| Авторы: |
Катречко С Л |
Обратный метод С.Ю. Маслова
С.Л. Катречко
Обратный метод С.Ю. Маслова *[1]*
В 60-е годы можно говорить о возникновении новой области на стыке логики, эвристики, психологии — теории поиска вывода.
Теория поиска вывода (ТПВ) — это область математической логики, которая изучает возможные способы решения задач в каком-либо исчислении. Более точно, согласно работе С.Ю. Маслова "Теория дедуктивных систем и ее применения", проблематику ТПВ можно определить так: выявление по исчислению и объекту в языке этого исчисления структуры возможных выводов этого объекта, причем выводов интересных в каком-либо отношении. Развитие ТПВ тесно связано с развитием ЭВМ и проблематикой "искусственного интеллекта", так как именно исследования в области "искусственного интеллекта" особенно остро поставили вопрос о том, как протекает процесс решения у человека и как научить этому ЭВМ.
Данная статья будет посвящена области ТПВ, которая получила название автоматическое доказательство теорем [1] и имеет тесную взаимосвязь с логическим программированием [2]. В данной статье внимание будет сосредоточено на одном из важных и интересных результатов в этой области — обратном методе, который был предложен в середине 60-ых годов одним из пионеров разработки теории поиска вывода, российским логиком С.Ю. Масловым (1932 — 1983). Полное представление об обратном методе (ОМ) можно получить в оригинальных работах С.Ю. Маслова [см., например, работу 3].
В настоящее время в ТПВ существует несколько мощных методов автоматического доказательства теорем логических исчислений, среди которых наиболее известными и разработанными являются метод резолюций [4] и метод расщеплений [5]. По своим возможностям обратный метод С.Ю. Маслова является не менее эффективным методом автоматического доказательства теорем, но из-за ряда причин не получил широкого распространения в программировании. Одной из причин такого положения дел является сложность понимания ОМ в оригинальном изложении С.Ю. Маслова. В данной статье будет предложена некоторая конкретизация ОМ для исчисления высказываний, которая проясняет "механизм работы" обратного метода. Другое изложение ОМ для исчисления высказываний можно найти в статьях Г.В. Давыдова [6, 7].
Более того, здесь будет сделана попытка представить логические исчисления, построенные на базе обратного метода (исчисления благоприятных наборов), в качестве базисного языка для "подключения" мощных правил вывода и моделирования других методов АДТ, и в частности для моделирования метода резолюций и метода расщеплений.
Для изложения идейной стороны обратного метода в данной статье устанавливается тесная взаимосвязь ОМ с секвенциальными исчислениями. При этом прослеживается "генетическая" зависимость ОМ от секвенциальных исчислений, которая и проясняет суть подхода, предложенного в обратном методе С.Ю.Маслова.
ОБРАТНЫЙ МЕТОД И СЕКВЕНЦИАЛЬНЫЕ ИСЧИСЛЕНИЯ
Для формулировки обратного метода С.Ю. Маслова в исчислении высказываний (исчисления благоприятных наборов) и выявления основных идей, заложенных в ОМ, постараемся последовательно воспроизвести путь его формирования из секвенциальных исчислений. Для этого необходимо коснуться существенных особенностей этих исчислений.
Секвенциальные исчисления достаточно хорошо приспособлены для поиска доказательства логических формул благодаря некоторым своим особенностям. Главная из них заключена в их аналитическом характере: секвенциальные исчисления перевернули направление поиска вывода, характерное для исчислений гильбертовского типа. Если в гильбертовских (аксиоматических) исчислениях вывод строится "сверху вниз" от аксиом к доказываемой формуле, то секвенциальные исчисления изменили процесс построения вывода (дерева вывода). По существу, первоначально строится даже не дерево вывода, а дерево поиска вывода, которое при определенных условиях может превратиться в дерево вывода (вывод). Дерево поиска вывода строится "снизу вверх": от исходной формулы к концевым вершинам дерева поиска. При этом если все концевые вершины дерева поиска вывода являются аксиомами данного исчисления, то дерево поиска вывода "автоматически" превращается в дерево вывода (вывод): для этого достаточно "прочитать" построенное дерево поиска вывода "сверху вниз". Таким образом, в секвенциальных исчислениях сделана попытка для построения вывода формулы существенным образом использовать ту информация, которая содержится в самой формуле: состав переменных и ее структура (связи между различными переменными). Идейную сторону такого аналитического подхода к построению выводов можно выразить следующим образом: вся информация о том, выводима данная формула или нет, содержится в самой формуле, поэтому при надлежащем анализе формулы можно утверждать о ее выводимости (невыводимости).
Секвенциальные исчисления и представляют собой один из возможных способов такого последовательного анализа. В настоящее время существует несколько других исчислений аналитического характера, реализующих эту идею: например, исчисление аналитических таблиц Р. Смульяна [**; 8] или метод семантических таблиц Э. Бэта [9].
Суть работы секвенциальных исчислений сводится к последовательной разбивке исходной формулы на более простые подформулы до тех пор, пока не будут получены элементарные подформулы, по виду которых можно утверждать о выводимости (невыводимости) исходной формулы.
Обратный метод С.Ю. Маслова *[1]*
В 60-е годы можно говорить о возникновении новой области на стыке логики, эвристики, психологии — теории поиска вывода.
Теория поиска вывода (ТПВ) — это область математической логики, которая изучает возможные способы решения задач в каком-либо исчислении. Более точно, согласно работе С.Ю. Маслова "Теория дедуктивных систем и ее применения", проблематику ТПВ можно определить так: выявление по исчислению и объекту в языке этого исчисления структуры возможных выводов этого объекта, причем выводов интересных в каком-либо отношении. Развитие ТПВ тесно связано с развитием ЭВМ и проблематикой "искусственного интеллекта", так как именно исследования в области "искусственного интеллекта" особенно остро поставили вопрос о том, как протекает процесс решения у человека и как научить этому ЭВМ.
Данная статья будет посвящена области ТПВ, которая получила название автоматическое доказательство теорем [1] и имеет тесную взаимосвязь с логическим программированием [2]. В данной статье внимание будет сосредоточено на одном из важных и интересных результатов в этой области — обратном методе, который был предложен в середине 60-ых годов одним из пионеров разработки теории поиска вывода, российским логиком С.Ю. Масловым (1932 — 1983). Полное представление об обратном методе (ОМ) можно получить в оригинальных работах С.Ю. Маслова [см., например, работу 3].
В настоящее время в ТПВ существует несколько мощных методов автоматического доказательства теорем логических исчислений, среди которых наиболее известными и разработанными являются метод резолюций [4] и метод расщеплений [5]. По своим возможностям обратный метод С.Ю. Маслова является не менее эффективным методом автоматического доказательства теорем, но из-за ряда причин не получил широкого распространения в программировании. Одной из причин такого положения дел является сложность понимания ОМ в оригинальном изложении С.Ю. Маслова. В данной статье будет предложена некоторая конкретизация ОМ для исчисления высказываний, которая проясняет "механизм работы" обратного метода. Другое изложение ОМ для исчисления высказываний можно найти в статьях Г.В. Давыдова [6, 7].
Более того, здесь будет сделана попытка представить логические исчисления, построенные на базе обратного метода (исчисления благоприятных наборов), в качестве базисного языка для "подключения" мощных правил вывода и моделирования других методов АДТ, и в частности для моделирования метода резолюций и метода расщеплений.
Для изложения идейной стороны обратного метода в данной статье устанавливается тесная взаимосвязь ОМ с секвенциальными исчислениями. При этом прослеживается "генетическая" зависимость ОМ от секвенциальных исчислений, которая и проясняет суть подхода, предложенного в обратном методе С.Ю.Маслова.
ОБРАТНЫЙ МЕТОД И СЕКВЕНЦИАЛЬНЫЕ ИСЧИСЛЕНИЯ
Для формулировки обратного метода С.Ю. Маслова в исчислении высказываний (исчисления благоприятных наборов) и выявления основных идей, заложенных в ОМ, постараемся последовательно воспроизвести путь его формирования из секвенциальных исчислений. Для этого необходимо коснуться существенных особенностей этих исчислений.
Секвенциальные исчисления достаточно хорошо приспособлены для поиска доказательства логических формул благодаря некоторым своим особенностям. Главная из них заключена в их аналитическом характере: секвенциальные исчисления перевернули направление поиска вывода, характерное для исчислений гильбертовского типа. Если в гильбертовских (аксиоматических) исчислениях вывод строится "сверху вниз" от аксиом к доказываемой формуле, то секвенциальные исчисления изменили процесс построения вывода (дерева вывода). По существу, первоначально строится даже не дерево вывода, а дерево поиска вывода, которое при определенных условиях может превратиться в дерево вывода (вывод). Дерево поиска вывода строится "снизу вверх": от исходной формулы к концевым вершинам дерева поиска. При этом если все концевые вершины дерева поиска вывода являются аксиомами данного исчисления, то дерево поиска вывода "автоматически" превращается в дерево вывода (вывод): для этого достаточно "прочитать" построенное дерево поиска вывода "сверху вниз". Таким образом, в секвенциальных исчислениях сделана попытка для построения вывода формулы существенным образом использовать ту информация, которая содержится в самой формуле: состав переменных и ее структура (связи между различными переменными). Идейную сторону такого аналитического подхода к построению выводов можно выразить следующим образом: вся информация о том, выводима данная формула или нет, содержится в самой формуле, поэтому при надлежащем анализе формулы можно утверждать о ее выводимости (невыводимости).
Секвенциальные исчисления и представляют собой один из возможных способов такого последовательного анализа. В настоящее время существует несколько других исчислений аналитического характера, реализующих эту идею: например, исчисление аналитических таблиц Р. Смульяна [**; 8] или метод семантических таблиц Э. Бэта [9].
Суть работы секвенциальных исчислений сводится к последовательной разбивке исходной формулы на более простые подформулы до тех пор, пока не будут получены элементарные подформулы, по виду которых можно утверждать о выводимости (невыводимости) исходной формулы.
|
|