Теоретические основы оболочки для интерактивных систем верификации интуитивных математических доказательств


2018

Клещев А. С., Тимченко В. А.

Статьи в журналах

Онтология проектирования

Россия, Самара, ООО "Новая техника"

Т. 8, № 2(28)

219-239

1,037

2223-9537

Клещев А.С., Тимченко В.А. Теоретические основы оболочки для интерактивных систем верификации интуитивных математических доказательств // Онтология проектирования. 2018. Т.8. № 2(28). С.219-239. DOI: 10.18287/2223-9537-2018-8-2-219-239.

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

http://agora.guru.ru/scientific_journal/files/OD_2_2018.pdf