автореферат диссертации по философии, специальность ВАК РФ 09.00.01
диссертация на тему: Эпистемологический статус компьютерных теорем

Введение диссертации2000 год, автореферат по философии, Знатнов, Сергей Юрьевич

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

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

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

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

Степень разработанности проблемы. В современной философской и математической литературе невозможно выделить работы -монографии, книги, диссертации - полностью посвященные выбранной нами для рассмотрения теме. Но необходимо отметить наличие большого количества трудов, посвященных проблеме математического доказательства. А именно таким аспектам, как история развития понятия доказательства, становление критериев строгости доказательства, определению свойств и функций доказательств в дедуктивных системах, проблеме понимания доказательств и их признания математическим сообществом. В этой части работы мы опирались на статьи, монографии и книги отечественных и зарубежных авторов. В их числе: Аникеев В.Н. , Анисов A.M., Асмус В.Ф., Бурбаки Н., Васюков B.JL, Вейль Г., Даан - Дальмедико А., Пейффер Ж., Клини С.К., Кондаков Н.И., Кудрявцев Л.Д., Кузнецова И.С., Манин Ю.И., Мартин-Леф П., Молодший В.Н., Огурцов А.П., Перминов В.Я., Пуанкаре А., Рассел Б., Розов М.А., Рузавин Г.И., Самохвалов К.Ф., Смирнов В.А., Смирнов А.В., Смирнова Е.Д., Стяжкин Н.И., Такеути Г., Успенский В.А., Френкель А., Бар-Хиллел И., Чудинов Э. М., Brown J.R., Devlin К., Кас М., Rota G-C, Schwartz J.T., King J.P., MacKenzie D., Stewart I. , Ulam S.

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

- работы, связанные с рассмотрением общих вопросов применения ЭВМ на текущем этапе развития науки;

- проблемные статьи по анализу результатов неконтролируемой деятельности ЭВМ;

- статьи и книги, посвященные вопросам доказательства правильности программ;

- работы, связанные с философским осмыслением проблемы применения необозримых процедур в математике.

Вот список авторов, работы которых в основном рассматривались во второй главе нашего исследования: Анисов A.M., Барабашев А.Г., Бентли Д., Бирюков Б.В., Бисон М. Дж., Вовк С.Н. , Гаек П., Гавранек Т. , Глушков В. М., Гэри М., Джонсон Д., Дрейфус X., Зенкин А.А., Кочергин А.Н., Матиясевич Ю.В., Новодворский А.Е. , Ра китов А.И., Розов М.А., Рузавин Г.И., Смирнов А.В., Смирнов В.А., Успенский В .А., Чень Ч., Ли P., Appel К., Haken W. , Chaitin G., Detlef-sen M., Luker M., Devlin K. , Fallis D., Fetzer J., Franklin J., MacKenzie D., Teller P., Tymoczko T.

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

Результаты работы основаны на критическом анализе различных материалов по истории и теории доказательства, разнообразных подходов в обосновании правильности компьютерных программ, используемых как в теоретической математике, так и в прикладных системах в промышленности.

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

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

Другие способы обоснования достоверности нового знания базируются на формальном логическом анализе текстов.

В одном случае - это анализ текста программы и доказательство правильности программы. Оно проводится не тестированием, а анализом правильности построения текста программы. При этом программа рассматривается как объект некоторой формально заданной системы. Это поднимает уровень достоверности знания, полученного с применением ЭВМ. Но этот вариант обоснования не избавлен от возможных ошибок, хотя достоверность знания устанавливается на уровне достаточно низкой вероятности ошибки.

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

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

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

Цель работы. Основная цель нашей работы провозглашена уже в самом названии диссертации: определение эпистемологического статуса компьютерных теорем, доказательства которых получены с использованием необозримых процедур. Иначе, главный вопрос, исследованию которого мы посвятили нашу работу, звучит так: возможно ли в принципе достижение такого уровня математической строгости при доказательстве теорем (проведенных с неустранимым применением компьютеров), какой достигается в традиционных доказательствах?

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

