Внутренняя модель математической практики для систем автоматизированного конструирования доказательств теорем




Скачать 173.74 Kb.
Дата02.08.2016
Размер173.74 Kb.




скусственныи интеллект


УДК 681.3.057.51-7.311.17

ВНУТРЕННЯЯ МОДЕЛЬ МАТЕМАТИЧЕСКОЙ

ПРАКТИКИ ДЛЯ СИСТЕМ АВТОМАТИЗИРОВАННОГО

КОНСТРУИРОВАНИЯ ДОКАЗАТЕЛЬСТВ ТЕОРЕМ1

Ч. 1. Общее описание модели

Т. Л. Гаврилова, А. С. Клещев

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



ВВЕДЕНИЕ

Проблема автоматизации процесса конструи­рования правильных доказательств математиче­ских теорем является актуальной и для математи­ческого образования (обучения студентов доказа­тельству теорем), и для математической практики (доказательства теорем профессиональными мате­матиками). В работе [1] показано, что наиболее перспективны не автоматические, а автоматизиро­ванные (человеко-машинные) системы констру­ирования доказательств. Однако до сих пор и те, и другие системы основывались на моделях матема­тической логики, предназначенных для исследова­ния проблем метаматематики [2—5]. Именно по­этому эти системы служат целям обучения скорее математической логике, чем доказательству мате­матических теорем. Такие модели неадекватно представляют математическую практику и потому неудобны для математиков и студентов, работаю-

______________

1 Работа выполнена при финансовом содействии програм­мы № 16 Президиума РАН, проект «Теоретические основы ин­теллектуальных систем, основанных на онтологиях, для интел­лектуальной поддержки научных исследований» и программы № 16 ОЭММПУ РАН, проект «Синтез интеллектуальных сис­тем управления базами знаний и базами данных».

32

щих с системами автоматизированного констру­ирования доказательств (САКД). Дальнейшее раз­витие САКД может быть связано с разработкой бо­лее адекватной модели математической практики [1]. Такую модель можно представить в виде ком­бинации двух моделей: внутренней модели — фор­мальной системы, в рамках которой САКД осу­ществляет конструирование полных доказательств по информации, получаемой от математика, и внешней модели, в рамках которой математик уп­равляет процессом конструирования интуитивных доказательств. Внутренняя модель отвечает за пра­вильность сконструированных доказательств, а внешняя имитирует привычную для математиков систему понятий и представлений математической практики. Одним из недостатков существующих САКД как раз и является отсутствие в них внеш­ней модели и использование в этом качестве внут­ренней модели.

В настоящем цикле статей на основе требова­ний к внешней и внутренней моделям математи­ческой практики предлагается внутренняя модель для САКД. Данная статья является первой из цик­ла. В ней определяются требования к внешней и внутренней моделям математической практики, и дается общее описание внутренней модели.

CONTROL SCIENCES № 4 • 2006


ИСКУССТВЕННЫЙ ИНТЕЛЛЕКТ

1. ВНЕШНЯЯ И ВНУТРЕННЯЯ МОДЕЛИ МАТЕМАТИЧЕСКОЙ ПРАКТИКИ

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



Внешняя модель математического диалекта (ММД) — это язык, на котором САКД представ­ляет математику математические знания. Этот язык должен быть достаточно богат, чтобы пред­ставленные на нем математические знания выгля­дели привычно и понятно для математика (не тре­бовали изучения какого-либо неизвестного ему языка). Он должен быть расширяемым, как и ма­тематический диалект, а утверждения на нем должны интерпретироваться однозначно [1]. Кро­ме того, этот язык должен имитировать разделение математического диалекта на неформальную (ес­тественно-языковую) и формальную части. Внут­ренняя модель математического диалекта — это формальный язык, на котором математические знания представляются в САКД. Он также должен быть расширяемым, утверждения на нем также должны однозначно интерпретироваться. Но в от­личие от внешней модели, этот язык не должен имитировать разделение математического диалек­та на неформальную и формальную части, а в его описании должны быть явно выделены формаль­ный синтаксис, контекстные условия, логическая семантика и прагматика.

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

Внешняя модель способов рассуждения — это множество описаний способов рассуждения, пред­ставленных на языке внешней модели и доступных математику в процессе конструирования доказа­тельств теорем с помощью САКД. Внутренняя мо­дель способов рассуждения — это множество описа­ний тех же способов рассуждения, но представлен-

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



Внешняя модель доказательства теоремы — это текст интуитивного доказательства этой теоремы [1], представленный на языке внешней модели. Внутренняя модель доказательства теоремы — это структура данных САКД, представляющая полное доказательство этой теоремы [1]. Правильность доказательства теоремы (в том числе и интуитив­ного) должна следовать из возможности констру­ирования ее полного доказательства. Система долж­на поддерживать соответствие между внутренней и внешней моделями доказательств.

2. ОБЩЕЕ ОПИСАНИЕ ВНУТРЕННЕЙ МОДЕЛИ МАТЕМАТИЧЕСКОЙ ПРАКТИКИ

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



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

Расширяемость синтаксиса достигается благо­даря средствам САКД, позволяющим описать (конкретный или абстрактный) синтаксис каждой новой конструкции (терма или формулы) языка и добавить это описание к описанию синтаксиса языка ММД. Заметим, что с этой точки зрения описание синтаксиса термов и формул можно рас­сматривать как расширение пустых множеств тер­мов и формул языка ММД. Если САКД предостав­ляет средства описания конкретного синтаксиса, то в ее состав должен входить синтаксически уп­равляемый синтаксический анализатор, напри­мер, YACC [6]; если же в САКД имеются средства описания абстрактного синтаксиса, то в ее состав должен входить универсальный структурный редак­тор, (см., например, работу [7]). Рассмотрим слу­чай, когда описывается только конкретный син­таксис языка ММД.

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


