<<
>>

1.2.История создания систем автоматического поиска вывода

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

Отметим, что системы автоматического поиска натурального вывода в данном параграфе не рассматриваются. Такие системы будут подробно рассмотрены в следующем параграфе данной главы.

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

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

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

В 1834 году Ч. Бэббидж сконструировал цифровое счетное устройство. Особенностью этой машины была способность выполнять инструкции, считываемые с перфокарт. В 1842 году А. Лавлейс сделала описание работы аналитической машины Бэббиджа и составила первую программу для нее.

В дальнейшем стали создаваться машины, совершенствующие модель Бэббиджа. В 1855 году Дж. и Э. Шутц, базируясь на работах Ч.

Бэббиджа, построили свою механическую вычислительную машину. В 1869 году У.С. Джевонс, используя результаты Дж. Буля, построил усовершенствованную модель этой машины. В 1896

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

Промежуток времени между двумя мировыми войнами считается сегодня периодом рождения первого компьютера. В 1927 году в Массачусетском технологическом институте был изобретен аналоговый компьютер. В 1937 году Дж. Стибитц построил первую вычислительную машину на основе двоичной системы счисления.

В 1938-41 гг. К. Цузе предложил несколько моделей (Z1, Z2 и Z3) своей механической программируемой цифровой машины. Модель Z1 иногда называют первым в мире компьютером. В 1942 году в Университете штата Айова Дж. Атанасов и К. Берри создают первый в США электронный цифровой компьютер.

В России созданием «умных» машин занимались П.Д. Хрущов и А.Н. Щукарев. Создание вычислительных машин активно велось в советское время.

Появление первого компьютера открыло путь для развития механизируемых исчислений. В 50-е годы XX века были созданы две компьютерные программы, которые заложили два основных направления в области автоматического поиска доказательства.

Первая программа была создана М. Дэвисом на ламповом компьютере "Johniac". Эта программа могла доказать, что сумма двух четных чисел является четным числом - первое в истории доказательство математического утверждения, генерированное компьютером.

Вторая программа, которая могла доказывать ряд предложений из "Principia Mathematica"Б. Рассела и А.Н. Уайтхеда, была создана А. Невелом, Дж. К. Шоу и Г. Саймоном. Эта программа ориентировалась на человеческий способ рассуждений, пытаясь симулировать общие эвристические подходы и психологические моменты мышления.

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

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

В 1961 году М. Минский подвел итог этой дискуссии: «Кажется ясно, что программа решения реальных математических проблем должна комбинировать математические рассуждения... с эвристическими рассуждениями Невела, Шоу и Саймона».

В 1958-63 гг. Х. Ван предложил несколько версий своей первой логикоориентированной программы фирмы IBM по автоматическому доказательству. Это был большой шаг вперед: его программа могла доказывать около 350 предложений «Principia Mathematica» для чистого исчисления предикатов с равенством.

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

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

В 1960 году эту проблему решил Д. Правиц посредством механизма, названного унификацией. Позже был предложен унифицирующий алгоритм.

Независимо от этого над доказательствами математических утверждений в национальной лаборатории Аргонны работали Д. Карсон, Дж. Робинсон и Л. Уос. Ученые поставили перед собой задачу разработать такой принцип, в котором бы объединились различные методы в одно общее логическое правило.

В 1963-1965 гг. такое правило было найдено, и Дж. Робинсон публикует свою работу "A machine oriented logic, based on the resolution principle" [Robinson]. С тех пор метод резолюции прочно вошел в практически любую образовательную программу по логике и информатике.

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

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

К первому лагерю принадлежали ученые национальной лаборатории Аргонны под руководством Л. Уоса и группа под руководством Б. Мелтцера в университете Эдинбурга. В 1965-75 гг. они предложили десятки усовершенствованных стратегий поиска вывода.

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

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

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

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

В 60-е годы XX века Л. М. Нортон предложил эвристический прувер для теории групп, а А. Невинс - алгоритм, разрабатываемый на базе «человекоориентированной

логики». Результаты данных программ оказались не достижимыми для резолюционных процедур того времени. Здесь можно отметить работу исследователей университета Техаса, развивавших специализированные методы доказательства для конкретных областей математики.

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

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

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

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

Системы доказательства теорем разбиваются на два больших лагеря. Первый лагерь - это системы интерактивного доказательства теорем (proof checker), другое название этих систем - редакторы доказательств.

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

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