В рамках этой цели были установлены следующие задачи исследования:

- рассмотреть динамику становления понятия математического доказательства и его основных критериев и функций;

- определить место нового знания в традиционной дилемме теоретического и эмпирического;

- произвести обзор и классификацию программного обеспечения для доказательства математических утверждений;

- рассмотреть основные ошибки в математических доказательствах и ошибки в программах и предложить возможные варианты устранения этих ошибок;

- определить и обосновать возможность достижения традиционного для теоретической математики уровня достоверности при проведении компьютерных доказательств;

- рассмотреть влияние аксиологических предпосылок на решение проблемы признания доказательств (как традиционных, так и компьютерных);

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

Выбор метода обусловлен непосредственно главной задачей нашего исследования - определить и обосновать возможность достижения высокого уровня достоверности компьютерных теорем. Использование указанных методов в проводимом нами исследовании позволило ответить на один из актуальных вопросов методологии науки: возможно ли применение ЭВМ в теоретической математике без ущерба для установившихся канонов математической строгости?

Основные положения, выносимые на защиту.

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

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

3.Обзор и классификация существующего программного обеспечения, используемого в математической деятельности, позволяет нам сделать вывод о том, что применение ЭВМ приводит к получению существенных результатов, которые иначе были бы недостижимы. Поэтому использование компьютеров в точных науках необходимо о У рассматривать как особый вид исследовательской деятельности, который должен быть эпистемологически обоснованным. 4.Обзор, анализ и классификация ошибок в программах приводит к установлению того требования, что доказательство правильности работы программы нужно считать обязательным шагом в процессе применения ЭВМ в теоретических исследованиях. 5.Обеспечивает ли применение ЭВМ в доказательстве теорем рост математического знания? Мы утвердительно отвечаем на этот вопрос. При этом уточняем, что в настоящий момент мы видим единственный способ достижения максимального уровня строгости доказательства - компьютер должен представить доказательство в виде формального вывода в некоторой дедуктивной системе и зафиксировать этот вывод на материальном носителе. 6. В математике существенную роль в признании "больших" доказательств играет социальный фактор и аксиологические предпосылки. 7 Главное положение: анализ различных способов обоснования правильности результата, полученного в процессе выполнения необозримых процедур, позволяет их представить как: социальный способ; вероятностный способ (доказательство правильности программы путем ее тестирования); формальный способ (доказательство правильности программы на уровне формального анализа текста программы) и достоверный способ (доказательство правильности полученного и зафиксированного формального вывода исходного математического утверждения). Основной результат нашей работы состоит в обосновании тезиса о том, что эпистемологический статус компьютерных теорем может достигать такого же уровня, как и традиционные математические доказательства. Это возможно либо при наличии обозримого доказательства правильности программы доказательства теоремы, либо при наличии зафиксированного формального вывода исходного математического утверждения.

Теоретическая и практическая значимость работы.

Результаты диссертационного исследования представляют интерес как для философов, так и для представителей специально-научных областей знания.

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

Материалы диссертации могут быть практически использованы преподавателями для чтения лекций по теории познания, философии и методологии науки, при разработке спецкурсов для слушателей математических специальностей.

В настоящее время материалы диссертации используются автором для проведении лекционных и семинарских занятий на физико-математическом и технологическом факультетах Коломенского педагогического института.

Апробация работы. Основные идеи диссертации отражены в статьях и публикациях, тезисах научных конференций и других изданиях.

Идеи и предварительные результаты диссертационного исследования докладывались и публиковались в материалах различных конференций, из которых отметим следующие: XI международная конференция по логике, философии и методологии науки (Обнинск, 1995 г.), Международная конференция "Развитие логики в России: итоги и перспективы" (Москва, 1997 г.), Международная конференция "Применение новых компьютерных технологий в образовании" (Троицк 1991, 1994 г.г.), Научно-техническое совещание "Интеллектуальные системы в задачах проектирования, планирования и управления в условиях неполноты информации" (Казань, 1990 г.).