ИСКУССТВЕННЫЙ ИНТЕЛЛЕКТ


которых следует корректность этой конструкции. Проверка контекстных условий второго класса со­стоит в автоматическом (или автоматизирован­ном) доказательстве этих предложений.

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

Язык ММД состоит из трех подъязыков: языка представления математических утверждений, язы­ка представления пропозициональных утвержде­ний и метаязыка. Математические знания пред­ставляются на первом из них. Пропозициональ­ные утверждения не могут быть представлены на этом языке, поэтому для их представления вводит­ся специальный язык. Математические принципы и утверждения о синтаксических преобразованиях математических формул (например, правила диф­ференцирования или взятия неопределенного ин­теграла) также не могут быть представлены на первом подъязыке, поэтому для их представления также вводится специальный язык (метаязык). Средства расширения имеет только язык предс­тавления математических утверждений. Метаязык, надстроенный над ним, расширяется автоматиче­ски при его расширении. Язык представления пропозициональных утверждений расширяемым не является.

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


34

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



Экстенсионалом определения будем называть множество, состоящее из единственного предло­жения, имеющего форму равенства между опреде­ляемым термином и термом, задающим значение этого термина. Экстенсионалом пропозициональной тавтологии будем называть множество предложе­ний (конкретизации), полученных из этой тавто­логии заменой вхождений всех пропозициональ­ных переменных на произвольные предложения. Экстенсионалом математического утверждения (в частности, математической аксиомы) будем на­зывать множество предложений (конкретизации), полученных из этого утверждения заменой вхож­дений всех свободных переменных на произволь­ные, но «подходящие» термы без свободных пе­ременных. Экстенсионалом метаматематического утверждения (в частности, метаматематической аксиомы) будем называть объединение экстенси­оналов всех математических утверждений (конк­ретизации), полученных из этого метаматематиче­ского утверждения заменой вхождений всех син­таксических переменных на произвольные, но «подходящие» термы без свободных переменных или предложения. Экстенсионалом ядра (оболочки) внутренней модели знаний будем называть объ­единение экстенсионалов всех элементов этого яд­ра (оболочки). Объединение экстенсионалов ядра и оболочки внутренней модели знаний и есть мно­жество тех предложений, про которые известно, что они истинны.

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



CONTROL SCIENCES № 4 • 2006

ИСКУССТВЕННЫЙ ИНТЕЛЛЕКТ


рое предложение, имеющее форму импликации и принадлежащее объединению экстенсионалов яд­ра и оболочки; если Modus ponens используется для декомпозиции, т. е. требуется доказать предло­жение, совпадающее с заключением этой импли­кации, то это доказательство сводится к доказа­тельству условий этой импликации; если же Modus ponens используется для вывода, т. е. истинны ус­ловия этой импликации (установлено, что они принадлежат объединению экстенсионалов ядра и оболочки), то заключение этой импликации счи­тается доказанным. Доказательство предложения пусто, если это предложение входит в объедине­ние экстенсионалов ядра и оболочки.

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

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

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

ПРОБЛЕМЫ УПРАВЛЕНИЯ № 4 • 2006

зования правила вывода Modus ponens (для де­композиции или для вывода), к выбору в модели знаний способа рассуждения на этом шаге и к под­бору посылок для применения правила вывода Modus ponens.



ЗАКЛЮЧЕНИЕ

Результаты работы состоят в следующем. Опре­делены требования к внешней и внутренней моде­лям математической практики для САКД. Дано общее описание внутренней модели, введен ряд определений, которые будут использованы в по­следующих статьях этого цикла.



ЛИТЕРАТУРА

  1. Гаврилова Т. Л., Клещев А. С. Анализ подходов к решению
    проблемы правильности математических знаний // Про­
    блемы управления. — 2005. — № 3. — С. 13—19.

  2. Чень Ч., Ли Р. Математическая логика и автоматическое
    доказательство теорем. — М.: Наука, 1983. — 320 с.

  3. ETPS: A System to Help Students Write Formal Proofs /
    B. Andrews Peter, M. Bishop, E. Brown Chad, et al. // Re­
    search Report No. 03-002, April 2003 (Departvent of Mathe­
    matical Sciences. Carnegie Mellon University).

  4. JProver. Integrating Connectoin-Based Theorem Proving into
    Interactive Proof Assistants / Schmitt S., Lorigo L., Kreitz C.
    and Nogin A. // International Joint.

  5. Ulrich Endriss. The Interactive Learning Environment WinKE
    for Teaching Deductive Reasoning // First International Con­
    gress on Tools for Teaching Logic. King's College. — London,
    September 6, 2000.

  6. Stepheh C. Johnson. Yacc: Yet Another Compiler-Compiler
    .

  7. Орлов В. А., Клещев А. С. Многоцелевой банк знаний. Ч. 3.
    Концепция универсального Редактора ИРУО. — Влади­
    восток: НАЛУ ДВО РАН, 2003. — 28 с. es/publ/186_3.rtf>.

9(4232) 31-40-01, 31-04-24

e-mail: gavrilov@iacp.dvo.ru

kleschev@iacp.dvo.ru
35


База данных защищена авторским правом ©uverenniy.ru 2016
обратиться к администрации

    Главная страница