Примером редактора доказательств является система AUTOMATH, которая создана для проверки математических доказательств. В этой системе доказывается значительная часть теорем из чистой математики. Однако запись доказательств в AUTOMATH, как правило, в 10-20 раз длиннее, чем в естественном языке.

Из отечественных работ можно привести программу DEDUCTIO, разработанную А.В. Смирновым при участии А.Е. Новодворского [Смирнов-мл]. Эта программа позволяет работать не только с одной стандартной логической системой, но и делать выбор из довольно широкого списка известных систем. Программа предоставляет также пользователю возможность описать некоторую собственную систему, после чего она автоматически начинает ее поддерживать.

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

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

Разработки программ в области автоматической дедукции проводятся в целом ряде крупных мировых научно-исследовательских центров. В национальной лаборатории Аргонны создана программа OTTER, основанная на теории резолюций. OTTER является последним продуктом в цепи систем (AURA, ITP), которые были созданы под руководством Л. Уoca. Программа создана для поиска доказательств для классической логики предикатов первого порядка с равенством, написана на языке С,

занимает примерно 180 Кб и способна оперировать большим количеством дизъюнктов (миллиардами), что показывает ее высокую эффективность.

В Кембридже создана программа автоматической дедукции Isabelle. В Карнеги- Меллон университете создана программа для автоматического доказательства теорем для логики высоких порядков. В лаборатории KAKEHI и Университете WASEDA создана программа автоматического доказательства для секвенциального исчисления

В отечественной науке подобные программы начали создаваться также достаточно давно. В 60-е годы XX века под руководством Шанина Н.А. разработан алгоритм машинного поиска логического вывода [Шанин и др.]. Программа, реализованная по этому алгоритму, ищет вывод в классическом секвенциальном исчислении высказываний и перерабатывает его далее в натуральный вид.

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

Надо отметить, что концентрация внимания исследователей в области автоматического вывода на этих популярных дедуктивных методах не случайна и обусловлена, в первую очередь, практическими соображениями. Так, например, исследования в области теории резолюций тесно связаны с языками логического программирования (в частности, типа Пролог), где выводы основаны на методе резолюций, который изначально являлся составной частью Пролога [Братко].

Еще одной причиной такой ситуации является факт достаточно успешного практического применения неклассических логик в рамках различных проектов тестирования аппаратных средств [Bochmann], нередко спонсирующихся ведущими производителями таких средств (например, Intel).

На сегодняшний день самым распространенным и эффективным методом в данной области является метод тестирования моделей. В данном методе для описания моделей аппаратных средств используется дедуктивный аппарат, чаще всего основанный на модальной или временной логике, семантика для которых чаще всего строится в форме аналитических таблиц [Bochmann], [Bolotov &Fisher].

<< | >>
Источник: ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004. 2004

Еще по теме 1.2.История создания систем автоматического поиска вывода:

  1. ШАНГИН ВАСИЛИЙ ОЛЕГОВИЧ. АВТОМАТИЧЕСКИЙ ПОИСК НАТУРАЛЬНОГО ВЫВОДА В КЛАССИЧЕСКОЙ ЛОГИКЕ ПРЕДИКАТОВ. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2004, 2004
  2. Звездное небо и моральный закон: очерк истории пифагорейской идеи
  3. Поиск определения воли
  4. В поиске мыслительного феномена повторения одинакового
  5. 2. Изложение учения ранних пифагорейцев: поиск источников концептов логики и зла
  6. Терминологические и методологические проблемы
  7. Оглавление
  8. Цели, основные понятия и композиция исследования
  9. ВВЕДЕНИЕ
  10. Эстетизация (трактовки) воли
  11. Введение
  12. Ранние пифагорейцы как часть досократической философии
  13. Воля господина в трактовке Гегеля
  14. Эврит
  15. АФОНАСИНА Анна Сергеевна. ПСЕВДОПИФАГОРИКА: ТИМЕЙ ЛОКРСКИЙ О ПРИРОДЕ КОСМОСА И ДУШИ. ДИССЕРТАЦИЯ на соискание ученой степени кандидата философских наук. Новосибирск - 2013, 2013
  16. Лечич Никола Добривоевич. Общий источник генезиса логики и теории зла в идеях ранней пифагорейской школы. Диссертация на соискание ученой степени кандидата философских наук. Москва - 2016, 2016
  17. Бугай Дмитрий Владимирович. Прокл Диадох как комментатор Платона. Диссертация на соискание учёной степени кандидата философских наук. Москва - 2001, 2001
  18. Оглавление