Используя материалы диссертации, автор выступал с докладами и сообщениями на заседаниях кафедры философии Коломенского пединститута и научных конференциях КПИ.

Структура диссертации. В соответствии с целью, задачами и характером исследования структура работы была построена следующим образом: введение, две главы, заключение.

Заключение научной работыдиссертация на тему "Эпистемологический статус компьютерных теорем"

Заключение

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

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

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

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

Существуют различные способы обоснования правильности результата, полученного в процессе выполнения необозримых процедур. Их анализ позволяет выделить социальный способ, вероятностный способ (доказательство правильности программы путем ее тестирования), формальный способ (доказательство правильности на уровне формального анализа текста программы) и достоверный способ (доказательство правильности полученного и зафиксированного формального вывода).

Социальный вариант установления статуса не приводит даже к вероятностному знанию. Тестирование является эмпирическим методом и поэтому неприемлемо для установления статуса математических истин.

Поэтому мы особое внимание в своем исследовании обратили на два варианта формально-логического обоснования.

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

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

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

304 Френкель А., Бар-Хнллел И. Основания теории множеств. - М., 1966. Стр.359

Список научной литературыЗнатнов, Сергей Юрьевич, диссертация по теме "Онтология и теория познания"

1. Алексеев П.В., Панин А.В. Теория познания и диалектика. - М., 1991.- 383 с.

2. Алексеева И.Ю. Человеческое знание и его компьютерный образ. М.: ИФРАН, 1993.-215 с.

3. Аникеев В.Н. Гносеологические функции дедуктивного доказательства // Логика и теория познания. Л., 1990. - С. 51-58.

4. Аникеев В.Н. Развитие понятия доказательства в дедуктивных теориях. Автореферат дисс. канд. филос. наук. Л.: ЛГУ, 1974. -24 с.

5. Анисов A.M. ЭВМ и понимание математических доказательств. //Вопросы философии. 1987 , № 3 . С. 29-40.

6. Анисов A.M. Двойственность знания. //Философия науки. Вып.З. -М., 1997.-С. 88-109.

7. Анисов A.M. Концепция научной философии В.А. Смирнова. //Философия науки. Вып.2. М., 1996. С. 5-27.

8. Анисов A.M. Методологические проблемы применения ЭВМ в математических доказательствах и при моделировании практических рассуждений // Комплексные исследования: предмет, метод, задачи. М., 1987. - С. 35-45

9. Анисов A.M. Три типа существования. // Эпистемология и пост-неклассическая наука. -М.: ИФРАН, 1992. -С. 147-157

10. Арепьев Б.И. Некоторые аспекты философско-математических исследований 19-начала 20 веков. Курск, 1998. - 24 с.

11. Асмус В.Ф. Проблема интуиции в философии и математике. М.: Мысль, 1965.-312 с.

12. Барабашев А.Г. Философия математики в США: современное состояние // Закономерности развития современной математики. -М.: Наука, 1987. С. 288-302

13. Башмакова И.Г. О возникновении математики как науки. // Методологические проблемы развития и применения математики. М., 1985.-С. 173 -177

14. Беляев Е.А., Киселева Н.А., Перминов В.Я. Некоторыеособенности развития математического знания. МГУ., 1975. -112 с.

15. Бентли Д. Жемчужины творчества программистов: Пер. с англ. -М.: Радио и связь, 1990. 224 с.

16. Бирюков Б.В. Что же могут вычислительные машины? // Послесловие к книге Дрейфус X. Чего не могут вычислительные машины. М.: Прогресс, 1978. - С. 298-332.

17. Бирюков Б.В. Жар холодных числ и пафос бесстрастной логики. -М.: Знание, 1985. 192 с.

18. Бисон М. Дж. Доказательство программ и программирование доказательств. // Кибернетический сборник. Новая серия. М.: Мир, 1989. Вып. 26. С. 173-207.

19. Бочаров В.А., Маркин В.И. Основы логики М.: Космополис,1994. -272 с.

