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

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