В.А. Стеклова АН СССР, Т.98, 1968.

4. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. М., 1983.

5. Данцин Е.Я. Две системы тавтологичности, основанные на методе расщеплений //Записки научных семинаров ЛОМИ АН СССР, Т.105, 1981.

6. Давыдов Г.В. О корректировании недоказуемых формул //Записки научных семинаров ЛОМИ АН СССР, Т.4, 1967.

7. Давыдов Г.В. Синтез метода резолюций с обратным методом //Записки научных семинаров ЛОМИ АН СССР, Т.20, 1971.

8. Войшвилло Е.К. Символическая логика: классическая и релевантная. М., Высшая школа, 1989.

9. Математическая теория логического вывода (статьи Г. Генцена, С. Кангера, Э. Бэта). М., 1967

10. Гэри М.Г., Джонсон Д.С. ЭВМ и труднорешаемые задачи. М., 1982 г.

11. Машинный алгорифм естественного вывода в исчислении высказываний. М.-Л., 1965.

12. Вопросы кибернетики. Вып.131 (проблемы сокращения перебора). М., 1987.

13. Катречко С.Л. Модификации обратного метода С.Ю. Маслова //Материалы X Всесоюзной конференции по логике, методологии и философии науки. М., 1990.

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



--------------------------------------------------------------------------------

[1] Данный текст «расширен» за счет фрагмента из более ранней работы [14] (Катречко С.Л. Моделирование правила расщепления в обратном методе С.Ю. Маслова //Логические методы в компьютерных науках. М., ИФ РАН, 1991). == см. фрагмент ниже в разделе «ДОПОЛНЕНИЕ».
С.Л. Катречко

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

В настоящее время создано достаточно большое количество программ автоматического доказательства теорем. Как правило достоинство этих программ оценивается по эффективности их работы, т.е. по продолжительности машинного времени, необходимого для доказательства заведомо трудных формул. Именно это проблематика находится в центре внимания теории сложности, в рамках которой сформулирована так называемая 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 в данном исчислении занимает около двух страниц. Однако Р.Вейхрауху удалось значительно упростить д