20. Бузук Г.Л. Логика и компьютер. -М.: Финансы и статистика,1995.- 208 с.

21. Буковская Н.В. Природа консерватизма в научном познании // Методология науки. Вып. 1,-Томск, 1996. С.36-39.

22. Булос Дж., Джеффри Р. Вычислимость и логика. М.: Мир, 1994. - 396 с.

23. Бунге М. Интуиция и наука. -М.: Прогресс, 1967. -185 с.

24. Бурбаки Н. Очерки по истории математики. М., 1963. -292 с.

25. Василенко О.Н., Современные способы проверки простоты чисел. Обзор // Кибернетический сборник. Новая серия. М.: Мир,1988. Вып. 25. С. 162-188.

26. Васюков В.Л. Автоматическое доказательство теорем // Логика и компьютер 2: Логические языки, содержательные рассуждения и методы поиска доказательств. -М., 1995. - С.24-61.

27. Вейль Г. О философии математики. Л.: ГТТИ. - 128 с.

28. Вейль Г. Математическое мышление. М., 1989. - 400 с.

29. Виноградов В.Г. Научное предвидение. М.: Высшая школа, 1973. -188с.

30. Вирт Н. Алгоритмы и структуры данных: Пер с. англ. -М.: Мир,1989.-360 с.

31. Вовк С.Н. О философском анализе метода математического эксперимента. // Философские проблемы современного естествознания. М., 1983. - N 55. - С. 96-103.

32. Воз Л. Решение некоторых открытых проблем с помощью программы для автоматического доказательства теорем // Кибернетический сборник. Новая серия. М.: Мир, 1984. Вып. 21.

33. Гаек П., Гавранек Т. Автоматическое образование гипотез. М.: Наука, 1984.

34. Гелернтер Г. Реализация машины, доказывающей геометрические теоремы // Фейгенбаум, Фельдман. Вычислительные машины и мышление. М.: Мир, 1967. - 552 с.

35. Гемпель К.Г. Логика объяснения М., 1998,- 237 е.,

36. Глушков В. М. Кибернетика: вопросы теории и практики. -М.: Наука, 1986. -488 с.

37. Грэхем Р. и др. Конкретная математика. М.: Мир, 1998,- 703 с.

38. Гусев С.С., Тульчинский Г.Л. Проблема понимания в философии. М.: Политиздат. 1985.- 192 с.

39. Гэри М., Джонсон Д. Вычислительные машины и труднорешае-мые задачи. М.: Мир, 1982. - 416 с.

40. Даан Дальмедико А., Пейффер Ж. Пути и лабиринты. Очерки по истории математики. - М., 1986.

41. Джонстон Г. Учитесь программировать. М.: ФиС, 1989. - 368 с.

42. Дрейфус X. Чего не могут вычислительные машины. М.: Прогресс, 1978. -332 с.

43. Ершов Ю.Л., Самохвалов К.Ф. О новом подходе к методологии математики // Закономерности развития современной математики. М.: Наука, 1987. - С. 85-105

44. Зарубежные исследования по философским проблемам математики 90-х годов: научно-аналитический обзор. М.: ИНИОН, 1995.-74 с.

45. Зеленогорский Ф.А. О методах исследования и доказательства. -М.: РОССПЭН, 1998.-318 с.

46. Зенкин А.А. Когнитивная компьютерная графика.//Материалы XI Международной конференции по логике, методологии и философии науки. Москва Обнинск, 1995.

47. Знатнов С.Ю. Математические ценности и проблема признания доказательств. Коломна, 2000. - 23 с. Рукопись деп. в ИНИОН РАН № 55443

48. Знатнов С.Ю. Проблема ценности метода в математике. // Аксиология и историческое познание. Коломна. 1996. С. 177-181.

49. Ивин А.А. Логика. -М.: Знание, 1997. 240 с.

50. Ивин А.А., Никифоров А.Л. Словарь по логике М.: ВЛАДОС, 1997.- 384 с.

51. Информатика / Сост. Д.А. Поспелов. М.: Педагогика - Пресс, 1994.- 352 с.

