Год: 2018

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

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

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

Импакт-фактор издания:

Страна, город, издательство: Россия, Самара, ООО "Новая техника"

Импакт-фактор издания по РИНЦ: 1,037

ISSN / ISBN: 2223-9537

Название издания: Онтология проектирования

Выходные данные: Т. 8, № 2(28)

Тип публикации: Статьи в журналах

DOI: 10.18287/2223-9537-2018-8-2-219-239

Ссылки: