БЕЛОРУССКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТВыпускная работа по«Основам информационных технологий» Аспирант кафедры дифференциальных уравнений Зорин Евгений ВладимировичРуководители:Член-корреспондент НАН Б, профессор Берник Василий Иванович,ст. преподаватель Кожич Павел Павлович Минск – 2007 г. Оглавление Оглавление 2Реферат 3Введение 4Часть 2. Некоторые программные пакеты предназначенные для математических расчетов 10Mathematica 10Maple 12Список литературы к реферату. 15Предметный указатель к реферату 16Интернет ресурсы в предметной области исследования. 17Действующий личный сайт в WWW (гиперссылка). 18Граф научных интересов . 19Презентация магистерской диссертации. 20Список литературы к выпускной работе. 21 ^ БЕЛОРУССКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ Реферат по теме«Применение информационных технологий в математике» Аспирант кафедры дифференциальных уравнений^ Зорин Евгений ВладимировичРуководители:Член-корреспондент НАН Б, профессор Берник Василий Иванович,ст. преподаватель Кожич Павел ПавловичМинск – 2007 г Введение Тест Тьюринга — тест, предложенный Аланом Тьюрингом в 1950 г. в статье «Вычислительные машины и разум» (Computing machinery and intelligence) для проверки, является ли компьютер разумным в человеческом смысле слова. Тьюринг предложил тест, чтобы заменить бессмысленный, по его мнению, вопрос «может ли машина мыслить?» на более определенный.Тест должен проводиться следующим образом. Судья (человек) переписывается на естественном языке с двумя собеседниками, один из которых — человек, другой — компьютер. Если судья не может надежно определить, кто есть кто, считается, что компьютер прошел тест. Предполагается, что каждый из собеседников стремится, чтобы человеком признали его. Чтобы сделать тест простым и универсальным, переписка сводится к обмену текстовыми сообщениями.Переписка должна производиться через контролируемые промежутки времени, чтобы судья не мог делать заключения исходя из скорости ответов. (Во времена Тьюринга компьютеры реагировали медленнее человека. Сейчас это правило необходимо, потому что они реагируют гораздо быстрее, чем человек.) (материал из Wikipedia)В программу научной конференции по кибернетике и информатике, которая пройдет в июле этого года во Флориде, включили бессмысленный доклад, состоящий из случайно подобранного текста, таблиц и диаграмм, сообщает BBC News. Эта работа, озаглавленная "Рутер: Методология типичной унификации точек доступа и резервирования", была написана компьютерной программой-генератором случайных текстов.(новостная лента, апрель 2005 года, http://www.lenta.ru/news/2005/04/16/hoax/)Компьютеры играют все большую роль в современном мире. Они заменяют человека повсюду, где требуется методичное, кропотливое, четкое и быстрое руководство происходящими процессами и молниеносное реагирование на происходящие события. Вместе с тем до сих пор остается нерешенной проблема алгоритмизации творческих процессов. Да, компьютеры пишут стихи (одну из программ для этого можно скачать вот здесь: http://lleo.aha.ru/soft/lleo_dip.htm), рисуют абстрактные картины, но люди по прежнему интересуются такими произведениями только исходя из того, что они созданы необычным автором. Процесс «инсайта», творческого создания чего-либо нового, до сих пор не удается по-настоящему алгоритмизировать, несмотря на огромный интерес который вызывает этот вопрос для людей и (как следствие) огромные усилия прикладываемые в этой области. Данная работа разбита на две части. В первой части рассматривается вопрос применения компьютеров к автоматическому доказательству теорем, во второй рассматриваются пакеты применяемые при компьютерных вычислениях.^ Часть 1. Доказательство теорем при помощи коспьютеров. В начале XX века в математике возник грандиозный проект: создание единой процедуры для доказательства математических теорем (исторически этот проект был совмещен с проектом по проверке непротиворечивости математики и построении ее полностью строгой формальной базы). В то время еще не существовало компьютеров, поэтому речь изначально шла об алгоритмической последовательности действий выполняемой человеком, тем не менее от такого алгоритма требовалось ровно то, что сегодня является трудовой нишей практически полностью занятой компьютерными программами: на каждом шаге исходя из уже полученных сведений должно было быть определено однозначно что нужно делать.Как известно, оказалось что существуют естественные ограничения для реализации такой программы наиболее известным из которых является теорема Геделя о неполноте (если формальная система включает в себя аксиомы Пеано, то есть аксиоматику натуральных чисел, то в такой системе либо можно для какого-то утверждения P доказать как P, так и отрицание P, либо существует какое-то утверждение Q, которое можно сформулировать в этой системе, которое нельзя ни доказать, ни опровергнуть (то есть доказать обратное) в рамках этой системы). Более того, как оказалось, для многих формальных систем (здесь это можно читать как «областей математики») не существует даже алгоритма позволяющего определить, является ли данное утверждение теоремой или нет (этот вопрос сильно отличается от вопроса о полноте, ответ на который дает теорема Геделя – здесь ставится вопрос о существовани алгоритма, выдающего «да», если утверждение можно доказать в данной формальной системе, и «нет», если такого доказательства нет, то есть может быть в этом случае утверждение неверное (то есть теоремой является его отрицание), а может быть оно и не доказывается и не опровергается). Про формальную систему, в которой существует алгоритм, определяющий для данного утверждения является ли оно теоремой, говорят что она разрешима. В противном случае, естественное, говорят что она неразрешима. Как было доказано в 1936-ом году Черчем, натуральные числа (с аксиоматикой Пеано) являются неразрешимой формальной системой. На первый взгляд несколько удивительно, но, как было показано Тарским (в начале 30-х годов, хотя из-за войны работы вышла только в 1948-м), действительная арифметика является разрешимой. Создав свою аксиоматику Евклидовой геометрии (которая, конечно же, соответствует естественному пониманию об этом объекте) Тарский доказал что и эта формальная система является разрешимой. В то же время уже проективная геометрия оказалась неразрешимой. Как оказалось в итоге, действительная арифметика, Евклидова геометрия, арифметика Пресбургера (натуральные числа, но в формальной системе не разрешены высказывания относительно умножения) и теория абелевых групп являются разрешимыми формальными системами. С другой стороны, арифметика натуральных чисел, топология, логики первого порядка с предикатами более чем от одной переменной, теория групп (не обязательно абелевых) являются неразрешимыми. Здесь стоит отметить, что многие задачи математики на том или ином этапе (возможно, после долгой творческой работы над ними людей) сводятся к утверждениям в действительной арифметике, даже если изначально они возникли в алгебре или теории чисел. В то же время, статья Тарского «A Decision Method for Elementary Algebra and Geometry» дает хороший алгоритм сведения любой задачи в действительной арифметике к вычислению конкретной формулы (может быть довольно сложной, но более чем посильной для современных компьютеров). Собственно, там приводится алгоритм того как преобразовать утверждение в действительной арифметики начинающееся с квантора существования к другому утверждению, уже не содержащему такового, и как несложно видеть такими преобразованиями можно свести любое утверждение содержащее много кванторов существования и всеобщности (и любые логические операции) к логической формуле без кванторов, которую потом можно проверить при всех значениях логических переменных. Конечно, утверждения вроде «для всех полиномов...» не формализуются таким способом, сам Тарский в предисловии к упомянутой выше статье пишет что теорема «любой полином нечетной степени имеет корень» не относится к заданной им формальной системе. Тем не менее, вероятно, программа строящая доказательства утверждения посредством сокращения кванторов в действительной арифметике (скорее всего, это было бы интересно и для теории абелевых групп, и для других «распространенных» формальных систем про которые известно что они разрешимы), могла бы оказать большую помощь в процессе нащупывания общего доказательства, давая доказательства для все более и более объемлющего класса частных случаев. Один из очень распространенных методов поиска доказательства у математиков такой: пробуют доказывать сначала во все более и более частных случаях, пока доказательство в достаточно частном случае не отыщется достаточно быстро, потом опираясь на него, «по его мотивам» пробуют находить доказательства во все более и более общих случаях, в обратном порядке возвращаясь к исходному утверждению. Программа реализующая «алгоритм Тарского» могла бы сразу давать хоть какое-то доказательство (возможно, изначально не очень простое для восприятия, но это уже поправимо человеком, упрощать доказательство процесс намного более простой нежели искать новое) как только мы ограничим число параметров каким-либо конечным числом. К сожалению, никакая из известных автору программ «автоматического доказательства теорем», включая и те что носят имя Тарского (например, вот этот пакет для Mathematica http://www.di.unito.it/~stefano/Mathematica-TarskiGames.nb), не выполняет большего чем преобразования логических выражений (точнее говоря, все что умеет делать автор с логическими выражениями посредством известных ему программ, это вычислять их значения, проверять всегда ли они истинны и т. пр.), процесс «сокращения кванторов» если где-то он и реализован, автором не обнаружен (поиск проводился достаточно долгий и интерес к объекту поиска наличествовал).^ Часть 2. Доказательство теорем при помощи компьютеров. Хотя автоматическое доказательство теорем пока имеет весьма ограниченное применение в «чистой» математике, компьютеры оказывают неоценимую помощь человеку в другом ее аспекте, в конкретных вычислениях. Собственно говоря, это и являлось основной мотивацией при их создании, можно сказать что «это их основное предназначение». Для математиков докомпьютерной эры вычисления являлись обычно тяжелой необходимостью, которая редко кому доставляла удовольствие. Широко известен следующий отрывок из письма (20 января 1903 года) Альберта Эйнштейна его будущей жене, тогда Милеве Марич^ ..Если хочешь замужества, ты должна будешь согласиться на мои условия, вот он