52. Катленд Н. Вычислимость. Введение в теорию рекурсивных функций. М.: Мир, 1983. - 256 с.

53. Кибернетика, мышление, жизнь. Под. ред. А.И. Берга и др. -М.: Мысль, 1964.-511 с.

54. Клини С.К. Введение в метаматематику. М.: ИЛ, 1957. 526 с.

55. Компьютер обретает разум: Пер с англ./ Под редакцией и с предисловием В.Л.Стефанюка. М.: Мир, 1990. - 240 с.

56. Косарева Л.М. Рождение науки нового времени из духа культуры. М.: ИПРАН, 1997,- 358 с.

57. Кочергин А.Н. Машинное доказательство теорем как нетрадиционная исследовательская программа в математике // Исследовательские программы в современной науке. Новосибирск, 1987. -С. 70-89

58. Кочергин А.Н. Моделирование мышления. М.: Политиздат, 1969.-224 с.

59. Коэн X., Ленстра X., мл. Проверка чисел на простоту и суммы Якоби. // Кибернетический сборник. Новая серия. М.: Мир, 1987. Вып. 24. С. 109-159.

60. Кудрявцев Л.Д. Мысли о современной математике и ее изучении. -М.,1977.-111 с.

61. Кузнецова И.С. Гносеологические проблемы математического знания. Л.: Издательство Ленинградского университета, 1984. -135 с.

62. Кульматов В.А. Логическое учение Р. Луллия: автореферат дис. канд.филос.наук : 09.00.07 / Санкт-Петербург. Ун-т. -СПб., 1996,-18с.

63. Кун Т. Структура научных революций. М.: Прогресс, 1975. - 288 с.

64. Лакатос И. Доказательства и опровержения. М.: Наука, 1967. -152 с.

65. Лейбниц Г.В. Сочинения в 4-х т. Т. 2. М.: Мысль, 1983. - 686 с.

66. Лейбниц Г.В. Сочинения в 4-х т. Т. 3. М.: Мысль, 1984. - 734 с.

67. Литцман В. Где ошибка? М.: Физматгиз, 1962,- 192 с.

68. Логика и компьютер. Вып. 1. М., 1990. - 240с.

69. Логика и компьютер. Вып. 3. -М.: Наука, 1996. 225с.

70. Локтюхова М.А К проблеме строгости математического доказательства // Естествознание и философия. М., 1994. - Вып. 6. - С. 11-13 Рукопись деп. в ИНИОН РАН.

71. Мадер В.В. Введение в методологию математики. М.: ИНТЕР-ПРАКС, 1994.-447 с.

72. Манин Ю.И. Доказуемое и недоказуемое. М.: Сов.радио, 1979. - 167 с.

73. Мартин-Леф П. Очерки по конструктивной математике. М., 1975.

74. Матиясевич Ю.В. Вещественные числа и ЭВМ. // Кибернетика и ВТ. М.: Наука, 1986. Вып.2. - С. 104-133

75. Молодший В.Н. Очерки по философским вопросам математики. -М., 1969. -230с.

76. Морозов К.Е. Математическое моделирование в научном познании. М.: Мысль, 1969. - 212 с.

77. Невинс А. Доказательство теорем планиметрии с использованием прямых рассуждений// Кибернетический сборник. Новая серия. -М.: Мир, 1979. Вып. 16. С. 145-170.

78. Никитин А.Г. Познание и заблуждение М.: Прометей, 1998,- 219 с.

79. Новодворский А.Е., Смирнов А.В. Интерактивная система поиска вывода в различных логических системах. // Материалы XI Meждународной конференции по логике, методологии и философии науки. Москва Обнинск, 1995.

80. Ньюэлл А., Шоу Дж., Саймон Г. Эмпирические исследования машины «Логик-Теоретик»; пример изучения эвристик.// Фей-генбаум, Фельдман. Вычислительные машины и мышление. М.: Мир, 1967. - 552 с.

