Обратный метод С.Ю.Маслова и моделирование сознания

С.Л. Катречко

Обратный метод С.Ю. Маслова и моделирование сознания

В настоящее время создано достаточно большое количество программ автоматического доказательства теорем. Как правило достоинство этих программ оценивается по эффективности их работы, т.е. по продолжительности машинного времени, необходимого для доказательства заведомо трудных формул. Именно это проблематика находится в центре внимания теории сложности, в рамках которой сформулирована так называемая P = NP — проблема, указывающая на принципиальные ограничения эффективности работы любого алгоритма. В частности, одной из конкретизаций P = NP — проблемы является задача по созданию алгоритма, выявляющего общезначимость пропозициональных формул за полиноминальное (от числа переменных формул) время.

Можно выделить несколько путей преодоления принципиальных ограничений, связанных с P = NP — проблемой. Первый из них связан с поиском хорошо работающих «быстрых» алгоритмов для больших подклассов формул пропоцизиональной логики, т.е. «неполных» алгоритмов. Например, именно этот подход реализован в языке Пролог, который работает с «хорновским» подклассом формул. Второй связан с созданием «быстрых» вероятностных алгоритмов, которые гарантируют достоверность результата с большой вероятностью. Достаточно перспективным представляется подход разработки «сверхполных» процедур группой А. Драгалина, которые, в силу своей сверхполноты, могут иногда выдавать неверные ответы. Третий подход связан с попыткой решения «в лоб» собственно P = NP — проблемы, т.е. поиском полиноминальных алгоритмов NP-полных задач. В этой связи представляется интересным использование следующего методологического принципа, который широко пропагандировал В.А. Смирнов. Суть его сводится к тому, что для решения труднорешаемой задачи полезно переформулировка этой задачи на другом языке, в силу чего решение задачи оказывается тривиальным. Важно понимать при этом, что новый язык, на котором формулируется задача, должен быть, по существу, метаязыком, содержащим средства для выражения новых абстракций, которые, в свою очередь, необходимы для выражения релевантной для решения задачи дополнительной информации ( в нашем случае — для существенного сокращения времени решения задачи). Хотелось бы отметить, что применение этого методологического принципа позволяет говорить о моделировании существенных черт сознания (мышления), связанных со способностью «схватывать» идею решения, что было показано ленинградским логиком С. Масловым при проведении несложного психологического экспперимента по построению вывода в незнакомом исчислении за ограниченное время [1].

Хорошей иллюстрацией применения этого принципа может служить следующий пример. Пусть нам дано аксиоматическое исчисление:

аксиома 1: A = A A [B], B = С

аксиома 2: (A = B) = (B = A) правило вывода: -------------------- ,

аксиома 3: (A = (B = C) = ((A = B) = C) А [С]

в котором необходимо построить вывод формулы W: (P = Q) = ((Q = R) = (R = P))

Вывод формулы W в данном исчислении занимает около двух страниц. Однако Р.Вейхрауху удалось значительно упростить данную задачу, предложив следующее правило (метаправило) для исчислений подобного типа: Каждое высказывание W, построенное только из пропозициональных переменных с помощью связки эквивалентности "=" таким образом, что любая пропозициональная переменная p входит в W четное число раз (подчеркнуто мной — К.С.), является теоремой [2].

Данное правило позволяет "свести" доказательство некоторой формулы W к простому подсчету "четности" разных переменных, что значительно сокращает "вывод" данной формулы W. Это стало возможным за счет использования при построении вывода новой абстракции — понятия "четное число", которое в языке логики высказываний невыразимо.

С этой точки зрения, представляет интерес подход к построению алгоритмов нахождения общезначимости для пропозициональной логики, предложенный С.Ю.Масловым, который получил название обратный метод [3]. Фактически, исчисления обратного метода представляют из себя метаисчисления, в котором удается выразить информацию о «зацепленности» переменных формулы. Использование этой дополнительной информации позволяет надеяться на построение более эффективных алгоритмов поиска вывода, теоретическая проработка которых велась под руководством Владимира Александровича Смирнова (некоторые из возможных алгоритмов поиска вывода представлены в [4]).

Литература:

1. Маслов С.Ю. Теория поиска вывода и вопросы психологии творчества //Вопросы семиотики, 1979, Вып. 13, С. 17-46

2. Weyhrauch R.W. Prolegomena to a theory of mechanized formal reasoning //Artificial Intelligence, 1980, Vol. 13. P. 133 - 170

3. Маслов С.Ю. Обратный метод установления выводимости для логических исчислений //Труды математического института им. В.А. Стеклова АН СССР, 1968, Т. 98. С. 26 - 87

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