Игошин Математическая логика и теория алгоритмов (1019110), страница 99
Текст из файла (страница 99)
Исторически так оно и произошло: первые теоремы, доказанные компьютером, были теоремы формализованного исчисления высказываний. В логике и компьютерных науках стали говорить об автоматическом, или механическом, или машинном доказательстве теорем. В настоящем параграфе сначала будет рассказано об одной из первых попыток применить компьютер для поиска доказательств математических теорем — о компьютерной программе «Логик-теоретик», созданной в первой половине 1950-х гг. в США. Программа Логик-теореппг» и программы, близкие к ией.
В 1957 г. известные американские специалисты по информатике А.Ньюэлл, Г.Саймон, Дж. Шоу 19.181 сообщили, что при помощи разработанной ими программы «Логик-теоретик» на электронно-вычислительной машине 1ВМ-704 получены доказательства для ряда (38) теорем формализованного исчисления высказываний, содержащихся в известном труде Б.Рассела и А.Уайтхеда «Рг1пс1р)а МагЬегпаг)са» (1925 — 1927). В память машины с самого начала было помещено пять аксиом исчисления высказываний Рассела — Уайтхеда и три правила вывода.
Кроме того, программа составлена так, что каждая из уже доказанных теорем оставалась в памяти машины и могла использоваться для дальнейших доказательств. Алгоритм поиска доказательств имел так называемый эвристический характер. Под «эвристиками» здесь понимается выявление общих правил, позволяющих решить поставленную задачу без необходимости систематического перебора всех потенциально существующих вариантов.
С помощью своей программы «Логик-теоретик» ее создатели попытались смоделировать процесс поиска такого доказательства человеком. В качестве доводов, подтверждающих, что программа моделирует человеческое мышление„приводились результаты сравнения записей доказательств теорем в виде программы с записями рассуждений «думающего вслух> человека. В основу алгоритма программы «Логик-теоретик» были положены следующие три эвристических метода: метод подстановки, метод отделения (шодиз ропепз) и метод целеобразования. Метод подстановки предназначен для поиска среди исходных аксиом и ранее доказанных теорем такой, которую требуется доказать в данный момент.
При этом программа пытается определить, какие переменные или подформулы в уже имеющейся формуле нужно заменить и на какие формулы, чтобы получить ту формулу, которую требуется доказать. Для этого программа выполняет подстановки одних формул в другие и осуществляет равносильные преобразования формул на основании наличия в своей памяти основных равносильностей алгебры высказываний (коммутативность, ассоциативность, идемпотентность конъюнкции и 398 дизъюнкции, законы поглощения и де Моргана, выражение импликации через дизъюнкцию и отрицание и т. п.). Сам поиск доказательства той или иной теоремы (формулы) осуществляется методами отделения и целеобразования.
метод оглделения состоит в том, что доказываемая формула заменяется более простой, доказав которую мы затем доказываем исходную формулу. Если à — теорема, подлежащая доказательству„то машина ищет аксиому или уже доказанную теорему вида 6 -» Е Затем делается попытка решить подзадачу — доказать теорему 6. Если она окажется доказанной, то из двух теорем 6 и 6-» Г по правилу МР (гподцз ропепа) оказывается доказанной и теорема Г. Метод целеобразовалия предусматривает многократное использование метода отделения.
Например, при необходимости доказать теорему Г» Н машина ищет ранее доказанную теорему вида Г-» 6. Если такая теорема найдена в памяти, то перед машиной встает новая подзадача — доказать теорему 6 — » Н. Если и ее доказательство найдено, то из этих импликаций выводится требуемая теорема à — » Н. Таким образом, общая идея алгоритма поиска доказательства заданной теоремы Г состоит в восстановлении цепочки-доказательства так называемым обратным ходом, отправляясь от самой формулы Ги восстанавливая ее вплоть до уже доказанных теорем или до аксиом. Процесс поиска предшествующих формул исключительно неоднозначен и, как бы он ни бьи организован, носит переборный характер.
И успешность выбора той или иной формулы не может быть оценена локально, в момент выбора. Поэтому программа вынуждена перебирать варианты, заходить в тупики, проходить циклы, прежде чем она сможет найти правильный путь решения. Повышение эффективности процесса вывода — центральная проблема всех автоматизированных систем дедуктивного вывода. Как уже отмечено, с помощью этой программы была доказана часть теорем исчисления высказываний из книги Рассела и Уайтхеда «Рппс(р)а Маг)тешат)са». Например, первая из этихтеорем имеет вид: (Г-» — Г) — » — Е Эту теорему машина доказала в четыре шага и напечатала результат на выводном устройстве через 10 с после начала работы программы. Доказывая теорему (Г ч (6 ~ Н)) » -» ((Г ~ 6) ~ Н), машина через 23 мин после начала работы объявила об исчерпании возможностей данной программы.
Простая на вид, но сложная для доказательства теорема — (Г-+ 6) -+ — Г была доказана через 12 мин в пять этапов. На этом примере, кстати, наглядно лемонстрируются принципиальные преимушества эвристических методов: если бы та же машина использовала не эвристические, а лишь чисто переборные методы, то лля доказательства последней теоремы ей потребовалось бы несколько тысяч лет машинного времени 19.24, с. 253]. 399 Создатели программы «Логик-теоретик» показали также, что их программа может не только доказывать известные теоремы исчисления высказываний, но и может выдвигать новые теоремы и стремиться к их доказательству. Аналогичные исследования по проблеме машинного поиска логического вывода велись и в Советском Союзе.
Наибольшую известность получили исследования Н.А. Шанина и его сотрудников. В 19.281 решается такая проблема: в заданном конкретном формализованном исчислении высказываний требуется составить алгоритм, выясняющий для любых формул Гь .6и ..., Г„ и б этого исчисления, выводима ли формула 6 из формул У;, Гь ..., Г„, и при утвердительном ответе на этот вопрос искомый алгоритм должен строить (и это в проблеме главное) вывод формулы 6 из формул Рь У~, ...„Г . Машинная программа, реализующая удовлетворяющий указанным требованиям алгоритм, работала на машине «Урал-4» — одной из лучших советских электронно-вычислительных машин первой половины 1960-х гг.
Отметим также работы американского программиста Ван Хао [9.51, который в 1959 г. составил три программы для доказательства теорем исчисления высказываний и исчисления предикатов, реализовав их на машине 1ВМ-704. Первая из них позволила машине за 37 мин доказать более двухсот теорем из первых пяти глав упоминавшейся книги Рассела и Уайтхеда «РПпс1р1а Маг)тета11са», причем 12/13 этого времени было израсходовано на ввод и вывод данных, так что время, потраченное собственно на доказательство, составило менее 3 мин. По второй программе машина сама составляла формулы исчисления высказываний и выбирала из них нетривиальные теоремы, строя их доказательства.
В течение 1 ч было образовано и проверено около 14 тыс. формул, из которых выделено около тысячи теорем. Наконец, третья программа предназначалась для доказательства более 150 теорем следующих пяти глав «Рппс)р1а Ма11зегпа11са» для исчисления предикатов с равенством. В течение 1 ч машина нашла доказательства для 85 теорем, которые были стройнее и короче доказательств, приведенных Расселом и Уайтхедом. Позже появились программы, которые для доказательства теорем формализованного исчисления высказываний стали эффективно использовать метатеорию, т.е.
теоремы о теоремах формальной теории. Первой такой программой стала программа французского математика Ж.Питра, созданная в 1966 г. Использование метатеорем позволило осуществить наибольший глобальный обзор поиска и сконцентрировать внимание на наиболее важных направлениях, не загружая память несущественными результатами. Программа Ж. Питра работает с шестью формализованными исчислениями высказываний, базирующимися на системах аксиом Рассела, Лукашевича. Гильберта, Бернея и Шеффера.
Она отыскивает все основные теоремы, причем иногда дает для них оригинальные доказательства. Про- 400 грамма умеет работать и на уровне предположений: ей задается конкретное выражение и требуется его доказать. Достоинство программы в том, что с ее помощью удалось доказать некоторые теоремы, которые не смог доказать ее создатель.
Вот суждение об этом самого Лукашевича: Нужно быть очень опытным и искусным в построении логических доказательств, чтобы вывести закон коммутативности (Р— > (Ц вЂ” ~ Я)) -э (Д -э (Р— > 11)) или даже закон упрощения Р— > (Π— > Р)». Программа Ж. Питра эффективно доказывает оба этих утверждения в рассматриваемой аксиоматике. Метод резолюций для доказательства теорем исчисления высказываний н нсчнслениа преднкатов. Этот метод, разработанный американским математиком Дж. Робинсоном 19.201 в 1965 г., способствовал значительному прогрессу в автоматическом доказательстве теорем.
Корни этого метода лежат в исследованиях известного французского логика Ж. Эрбрана, который в 1930 г. доказал очень важную теорему, послужившую основой для предложенного им механического метода доказательства теорем. (Эрбран погиб в 1931 г. в возрате 23 лет в Альпах во время восхождения на одну из вершин.) Как известно, в исчислении предикатов каждая теорема является обшезначимой формулой (т.е. истинной во всякой интерпретации). Следовательно, необщезначимая формула не может быть теоремой.
Так вот, Эрбран предложил алгоритм, устанавливающий необщезначимость формулы и, следовательно, ее недоказуемость. Точнее, он предложил алгоритм для нахождения интерпретации, не удовлетворяющей данной формуле, т.е. интерпретации, на которой формула превращается в ложное высказывание. Если заданная формула в действительности была общезначимой, то такой интерпретации не находилось, и алгоритм Эрбрана устанавливал этот факт за конечное (может быть, большое) число шагов.
Если же заданная формула в действительности не была общезначимой, то алгоритм Эрбрана не мог установить этого факта за конечное число шагов. Таким образом, при отсутствии в то время вычислительных машин алгоритм Эрбрана оказался весьма трудоемким для ручных вычислений и не получил практического применения. С появлением вычислительных машин интерес к механическому доказательству теорем резко возрос.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