81. Огурцов А.П. Редукция к абсурду и апогогическое доказательство. // Смирновские чтения: 2 международ, конф. М.: ИФ РАН, 1999.-С.213-216.

82. Оревков В.П. Алгоритм Британского музея // Приложении к книге Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем. -М.: Мир, 1983.-360 с.

83. Перминов В .Я. Эмпиризм в современной философии математики // Теоретическое и эмпирическое в современном научном познании. -М., 1984. с. 195-213.

84. Перминов В.Я. Развитие представлений о надежности математического доказательства. М.: Изд-во МГУ, 1986. - 239 с.

85. Перминов В.Я. Содержательность и строгость математического доказательства // Интуиция, логика, творчество. М., 1987. - С. 78-85.

86. Пуанкаре А. О науке. -М.: Наука, 1990. 736 с.

87. Ракитов А.И. Информация, наука, технология в глобальных исторических изменениях. М.: ИНИОНРАН, 1998. - 104 с.

88. Ракитов А.И. Философия компьютерной революции. М.: Политиздат, 1991. -287с.

89. Рассел Б. Человеческое познание: его сфера и границы. К.: Ника-Центр, 1997. -560 с.

90. Розов М.А. О понятии мысленного эксперимента // Смирновские чтения: 2 международ, конф. -М.: ИФРАН, 1999. С. 217-220.

91. Рузавин Г.И. Вероятность и правдоподобные рассуждения. //Философия науки. Вып.2. -М., 1996. Стр. 163-190.

92. Рузавин Г.И. Интуиция и понимание в математике // Интуиция, логика, творчество. М., 1987. - С. 85-98.

93. Рузавин Г.И. Методы научного исследования. М.: Мысль, 1974. -237 с.

94. Рузавин Г.И. Научная теория. М.: Мысль, 1978. - 244 с.

95. Рузавин Г.И. О природе математического знания. М.: Мысль, 1968. 302 с.

96. Самохвалов К.Ф. Степень понятности доказательств как функция их длины // Мышление, когнитивные науки, искусственный интеллект. М., 1988. - С. 35-39.

97. Смирнов В.А. Творчество, открытие и логические методы поиска доказательства // Природа научного открытия. М., 1986. - С. 101-114

98. Смирнова Е.Д. Логика и философия. М.: Росспэн, 1996. - 299 с.

99. Стрыгин В.З. Критика формальнологического метода исследования в дискретной математике. М.: Изд. отд. ЦАГИ, 1998. - 20 с.

100. Стрыгин В.З. Матричная логика и комбинаторные машины. М.: Изд. отд. ЦАГИ, 1998.- 19 с.

101. Стяжкин Н.И. Формирование математической логики. М.: Наука, 1967. - 505 с.

102. ТакеутиГ. Теория доказательств. М., 1978. -412 с.

103. Титов Н.И. Три проблемы теории чисел. М.: Диалог-МГУ, 1999. - 126 с.

104. Узбек К.М. Истина и доказательство в математике // Философские проблемы современного естествознания. М., 1983. - N 55. -С. 91-96

105. Уильяме X. Проверка чисел на простоту с помощью вычислительных машин // Кибернетический сборник. Новая серия. М.: Мир, 1986. Вып. 23. - С. 51-59.

106. Успенский В.А. Семь размышлений на темы философии математики. // Закономерности развития современной математики. М.: Наука, 1987. - с. 106-154.

107. Успенский В.А. Машина Поста. М.: Наука, 1988. - 96 с.

108. Фейгенбаум, Фельдман. Вычислительные машины и мышление. -М.: Мир, 1967.- 552 с.

109. Фейнберг Е.Л. Две культуры: интуиция и логика. М.: Наука, 1992.-251 с.

110. Философские проблемы естествознания. М., 1985. - 400 с.

111. Франс А. Остров пингвинов. Собр.соч. в 8-и томах. Т.6. М., 1959.- 763 с.

112. Френкель А., Бар-Хиллел И. Основания теории множеств. М., 1966. -555 стр.

113. Хазен A.M. О возможном и невозможном в науке, или где границы моделирования интеллекта. М.: Наука, 1988,- 384 с.

114. Хакинг Я. Представление и вмешательство. Начальные вопросы философии естественных наук М.: Логос, 1998,- 291 с.

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

116. Чудинов Э. М. Природа научной истины. М.: Политиздат, 1977. -312с.

117. Швецкий М.В. Язык профессионала программиста и пользователя ЭВМ. Самара, 1993. - 405 с.

118. Шилейко А.В., Шилейко Т.Н. Информация или интуиция? -М.: Молодая гвардия, 1983. 208 с.

119. Штеренберг М.И. О полноте научного метода // Философские исследования. М., 1997, вып.З. стр. 106-131.

120. Эббинхаус Г.-Д. и. др. Машины Тьюринга и рекурсивные функции. М.: Мир, 1972. - 262 с.

121. Эндрю А. Искусственный интеллект. М.: Мир, 1985. - 265 с.

122. Яннакакис М. Укладка планарных графов в книгу из 4-х страниц // Кибернетический сборник, новая серия, Вып.28. -М.: Мир, 1991.-С. 21-65

123. Appel К., Haken W. The solution of the four-color-map problem // Scientific American, 1977, № 10. P. 108-121

124. Brown J.R. Proofs and Picture // British journal for the Philosophy of Science. -Aberden, 1997. vol.48, N2. p.161-180

125. Chaitin G. Randomness and mathematical proof. // Scientific American. 1975, №232 (5). P. 47-52

126. Cooke D.J., Bez H.E. Computer mathematics.- Repr.- Cambridge etc.: Cambridge univ. press, 1987,- XII, 394 p. (Cambr. Сотр. Science Text; 18)

127. Detlefsen M., Luker M. The four-color problem and mathematical proof// J. Of Philosophy, 1980. Vol. 77, N 12. P. 803-820.

128. Devlin К. The Logical Structure of Computer-Aided Mathematical Reasoning 11 American Mathematical Monthly. 1997, aug-sept. P. 632-646

129. Fallis D. The epistemic status of probabilistic proof // J. of philosophy. -N.Y., 1997. -Vol. 94, N 4. P. 165-186

130. Fetzer J. Philosophy and computer science: reflections on the program verification debate // The digital phoenix. -Oxf., Maiden, 1998. P. 253-273.

131. Franklin J. Mathematics, the computer revolution and real world // Philosophica. -Gent (Belgium), 1988(2). Vol.42. P. 79-92.

132. Kac M., Rota G-C, Schwartz J.T. Discrete thoughts: Essays on mathematics, science, a. Philosophy. Boston etc.: Birkhauser, С 1986,- XII, 264 p.

133. King J.P. The art of mathematics.- New York;London.Plenum press, 1993.-VI,313 p

134. Logic Programming and Automated Reasoning. Springer, 1992. Vol 624.

135. Lubanski M. Komputerowa metoda dowodzenia? // Studia filoz. W-wa, 1984. -N 7. - S. 21-28

136. MacKenzie D. Negotiating arithmetic, constructing proof: The sociology of mathematics and information technology // Social studies of science . L., 1993. - Vol. 23, N 1. - P. 37-65

137. MacKenzie D. Slaying the Kraken: The sociohistory of a Mathematical Proof/'/' Social studies of science . L., 1999. - Vol. 29, N 1. - P. 760

138. Mathematics of program construction.- Berlin etc.: Springer, 1993,-V.669, 378 p.

139. Parigot M. Classical Proof as Program // Computational logic and proof theory. Springer-Verlag. 1993. V.713. p.261-273

140. Stewart I. Concepts of modern mathematics.- Repr.- Harmondsworth (Mddx.) etc.: Penguin books, 1976,- VIII, 315p.

141. Teller P. Computer proof// J. Of Philosophy, 1980. Vol. 77, N 12. P.797-803

142. Turing A.M. Intelligent Machinery // Mechanical intelligence.-Amsterdam etc.: North-Holland, 1992,- XIX. P. 107-128.