Модели и методы автоматической проверки решений задач тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат наук Кацман Виктор Игоревич

• Кацман Виктор Игоревич
• кандидат наук
• 2022

Оглавление диссертации кандидат наук Кацман Виктор Игоревич

ВВЕДЕНИЕ

ГЛАВА 1. Задачи на преобразования лямбда-термов, процесс их решения и анализ существующих методов проверки решений таких задач

1.1 Задачи на преобразования лямбда-термов

1.2 Задачи на оперирование формулами

1.3 Роль автоматической проверки решений задач в автоматизации образовательного процесса

1.4 Альтернативные подходы к записи решений

1.5 Существующие методы автоматической проверки

1.5.1 Автоматическая проверка по ответу

1.5.1.1 Методы, основанные на нормализации

1.5.1.2 Методы, основанные на вычислительных экспериментах

1.5.1.3 Плюсы и минусы подхода

1.5.2 Автоматическая пошаговая проверка

1.6 Игрофикация процесса решения задач

1.7 Выводы по главе

ГЛАВА 2. Язык для записи цепочек преобразований и их проверка методом эффективного перебора правил

2.1 Модель проверки решения задачи как цепочки преобразований

2.2 Язык записи цепочек преобразований

2.3 Взвешенный орграф преобразований

2.4 Эвристика для оценки расстояния ^и, V)

2.4.1 Эвристика для символьных выражений

2.4.2 Эвристика для логических утверждений

2.5 Алгоритм БЛ8С для проверки переходов

2.6 Проблемы предложенного алгоритма

2.7 Выводы по главе

ГЛАВА 3. Метод вычислительных экспериментов для проверки корректности преобразований

3.1 Алгоритм автоматической проверки равенств

3.2 Алгоритм автоматической проверки неравенств

3.3 Экспериментальные оценки

3.4 Выводы по главе

ГЛАВА 4. Метод проверки корректности и тривиальности цепочек преобразований

4.1 Операции с нулевым весом

4.2 Сокращенный взвешенный орграф преобразований

4.3 Алгоритм автоматической проверки 8ТЕРТЕЯ8Т

4.4 Пример работы алгоритма

4.5 Экспериментальные оценки

4.6 Выводы по главе

ГЛАВА 5. Модели игрофикации процесса решения задач

5.1 Общий подход к игрофикации

5.2 Модель «правило - способ применения»

5.3 Модель «место применения - правило»

5.4 Модель «проверка решения»

5.5 Выводы по главе

ГЛАВА 6. Разработка и опытная эксплуатация

6.1 Хронология разработки

6.2 Используемые технологии

6.3 Оценка удобства разработанного языка и применимости алгоритма проверки

6.4 Эксплуатация программных комплексов для игрофикации

6.5 Оценка экономии преподавательского времени

6.6 Выявленные недостатки исследования

6.7 Выводы по главе

ЗАКЛЮЧЕНИЕ

ЛИТЕРАТУРА

ПРИЛОЖЕНИЕ 1. ГРАММАТИКА РАССМАТРИВАЕМЫХ В РАБОТЕ СИМВОЛЬНЫХ ВЫРАЖЕНИЙ

ПРИЛОЖЕНИЕ 2. ГРАММАТИКА РАССМАТРИВАЕМЫХ В РАБОТЕ ЦЕПОЧЕК ПРЕОБРАЗОВАНИЙ

ПРИЛОЖЕНИЕ 3. ТАБЛИЦА СИНТАКСИЧЕСКИ УПРЯВЛЯЕМОГО ПЕРЕХОДА БТЕРТ

ПРИЛОЖЕНИЕ 4. КЛЮЧЕВЫЕ ЭЛЕМЕНТЫ АВТОМАТОВ СИНТАКСИЧЕСКОГО РАЗБОРА ВЫРАЖЕНИЙ В ЯЗЫКЕ БТЕРТ

ПРИЛОЖЕНИЕ 5. КЛЮЧЕВЫЕ ЭЛЕМЕНТЫ СИНТАКСИЧЕСКОГО РАЗБОРА ЦЕПОЧЕК ПРЕОБРАЗОВАНИЯ В ЯЗЫКЕ БТЕРТ НА ДИАГРАММЕ ПОТОКОВ ДАННЫХ

ПРИЛОЖЕНИЕ 6. АКТ ВНЕДРЕНИЯ

ВВЕДЕНИЕ

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

Лямбда-термами могут являться:

1. Символьные выражения, содержащие элементарные функции вещественной переменной;

2. Логические утверждения - равенства и отношения порядка символьных выражений.

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

Введение диссертации (часть автореферата) на тему «Модели и методы автоматической проверки решений задач»

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

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

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

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

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

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

Степень разработанности темы исследования. Наибольший вклад в формирование и развитие методов проверки эквивалентности À-термов, автоматического сравнения символьных выражений и использовании автоматизации в образовании оказали A. Church, A. Tarski, A. Turing, R.J.Back, T.Auvinen, L.Bazzini, M.Cerulli, G.Chiappinni, F.Arzarello, L.Linchevski, L.Manilla, B.Pedemonte, D.Richardson, H.Rogers, A.Sfard, M.Tirronen, V.Tirronen, S.Willman, S.Wallin, S. Wolfram, А.А.Марков, И.Л.Артемьева, С.Н.Поздняков, С.Е.Рукшин, Ю.В.Матиясевич.

Задача проверки отношения эквивалентности À-термов в общем случае является неразрешимой. Однако, для большинства рассматриваемых в работе символьных выражений и логических утверждений существуют способы проверки их эквивалентности, основанные на нормализации, алгоритме Тарского, либо методах вычислительных экспериментов (используются в образовательных платформах Coursera, Stepic и других). Неразрешимость проверки эквивалентности в общем случае следует из теоремы Ричардсона; методы вычислительных экспериментов вероятностные и приводят к

большому числу ошибок в случае выражений с Гузкой областью определения, вероятность попадания в которую точкой из равномерного распределения в шаре с центром в начале координат и радиусом, равным наибольшей константе в выражении, меньше 1%.

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

В целом методы автоматической пошаговой проверки решений на сегодняшний день изучены явно недостаточно. Большинство результатов есть лишь для очень узких предметных областей, например, построении геометрических примитивов в «EucHdea», простейших задач на знания арифметики в «GeoGebra» или задач на изучение центробежной силы и равномерного движения по окружности. Очень существенный вклад в развитие области внесло подробное описание концепции «структурированного вывода» для большого числа типов выкладок. Эта концепция лежит в основе системы «eMathStudio», нацеленной на проверку структурированных решений на преобразование формул. Однако системные подходы к автоматизации проверки корректности и тривиальности преобразований над выражениями и логическими утверждениями отсутствуют, что предопределило и обусловило цель и задачи данного диссертационного исследования.

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

Достижение поставленной цели потребовало решения следующих основных задач:

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

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

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

4. Проведение опытной эксплуатации в учебном процессе с участием студентов младших курсов и оценка эффективности разработанных моделей и алгоритмов.

Объектом исследования являются аппликации и применения правил

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

Предметом исследования являются алгоритмы автоматической

проверки корректности и тривиальности логических утверждений, а также

способы удобной записи преобразований над ними.

Основные положения, выносимые на защиту:

1. Алгоритм автоматической проверки корректности и тривиальности переходов в цепочке преобразований на основе комбинации методов эффективного перебора правил и вычислительных экспериментов.

2. Алгоритмы автоматической проверки равенств и неравенств символьных выражений на основе вычислительных экспериментов.

3. Язык STEPT для записи цепочек преобразований над символьными выражениями и логическими утверждениями, удобный для записи решений задач на преобразование формул.

4. Модели игрофикации процесса решения учебных задач на развитие навыков оперирования формулами «правило - место применения», «место применения - правило» и «проверка решения».

Научная новизна:

1. Разработан алгоритм проверки равенств символьных выражений с Гузкой областью определения за счет применения метода вычислительных экспериментов в комплексной области и адаптивного подбора порогов вероятностной проверки.

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

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

утверждений в ходе решения задач на развитие навыков оперирования формулами.

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

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

Методы исследований сочетают в себе методы дискретной математики, оптимизации, теории алгоритмов, теории формальных грамматик и языков программирования, методы проектирования программных комплексов, методы объектно-ориентированного и параллельного программирования, а также методы теории вероятностей и математической статистики. Разработанные методы и алгоритмы реализованы на языках C++ и Kotlin; реализованный программный комплекс использует сервер на основе технологии Spring Boot и базу данных PostgreSQL, эксперименты анализировались с использованием языков Python и R, а также Excel; в ходе работы использовались IDE IntelliJ Idea, PyCharm и RStudio, а также Jupyter Notebook; временные замеры проводились на машине 2,3 GHz Quad-Core Intel Core i5.

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

Практическая значимость диссертационной работы состоит в создании общедоступных программных комплексов:

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

2. Решения учебных задач на повышение навыков оперирования формулами в игровой форме.

В частности, разработаны www.mathhelper.online и www.mathhelper.space/twf/prototype/demo.html, позволяющие автоматически проверять решения задач, а также решать задачи в стандартном и игровом форматах.

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

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

Апробация результатов работы. Основные положения диссертационной работы докладывались и обсуждались на следующих конференциях: Международная конференция по преподаванию информатики, компьютерные инструменты в преподавании ISSEP-2018, Международная конференция «Информатизация непрерывного образования» ICE-2018, Международная конференция «Передовые технологии в аэрокосмической отрасли, машиностроении и автоматизации» MIST-2019, Международный форум «Цифровые технологии в инженерном образовании» ITEE-2019, СПИИРАН семинар «Информатика и автоматизация» 2021, семинар «Алгоритмическая математика» ЛЭТИ 2021.

Внедрение результатов работы. Результаты диссертационного исследования неоднократно использовались в Политехническом и Электротехническом университетах Санкт-Петербурга для автоматической проверки решений задач по теории множеств, логическим исчислениям, комбинаторике и теории чисел, а также для игрофикации процесса решения учебных задач из тех же областей. Суммарно с 2018 по 2021 год разработанными программными комплексами воспользовались более 300 студентов и решили более 2000 задач.

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

Публикации. По теме диссертации опубликовано 7 работ, в том числе 3 из них в журналах списка рекомендованных ВАК и 2, входящие в международные реферативные системы цитирования и базы данных Scopus и Web of Science.

Личный вклад автора. Содержание диссертации и выносимые на защиту положения отражают личный вклад автора в предметную область

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

Объем и структура работы. Диссертация состоит из введения, 6 глав, заключения и 6 приложений. Основной текст содержит 125 страниц с 46 рисунками и 7 таблицами. Список литературы содержит 140 наименований на 10 страницах.

ГЛАВА 1. Задачи на преобразования лямбда-термов, процесс их решения и анализ существующих методов проверки решений таких задач

1.1 Задачи на преобразования лямбда-термов

Бестиповое ^-исчисление формализует представление вычисления выражения как подстановку значений аргумента вместо параметров в определение функции [62, 72]. ^-термы разбиваются на 4 класса:

1. Переменные;

2. Константы;

3. Аппликации или комбинации - задают применение функции к ее аргументам);

4. Абстракции - задают определения функций на основе параметризованных выражений, представляющих их тела.

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

Вместе с бета-преобразованием ^-исчисление является полным по Тьюрингу, то есть позволяет задать любую вычислимую функцию. Задача проверки эквивалентности ^-термов в общем случае является неразрешимой [62, 72].

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

Исследуемые в работе символьные выражения, задаются диаграммой Вирта [138] (Рис. 1). Грамматика таких символьных выражений приведена в приложении 1.

Рис. 1. Диаграмма Вирта и метамодель символьных выражений

Примеры символьных выражений, рассматриваемых в работе:

1. 1^=1(—1)к-1 * С (к, 0 * /п — рассматривается; здесь С - число

сочетаний: С(т,п) = --^—

(т-п)\п\

2. 0.(3) - бесконечная периодическая дробь - не рассматривается. Рассматривается в записи 1/3

В числе рассматриваемых в работе выделяются символьные выражения с C-узкой областью определения - выражения, с областью определения, вероятность сгенерировать точку в которой из равномерного распределения в шаре с центром в начале координат и радиусом, равным наибольшей константе в выражении, меньше 1%. При сравнении таких выражений методом вычислительных экспериментов существенно усугубляется проблема подбора репрезентативных точек (подробнее в пункте «методы, основанные на вычислительных экспериментах»).

Пример символьного выражения с С-узкой областью определения: — х) * (х — 999). Область определения [999;1000], максимальная константа 1000, вероятность, что точка, сгенерированная из равномерного распределения на отрезке [-1000;1000] попадет в [999;1000] равна 1/2000.

Логическое утверждение (logical proposition) [71] - утверждение над символьными выражениями, которое может быть истинно либо ложно. В работе рассматриваются утверждения, которые могут задавать равенство символьных выражений, отношение порядка над символьными выражениями, а также логическую конъюнкцию и дизъюнкцию других рассматриваемых утверждений.

Рис. 2. Метамодель логических утверждений над символьными выражениями

Примеры логических утверждений, рассматриваемых в работе: 1. sin(x) < cos(x) + 1 гх + у = 4

2.

х * у = 4 X * у = 6

1.2 Задачи на оперирование формулами

Значительную часть учебных практических задач в области технических наук составляют задачи на закрепление навыков оперирования формулами.

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

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

Точно верные в контексте задачи логические утверждения называются фактами. Фактами являются:

1. Исходно данные логические утверждения, которые обозначены в условии задачи как истинные (в контексте этой задачи).

2. Логические утверждения, уже доказанные в ходе решения задачи.

Задача на оперирование формулами подразумевает наличие множества символьных выражений и/или логических утверждений E, которые могут встречаться в рассматриваемой предметной области.

Множество правил преобразования - множество отображений множества E в себя, элементы которого соответствуют преобразованиям, которые учащиеся могут применять при решении задачи. Примеры правил преобразования:

1. sin(2 * х) ^ 2 * sin(x) * cos (х)

2. a2 -b2 ^ (a-b)*(a + Ь)

3. а + с = b + c ^ a = b

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

Примеры применения правила преобразования: 1. В результате применения правила а2 — b2 ^ (а-Ь)*(а + Ь) к выражению х + ((а3)2 — (5 — у)2) получим выражение х + ((а3) — (5 — у))((а3) + (5 — у)).

4. В результате применения правила а + с = b + c ^ a = b к логическому утверждению sin(x) + а = cos(x) + а получим логическое утверждение sin(x) = cos(x).

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

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

Задачи на развитие навыков оперирования формулами можно разделить на группы, описанные в таблице:_

Задачи «на Задачи «на Задачи «на

память» доказательство» сведение»

Требование к Перечислить Обосновать Преобразовать

учащимся изученные исходно данное исходно данное

правила утверждение, выражение или

преобразований пользуясь логическое

изученными утверждение так,

правилами чтобы оно

преобразования удовлетворяло

исходно заданным

требованиям,

пользуясь

изученными

правилами

преобразования

Примеры 1. Напишите 1. Докажите, что 1. Выведите

формулу синуса sin(2x) = формулу для

двойного угла 2 sin(x) cos (х). sin(2x) так чтобы в

(При известном числе аргументов

2. Перечислите правиле тригонометрических

формулы, преобразования функций

описывающие sin(x + у) = использовался

закон де sin(x) cos (у) + только моном «X»

Моргана sin(y) cos (х)) (При известном

правиле

2. Докажите, что преобразования

х V (x Л у) = х sin(x + у) =

sin(x) cos (у) +

sin(y) cos (х))

2. Преобразуйте

х 0 у к 3-КНФ

3. Решите уравнение

С(х+ 1, х) = 3

4. Решите систему:

(х + у = 4

{ "х * у = 6

( х * у = 9

Тренируемые Знание формул Знание формул Знание формул

знания и предметной предметной предметной

навыки области области, умение области, умение

строить цепочку строить цепочку

убедительных убедительных

рассуждений, рассуждений, когда

когда известны и известно только

начало, и конец начало (по

этой цепочки сравнению с

задачами на

доказательство не

так понятно, к чему

преобразовывать)

При проверке Проверить Проверить Проверить

преподавателю правильность правильность правильность

требуется написанных цепочки цепочки

формул и их преобразований и преобразований,

соответствие соответствие совпадение

вопросу начального и начального

конечного элемента цепочки с

элементов исходно данным

цепочки символьным

требуемому выражением или

утверждению логическим

предложением, а

также

удовлетворение

конечного элемента

цепочки требуемым

критериям

Табл. 1. Классификация задач на развитие навыков оперирования формулами

В случае задач «на память» ответ учащегося может быть представлен в виде перечня логических утверждений. Автоматическая проверка подобных задач может быть организована следующим образом: 1. Преподаватель задает требуемый перечень логических утверждений.

2. Утверждения, приведенные обучаемым, проверяются на:

2.1. Правильность;

2.2. Соответствие утверждениям, приведенным преподавателем.

3. Проверяется, что все утверждения, заданные преподавателем, были покрыты утверждениями, приведенными обучаемым.

Нетривиальными шагами в данной схеме является проверка правильности логических утверждений и проверка соответствия одного логического утверждения другому логическому утверждению.

В случае задач «на доказательство» и «на сведение» ответ учащегося может быть представлен в виде цепочки преобразований над символьными выражениями и логическими утверждениями. В работе рассматриваются цепочки преобразования, задаваемые диаграммой Вирта (Рис. 3). Грамматика рассматриваемых цепочек преобразования приведена в приложении 2.

Цепочка преобразований

Знак следования

Перенос строки

Знак Правило Знак

<— <—

следования следования

Цепочка преобразований

+последовательность термов : Термы +вручную выведенные правила : Правила

Последовательность термов состоит из шагов-преобразований, опционально дополненных обосновывающими зти преобразования правилами, либо ссылками на них

Рис. 3. Диаграмма Вирта и метамодель цепочек преобразования

Примеры рассматриваемых в работе цепочек преобразований:

= 2*з1п(х)(со5(2*х) + 0.5) _ 2*з1п(х)со5(2*х) + 51п(х) _ (э¡п(3*х)-э¡п(х)) + э¡п(а) _ з!п(Э*х)

Рис. 4. Пример цепочки преобразований, в виде которой может быть записано решение задачи «доказать тригонометрическое тождество»

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

решения задачи

3 *х+2*у =4 + 71

3/х2 + (4 +2 /)у2 + (2+ 7/)ху + (7-ЗУ)х+(-1-12»)у-Э+6; =0 3*х+2*у =4 + 71

3/хг + (2 +/)ху —2х -3/х +е/ху +2(2 +/)уг-4у - 6/у +Эх -3/(2 +/)у +6/ -3 = 0= > (х +2у -3/)(3/х + (2 +/)у -2 —ЗУ) =0 З'х+г'у =4 + 71

[х +2у-31 =0 = >х+2у = 3/ =>

3/X + (2 +/)у -2 -3; = 0 = > 3/Х + (2 +/)у = 2 +3/

{х+2у =34 = > х =31-2у Г х =31-2у 3*Х+2*у =4 + 7/ |з*(31-

2у) +2у = 4 + 71

.1

3/х + (2+/)у =2+3/ = > -Зх + (-1+2/)у = -3+2/ 3*х +2*у = 4 + 7/

= >

Гх=3/ 1 Э/ — 6)

= 3/ - 2у

6у+2*у =4 + 7/

-Зх = —3 +2/ — ( -1 +2/)у = >Х = 1--/ + (-^ + -/)у

3 3 3

3*Х+2"у =4 + 7/

= >

(х=3/-2(-1 + 0.5/)= >Х =3/ +2 —7 = >х =2+2/ [у= -1 + 0-5/

, 2. # 12л

X = 1-—! + (-— + -!)У 3 3 3

. 1з-2/-у+2/у+2у =4 + 7у = >(1+2/)у =1+9/= >у =3.8 + 1.4/

= >

(х = 3/ - 2у

-4у=4-2/= >у = -1 + 0.5/

х=1--/ + (-- + -/)у = >

3 3 3

3*(1— —/+(— — + —/)у)+2*у = 4+7/ 3 3 3

(х =2 + 2/ (у = -1 + 0.5/

* = 1— —/ + (— — + —/)*(3.8+1.4$ = >х= -1.2 + 1.4/ 3 3 3

у =3.8+1.4/

Рис. 6. Пример цепочки преобразований, в виде которой может быть записано решение

задачи «решить систему уравнений». Примечание: в случае переноса строки знак следования между логическими утверждениями может быть пропущен.

= >

[ х =2+2/ \у = -1 + 0.5/ |х = -1.2+1.4/ 1 у =3.0+1.4/

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

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

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

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

Список литературы диссертационного исследования кандидат наук Кацман Виктор Игоревич, 2022 год

ЛИТЕРАТУРА

1. Айвазян С.А. и др. Прикладная статистика: основы моделирования и первичная обработка данных / М.: Финансы и статистика. - 1983.

2. Андреева, Е.А. Вариационное исчисление и методы оптимизации: учеб. пособие / Е.А. Андреева, В.М. Цирулева. Тверь: ТвГУ, 2001. 576 с.

3. Антамошкин А.Н. Оптимизация функционалов с булевыми переменными / Томск: ТГУ. 1986. -129с.

4. Антипов, М. А., Бондарко, М. В., Вавилов, Н. А., Генералов, А. И., Демченко, О. В., Дыбкова, Е. В., Жуков, И. Б., Зильберборд, И. М., Карпов, Д. В., Лузгарёв, А. Ю., Пименов, К. И., Семёнов, А. А., & Шмидт, Р. А. Задачи по алгебре. Комплексные числа и многочлены / 2011 Издательство Санкт-Петербургского университета.

5. Ахо, А. Теория синтаксического анализа, перевода и компиляции (Тома 1-2. Синтаксический анализ) / А. Ахо, Дж. Ульман. — М. : Мир, 1978.

6. А. В. Ахо, Д. Э. Хопкрофт, Д. Д. Ульман, Структуры данных и алгоритмы / М., СПб., Киев: «Вильямс», 2001.

7. Башмаков М.И., Поздняков С.Н., Резник Н.А. Информационная среда обучения / Монография. СПб: СВЕТ, 1997.

8. Бахвалов Н.С Численные методы / -М: Наука, 1973 г.

9. Береснев В.А., Гимади Э.К., Дементьев В.Т / Экстремальные задачи стандартизации. Новосибирск, Наука, 1978.

10.Брудно А. Л. Метод Лобачевского / Квант. № 4 (1989), С. 51—53.

11.Васильев В.Ф. Численные методы решения экстремальных задач / М., Наука, 1981.

12.Выготский Л.С. Мышление и речь / Изд. 5, испр. - М.: Лабиринт, 1999. -352 с.

13.Гилл Ф., Мюррей У., Райт М. Практическая оптимизация / М.: Мир, 1985.

14.Гиндикин С. Г. Алгебра логики в задачах / М. Наука 1972

15. Гинзбург С. Математическая теория контекстно-свободных языков / М. Мир. 1970.

16.Гэри М., Джонсон Д., Вычислительные Машины и Труднорешаемые Задачи / М., Мир, 1982.

17. Дамбраускас А.П. Симплекс поиск / М.: Энергия. 1979

18.Дасгупта С. и др. Алгоритмы / С. Дасгупта, Х. Пападимитриу, У. Вазирани; Пер. с англ. под ред. А. Шеня. — М.: МЦНМО, 2014 ISBN 9785-4439-0236-4

19.Дейкстра Э. Дисциплина программирования = A discipline of programming / 1-е изд. - М.: Мир, 1978. - С. 275.

20.Демидович Б.П. Сборник задач и упражнений по математическому анализу / Учебное пособие. 13-е изд, 1997, Изд-вво Моск. ун-та, ЧеРо, ISBN 5-211-03645-X

21. Демьянов В.Ф., Васильев Л.В. Недифференцируемая оптимизация. М.: Наука, 1981.-384с.

22. Демьянков В.З., Панкрац Ю.Г., Лузина Л. Г. Универсальная грамматика. Краткий словарь когнитивных терминов / Под общ. ред. Е.С. Кубряковой. — М.: МГУ. 1997.

23. Денис Дж. Шнабель Р. Численные методы безусловной оптимизации и решения нелинейных уравнений. М.: Мир,- 1988.

24.Егорушкин О. П., Колбасина И. В., Сафонов К. В. О применении многомерного комплексного анализа в теории формальных языков и грамматик / Прикладная дискретная математика. — 2017. Т. 36. Л" 2. С. 76-89.

25.Карманов В.Г. Математическое программирование / М., Наука, 1975.

26.Карпов Ю. Г. Теория и технология программирования. Основы построения трансляторов. — СПб.: БХВ-Петербург. 2005.

27.Кацман В. И., Новиков Ф. И., 2020. Автоматическая проверка цепочек преобразований над символьными фактами на основе метода перебора логических правил. XXI век: итоги прошлого и проблемы настоящего, технические науки, 2020 №3(51) Т.9, 23-28, 10.46548/21vek-2020-0952-0003.

28.Кацман В. И., Новиков Ф. И., 2020. Игрофикация процесса решения типовых учебных задач на основе выбора правил преобразования / Современная наука, актуальные проблемы теории и практики, естественные и технические науки №9 2020, 63-69, 10.37882/22232966.2020.09.18.

29.Кацман В. И., 2020. Автоматическая проверка цепочек преобразований символьных неравенств на основе перебора логических правил / Приборы и системы. Управление, контроль, диагностика №11 2020, 19 -24, 10.25791/pribor.11.2020.1221.

30.Кацман В. И., Новиков Ф. И. 2018. Автоматизация проверки решения задач на основе перебора логических правил / Информатизация непрерывного образования (Informatization of continuing education), Москва, Материалы. международной научной конференции, 33-36.

31.Кибрик А. Е. Проблема синтаксических отношений в универсальной грамматике. Вып. XI. М.: Прогресс. 1982. С. 5-36.

32.Корбут А.А., Финкельштейн Ю.Ю. Дискретное программирование. и., Наука, 1969.

33.Кормен, Т., Лейзерсон, Ч., Ривест, Р. Алгоритмы: построение и анализ = Introduction to Algorithms / Пер. с англ. под ред. А. Шеня. — М.: МЦНМО, 2000. — 960 с. — ISBN 5-900916-37-5.

34.Манцеров Д.И., Перченок О.В., Поздняков С.Н. и др. Генерация математических задач и верификация решений в автоматизированных системах поддержки обучения / СПб - Изд-во СПбГЭТУ ЛЭТИ.-2012.-154 С.

35.Моисеев H.H. Элементы теории оптимальных систем. М., Наука, 1975.

36.Нестерова С.И., Скоков В.А. Численный анализ программ негладкой безусловной оптимизации / Экономика и математические методы. -1994.

37.Нестеров Ю.Е. Методы выпуклой минимизации / М.: Изд. МЦНМО, 2010.

38.Нильсон Н., Принципы искусственного интеллекта / М., Радио и связь, 1985.

39.Новиков Ф. А., Кацман В. И. 2020. Автоматическая проверка решений учебных задач на основе комбинации методов перебора логических правил и тестирования / Цифровые технологии в инженерном образовании: новые тренды и опыт внедрения (IT-Technologies for engineering education: new trends and implementation experience), Москва: Издательство МГТУ им. Н. Э. Баумана, 266-273.

40.Новиков, Ф. А. Визуальное конструирование программ / Информационно-управляющие системы. 2005. №6. 9-22.

41.Новиков, Ф. А. Дискретная математика / СПб: Питер, 2017. — 432.

42.Пападимитру X., Стайглиц К. Комбинаторная оптимизация. Алгоритмы и сложность. М.: Мир. - 1985.

43.Пентус А.Е., Пентус М.Р. Математическая теория формальных языков / М.: БИНОМ. Лаборатория знаний. - 2006.

44.Перельман И.И. Текущий регрессионный анализ и его применение в некоторых задачах автоматического управления / Изв. АН СССР, Энергетика и автоматика. -1960. -Т. XXIII, №2. -С.

45.Поздняков С.Н., Перченок О.В., Посов И.А. Автоматизация проверки решения геометрических задач по описанию их условий на предметно-ориентированном языке / Компьютерные инструменты в образовании. -СПб. - 2012. - № 1. - С. 37-44.

46.Сафонов К. В., Егорушкнн О. И. Системы полиномиальных уравнений, порождающих контекстно-свободные языки / Материалы Международной конференции «Решетнёвские чтения». Т. 2. — 2009. Красноярск. С. 535.

47.Сеа Ж. Оптимизация. Теория и алгоритмы М., Мир, 1973.

48.Серебряков В. А. [и др.]. Теория и реализация языков программирования / М. : МЗ Пресс, 2006.

49.Станкевич А.С. Общий подход к подведению итогов соревнований по программированию при использовании различных систем оценки / Компьютерные инструменты в образовании. - СПб. - 2011. - №2.

50.Стоцкий Э. Д. Управление выводом в формальных грамматиках / Проблемы передачи информации. — 1971. Т. 7. Вып. 3. С. 87—102.

51.Фаулер М. Предметно-ориентированные языки программирования / М. -СПб - Киев: Вильяме

52.Херц М. М. Энтропия языков, порождаемая автоматной или контекстно-свободной грамматиками с однозначным выводом / Научно-техническая информация. Серия 2. Вып. 4. — 1969.

53.Хомский Н. Три модели описания языка: Пер. с англ. / Кибернетический сборник. Вып. 2. — 1961. С. 237—266.

54.Хомский Н. О некоторых формальных свойствах грамматик / Кибернетический сборник. Нов. серия. Вып. 5. 1962. С. 279—311.

55.Хомский Н. Заметка о грамматиках непосредственно составляющих / Кибернетический сборник. Нов. серия. Вып. 5. — М.: Мир. 1962. С. 312316.

56.Хомский Н. Синтаксические структуры / Новое в лингвистике. Вып. 2. С. 412-527.

57.Хомский Н., Шютценберже М.Н. Алгебраическая теория контекстно-свободных языков / Кибернетический сборник. Нов. серия. Вып. 3. — 1966. С. 195 242.

58.Ababneh, O. Y. New Newton's Method with Third-order Convergence for Solving Nonlinear Equations / O. Y. Ababneh / International Journal of Mathematical, Computational, Physical, Electrical and Computer Engineering. — 2012. — Vol. 6, No. 1. — pp. 118—120.

59.Aitken, A. On Bernoulli's numerical solution of algebraic equations / Proceedings of the Royal Society of Edinburgh. — 1926. — Vol. 46.

60.Alfred V. Aho, John E. Hopcroft, Jeffrey D. Ullman. The Design and Analysis of Computer Algorithms, 1974.

61.Alfred V. Aho, Monica S. Lam, Ravi Sethi, Jeffrey D. Ullman. Compilers: Principles, Techniques, & Tools / Second Edition, 2007.

62.Anthony J. Field, Peter G. Harrison. Functional Programming / International computer science series, Addison-Wesley, 1988.

63.Amat S., Busquier S. Advances in Iterative Methods for Nonlinear Equations / Springer International Publishing, 2016.

64.Auvinen T. Harmful Study Habits in Online Learning Environments with Automatic Assessment / Proceedings of the 2015 International Conference on Learning and Teaching in Computing and Engineering. - 2015 - C. 50-57.

65.Back R.J., A calculus of refinements for program derivations / Acta Informatica, 25:593-624, 1988.

66.Back R.J., Sjoberg M., and Wright J., Field tests of the structured derivations method / Tech. Rpt. 491, Turku Centre for Computer Science, 2002.

67.Back R.J., Mannila L., Peltomaki M., and Sibelius P., Structured derivations: A logic based approach to teaching mathematics / In FORMED 2008: Formal Methods in Computer Science Education, Budapest, 2008.

68.Back R.J., Mannila L., and Wallin S., Student justifications in high school mathematics / In CERME 6, January 2009.

69.Back R.J., Mannila L., and Wallin S., " "It Takes Me Longer, but I Understand Better" - Student Feedback on Structured Derivations. In International Journal of Mathematical Edu- cation in Science and Technology, volume 41, pages 575-593, 2010.

70.Back R.J., Structured Derivations: a Unified Proof Style for Teaching Mathematics. Formal Aspects of Computing, 22(5):629-661, 2010.

71.Back R.J., Teaching Mathematics in the Digital Ave with Structured Derivations / Four Ferries Publishing, Abo Akademi University, 2016.

72.Barendregt, HENK P.. "Functional Programming and Lambda Calculus." Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (1990).

73.Brent R.P. Algorithms for minimization without derivatives / New Jersey. -Prentice -Hall Inc., Englewood Cliffs. 1973.

74.Coursera. [Электронный ресурс] - Режим доступа: https://ru.coursera.org/. Последний доступ 05.12.2021.

75. Игровые пазлы. [Электронный ресурс] - Режим доступа: www.dm.compsciclub.ru/app/list. Последний доступ 05.12.2021.

76.Dijkstra E. and Scholten C., Predicate Calculus and Program Semantics. Springer-Verlag, 1990.

77.Dijkstra E. The notational conventions I adopted, and why. Formal Aspects of Computing, 14:99 - 107, 2002.

78.Dorfler, W. Computer use and views of the mind / 1993 in Keitel.C and Rutheven.K, (eds), Learning from Computers: Mathematics Education and Technology, NATO ASI Series. Series F and Systems Sciences, Vol 121. London: Springer-Verlag.

79.Dreyfus, T. (Ed.). Imagery and reasoning in mathematics and mathematics education / 1994 Sante-Foy, Quebéc, Canada: Les presses de l'université Laval.

80.Dubinsky, Е. (1991). Reflective Abstraction in Advanced Mathematical Thinking. In D. Tall (Ed.) Advanced Mathematical Thinking, Kluwer: Dordrecht.

81.EDX. [Электронный ресурс] - Режим доступа: https://www.edx.org/. Последний доступ 05.12.2021.

82.Euclidea. [Электронный ресурс] - Режим доступа: https://www.euclidea.xyz. Последний доступ 05.12.2021.

83.FineReader. [Электронный ресурс] - Режим доступа: https://finereaderonline.com. Последний доступ 05.12.2021.

84.Fedorchenko, L. Equivalent Transformations and Regularization in Context-Free Grammars / L. Fedorchenko, S. Baranov // Cybern. Inf. Technol. — 2015. — Vol. 14, no. 4. — Pp. 29-44.

85.GeoGebra. [Электронный ресурс] - Режим доступа: https://www.geogebra.org. Последний доступ 05.12.2021.

86.Hargreaves K., Abrahams P. Tex for the Impatient / Addison-Wesley, 1990, ISBN 978-0201513752.

87.Heller A. Stohastic transformations and automata / Mathemetical System Theory. - 1967. № 3. P. 68-73.

88.Hibbard N., Gray J. and Harrison M. Scan limited automata and context limited grammars / Information and Control. — 1969. V. 11. № 1. P. 5-14.

89.MapleSoft. [Электронный ресурс] - Режим доступа: https://www.maplesoft.com. Последний доступ 05.12.2021.

90.Math Helper Demo. [Электронный ресурс] - Режим доступа: https://www.mathhelper.online/. Последний доступ 05.12.2021.

91.Math Helper TWF. [Электронный ресурс] - Режим доступа: https://www.mathhelper.space/twf/prototype/demo.html. Последний доступ 05.04.2020.

92.MathML. [Электронный ресурс] - Режим доступа: https://www.w3.org/TR/MathML3/. Последний доступ 05.12.2021.

93.MathQuil. [Электронный ресурс] - Режим доступа: https://www. http://www.mathquill.com. Последний доступ 05.12.2021.

94.Matlab. [Электронный ресурс] - Режим доступа: https://www.mathworks.com/products/matlab.html. Последний доступ 05.04.2020.

95.Mathai A. An Introduction to Geometrical Probability. CRC Press, 1999, ISBN 9789056996819.

96.Mannila L. and Wallin S., Promoting students justification skills using structured derivations. In ICMI 19 studies, 2009.

97.Mathematica. [Электронный ресурс] - Режим доступа: https://www.wolfram.com/mathematica/. Последний доступ 05.04.2020.

98.Mitchell T. Machine Learning / McGraw Hill, 1997.

99.Moodle. [Электронный ресурс] - Режим доступа: https://moodle.org/. Последний доступ 05.04.2020.

100. Morrill G. Categorial grammar. Logical Syntax, Semantics, and Processing / Oxford: Oxford Univ. Press. 2011. 236 p.

101. Nesterov, Yu. Introductory Lectures on Convex Optimization / A Basic Course. Springer. 2004, ISBN 1-4020-7553-7.

102. Nesterov Yu. Barrier subgradient method / Mathematical Programming - 2011 - V.127, N1. - P.31-56.

103. Nesterov Yu. Dual extrapolation and its application for solving variational inequalities and related problems / Mathematical Programming -2007 - V.109, N2-3. - P.319-344.

104. Nesterov Yu. Gradient methods for minimizing composite ^yH^H^s / Mathematical Programming - 2013 - V.140, N1. - P.125-161.

105. Nesterov Yu. Primal-dual subgradient methods for convex problems / Mathematical Programming - 2009 - V.120, N1. - P.261-283.

106. Nesterov Yu., Scrimali L. Solving strongly monotone variational and quasi- variational inequalities / Discrete and Continuous Dynamical Systems - 2011 - V.31, N4. - P.1383-1296.

107. Novikov, F., Katsman, V., 2018. Gamification of Problem Solving Process Based on Logical Rules / In Informatics in Schools. Fundamentals of Computer Science and Software Engineering, Pozdniakov, S. N. & Dagiené, V. (eds). Scopus, Springer International Publishing, 369-380.

108. Novikov, F., Katsman, V., Mosin, V., 2020. Automated Verification of Expression Transformation Chains Based on Computational Experiments / IOP Conference Series: Materials Science and Engineering. Scopus, 012132.

109. Ochsner A. and Makvandi R., Finite Elements for Truss and Frame Structures / An Introduction Based on the Computer Algebra System Maxima. Berlin: Springer-Verlag. 2019, DOI: 10.1007/978-3-319-94941-3

110. Pea, R. (1987). Cognitive technologies for mathematics education / In Schoenfeld, A. H. (Ed.) Cognitive science and mathematics education (pp. 89122). Hillsdale, NJ: Erlbaum.

111. Peltomaki M. and Back R.J., An empirical evaluation of structured derivations in high school mathematics. In ICMI-19 studies, Taipei, Taiwan, 2009.

112. Pentus M. Lambek calculus is NP-complete / Theor. Comput. Sci. — 2006. V. 357. P. 186-201.

113. P.J.M. van Laarthoven, E.H.L. Aarts: Simulated Annealing: Theory and Applications / in Mathematics and its application, Springer Science Business Media Dordrecht, 1987.

114. Rall, L. B., Automatic Differentiation: Techniques and Applications. Lecture Notes in Computer Science. 120. Springer. 1981. ISBN 978-3-54010861-0

115. Richardson D 1968, Some Unsolvable Problems Involving Elementary Functions of a Real Variable / Journal of Symbolic Logic 33 (4) 514-520 10.2307/2271358.

116. Rice H 1953 Classes of Recursively Enumerable Sets and Their Decision Problems / Transactions of the American Mathematical Society 74 (2) 358 10.2307/1990888.

117. Rogers H. The Theory of Recursive Functions and Effective Computability / MIT Press, 1987, ISBN: 0-262-68052-1; ISBN: 0-07-0535221.

118. Rosenberg A. L. A machine realization of the linear context-free languages / Information and Control. — 1977. V. 10. P. 175—188.

119. Rosenkrants D. Matrix equations and normal forms for context-free grammars // J. Assoc. Computing Machinery. V. 14. — 1967. P. 501-507.

120. Saito K.R. and Nakano R. Second-order learning algorithm with squared penalty term. / In Advances in Neural Information Processing Systems 9. -Denver, CO. -1997

121. Stepic Math Lesson. [Электронный ресурс] - Режим доступа: https://stepik.org/lesson/9176/step/1?unit=1721.

122. SymPy. [Электронный ресурс] - Режим доступа: https://www.sympygamma.com. Последний доступ 05.12.2021.

123. R. Tibshirani, J. Friedman Introduction to Statistical Learning / ISBN-13: 978-1461471370.

124. T. Hastie, R. Tibshirani, J. Friedman The elements of Statistical Learning Data Mining, Inference, and Prediction / Springer, New York, NY 10.1007/978-0-387-84858-7.

125. Thurston, W. On proof and progress in mathematics / 1995 For the Learning of Mathematics 15(1), 20-36.

126. Tirronen M. and Tirronen V. A framework for evaluating student interaction with automatically assessed exercises / Koli Calling Proceedings of the 16th Koli Calling International Conference on Computing Education Research - 2016. - С. 180-181.

127. Valiant L. G. General context-free recognition in less than cubic time / J. Comp. Syst. Sci. - 1975. V. 10. P. 308-315.

128. Velten K., Mathematical Modeling and Simulation: Introduction for Scientists and Engineers, 2019, ISBN 3527407588

129. Verzhbitskii, V. M. One specification of Mann—Ishikawa iterations / V. M. Verzhbitskii, I. F. Yumanova // NNA'12: Fifth Conference on Numerical Analysis and Applications. Abstracts (June 15—20, 2012, Lozenets). — 2012.

130. WeBWorK. [Электронный ресурс] - Режим доступа: https://webwork.elearning.ubc.ca/webwork2/. Последний доступ 05.04.2020.

131. Weisstein, E., Power Tower [Электронный ресурс] - Режим доступа: https://mathworld.wolfram.com/PowerTower.html. Последний доступ 05.04.2020.

132. Wiris. [Электронный ресурс] - Режим доступа: https://www.wiris.com. Последний доступ 05.12.2021.

133. WolframAlpha. [Электронный ресурс] - Режим доступа: https://wolframalpha.com. Последний доступ 05.12.2021.

134. Wolfram S., An Elementary Introduction to the Wolfram Language / Wolfram Media, 2015.

135. Wolfram S., The Background and Vision of Mathematica / WolframResearch, 2011.

136. Wolfram S., The Foundation of Mathematics and Mathematica / WolframResearch, 1999.

137. Willman S., Linden R., Kaila E., Rajala T. and Laakso M. On study habits on an introductory course on programming / Computer Science Education-2015. - С. 276-291.

138. Wirth N., The programming language Pascal / Berichte der Fachgruppe Computerwissenschaften, 1973-03, doi.org/10.3929/ethz-a-000814158. P 4749.

139. Younger D. H. Recognition and parsing of context-free languages in time / Information and Control. — 1967. V. 10. P. 598—605.

140. eMathStudio. [Электронный ресурс] - Режим доступа: https://emathstudio.com. Последний доступ 05.12.2021.

ПРИЛОЖЕНИЕ 1. ГРАММАТИКА РАССМАТРИВАЕМЫХ В РАБОТЕ СИМВОЛЬНЫХ

ВЫРАЖЕНИЙ

1. Терминальные символы:

1.1.Имена функций: {'sin', 'cos', 'sh', 'ch', 'th', 'cth', 'tg', 'ctg', 'asin', 'acos', 'atg', 'actg', 'sec', 'csc', 'sech', 'csch', 'exp', 'ln', 'abs', 'log', 'mod', 'compconj', 'P',' B', 'F', 'C', 'U', 'A', 'V', 'S1', 'S2'},

1.2.Буквы: {'a'-'z', 'A'-'Z'},

1.3.Цифры: {'0'-'9'},

1.4.Бинарные операции: {'+', '-', '*', '/', 'A', 'Л', 'V', '0' , '=' , , '\' },

1.5.Левые унарные операции: {'-', '-'},

1.6. Правые бинарные операции: {'!', 'л'},

1.7.Скобки: {'(', ')'},

1.8.Итераторные функции:

1.8.1. Сумма символьных выражений: {'X'},

1.8.2. Произведение символьных выражений: {'П'},

1.9. Разделители: {',', '.'},

1.10. Зарезервированные имена: {'п', 'е'}.

2. Нетерминальные символы:

2.1. СВ - символьное выражение,

2.2. ИФ - имя функции,

2.3. БК - буква,

2.4.Ц - цифра,

2.5. БО - бинарная операция,

2.6. ЛУО - левая унарная операция,

2.7. ПУО - правая унарная операция,

2.8. ИТФ - имя итераторной функции,

2.9. ЗИ - зарезервированные имена,

2.10. П - переменная,

2.11. ИмП - имя переменной,

2.12. Чис - число,

2.13. МинЗС - минимальное значение переменной-счетчика,

2.14. МаксЗС - максимальное значение переменной-счетчика,

2.15. СА - список аргументов,

2.16. ЧЧ - часть числа.

3. Правила:

3.1.ИФ ^ sin | cos | sh | ch | th | cth | tg | ctg | asin | acos | atg | аС^ | sec | csc | БееИ | сбсИ | ехр | 1п | аЬБ | log | сошрсоп) | Р | В | Б | С | и | А | V | | Б2

3.2.БК ^ а^А-7

3.3.Ц ^ 0-9

3.4.БО ^ + | - | * | / | шоё | Л | V | 0

3.5.ЛУО ^ - | -

3.6.ПУО ^ ! | '

3.7.ИТФ ^ X I П 3.8.ЗИ ^ п | е

3.9.ИмП ^ БК | ИмП БК

3.10. П ^ ИмП | ЗИ

3.11. ЧЧ ^ Ц | ЧЧ Ц

3.12. Чис ^ ЧЧ | ЧЧ.ЧЧ

3.13. СА ^ СВ | СА, СВ

3.14. СВ ^ СВ БО СВ | ЛУО СВ | СВ ПУО | ( СВ ) | ИФ ( СА ) | П | Чис | ИТФ ( П , МинЗС , МаксЗС , СВ )

3.15. МинЗС ^ СВ

3.16. МаксЗС ^ СВ

4. Начальные символы: 4.1.СВ

ПРИЛОЖЕНИЕ 2. ГРАММАТИКА РАССМАТРИВАЕМЫХ В РАБОТЕ ЦЕПОЧЕК ПРЕОБРАЗОВАНИЙ

1. Терминальные символы:

1.1.Знаки: {'<', '>', '<', '>', '=', '=>'}

1.2.Перенос строки: {'\п'}

1.3. Символьное выражение

1.4.Скобки: {'{', '[', }', ']'} - "большие" фигурные или квадратные скобки, трактуемые как система или совокупность. Соответственно: Скобка_большая_фигурная_системная, Скобка_большая_квадратная_системная

2. Нетерминальные символы:

2.1. Знак - знаки, связывающие выражения 2.2.Знак_следования - знак логического перехода

2.3. Перенос_строки

2.4. Логическое_утверждение

2.5. Расширенное_утверждение

2.6. Перечень_утверждений

2.7. Система_логических_утверждений

2.8. Совокупность_логических_утверждений

2.9. Правило

2.10. Правило_преобразования_выражений

2.11. Цепочка_преобразований_выражений

2.12. Цепочка_преобразования_логических_утверждений

3. Правила:

3.1.Знак ^ < | > | < | > | = 3.2.Знак_следования ^ =>

3.3.Перенос_строки ^ \п

3.4.Логическое_утверждение ^ Выражение Знак Выражение | Система_логических_утверждений | Совокупность_логических_утверждений

3.5.Расширенное_утверждение ^ Логическое_утверждение | Цепочка_преобразований_выражений | Цепочка_преобразования_логических_утверждений

3.6.Перечень_утверждений ^ Расширенное_утверждение | Расширенное_утверждение Перенос_строки Перечень_утверждений

3.7. Система_логических_утверждений ^ Скобка_большая_фигурная_системная Перечень_утверждений

3.8. Совокупность_логических_утверждений ^ Скобка_большая_квадратная_системная Перечень_утверждений

3.9.Правило_преобразования_выражений ^ [ Цепочка_преобразований_выражений ]

3.10. Правило ^ Правило_преобразования_выражений | [ Цепочка_преобразования_логических_утверждений ]

3.11. Цепочка_преобразований_выражений ^ Выражение | Выражение Знак Цепочка_преобразований_выражений | Цепочка_преобразований_выражений Знак Правило_преобразования_выражений Знак Цепочка_преобразований_выражений

3.12. Цепочка_преобразования_логических_утверждений ^ Логическое_утверждение | Логическое_утверждение Знак_следования Цепочка_преобразования_логических_утверждений | Логическое_утверждение Перенос_строки Цепочка_преобразования_логических_утверждений | Цепочка_преобразования_логических_утверждений Знак_следования Правило Знак_следования

Цепочка_преобразования_логических_утверждений

4. Начальные символы:

4.1.Цепочка_преобразования_логических_утверждений Цепочка_преобразования_выражений

ПРИЛОЖЕНИЕ 3. ТАБЛИЦА СИНТАКСИЧЕСКИ УПРЯВЛЯЕМОГО ПЕРЕХОДА 8ТБРТ

Символы грамматики МаШМЬ ЬАТБХ

СВ <тго,№> СВ ^тго1^ {СВ}

СВ * СВ СВ &#хБ7 СВ СВ \еёо1 СВ

СВ &#хВ7 СВ СВ \tmes СВ СВ ^ СВ

СВ / СВ <т£гае> СВ СВ </т&ас> \&ас{СВ}{СВ}

СВ л СВ <тБир> СВ СВ </тБир> {СВ} л {СВ}

X ( СЧ , МинЗС , МаксЗС , СВ) <типёегоуег> <то>&#х2211;</то> СВ СЧ = МинЗС МаксЗС </типёегоуег> \surn { СЧ = МинтЗС }л{Макс ЗС} СВ

П ( СЧ , МинЗС , МаксЗС , СВ) <типёегоуег> <то>&#х220Б ;</то> СВ СЧ = МинЗС МаксЗС </типёегоуег> \prod { СЧ = МинтЗС }л{Макс ЗС} СВ

Л &#х2227 \сар

&атр \wedge \land

V &#х2228 \сир \уее \1ог

0 &#х2295 \\ор1ш

&#х2192 Чо \imp1ies

—1 &#хАС \neg

\ \setminus

&#х2202

аЬ (СВ) 1 СВ | \1eft | СВ \right |

( ( \left (

) ) \right )

[ [ \left [

] ] \right ]

< &lt

> &gt

< &#x2264 \le

> &#x2265 \ge

=> &#x21D2 \Rightarrow

= &gt

ПРИЛОЖЕНИЕ 4. КЛЮЧЕВЫЕ ЭЛЕМЕНТЫ АВТОМАТОВ СИНТАКСИЧЕСКОГО РАЗБОРА ВЫРАЖЕНИЙ В ЯЗЫКЕ 8ТБРТ

вно узив ВВАСКЕТ.Ри^ТЮК

SD - afrywenr loßaaneHne AO-ièpHifû yana NAME Si - tpiyHKHMrt, ftoftafiirgHne ywa &RACXET FUNCTlOM S? • nnpftw**<Afl.

NAVT

53 - ysna OPERATION binary

54 ■ ocröaBiWHWB '/an a OPERATION, unary Wfl Si - AptiaäJiBHHB yina OPERATION, unary rifrit

ФОЛ'ЛИГ

SO • nahм/мии« утиля FUNCTION SI • оункдия Оез аргументов дэоаелен/е /зла FUNCTION

S? ■ пяс«имнняя, доьаапение узле VARIABLE

• ОПраГитаЛ приоритетен (■ опесвиий

80 • определение минимального

приоритета Ы • дооааление такого же узла 52 - добавление узла, если приоритет следующий 53 - рекуроип из узла

Где:

BRACKET_FUNCTЮN - функция, записанная с использованием нотации, подразумевающей запись символьных выражений в одну строку, с использованием специальных обозначений для записи фрагментов математических выкладок, которые считается общепринятым обозначать с помощью разделения на несколько строк, либо TEX

MATH_ML_FUNCTЮN - функция, записанная с использованием нотации, подразумевающие ввод математических выкладок в формате, близком к записям «на бумаге», за счет предлагаемого набора паттернов расположений и связей вводимых символов, соответствующих общепринятому расположению фрагментов выражений и логических утверждений для описываемых ими математических примитивов, а далее транслированной интерфейсом записи в теги MathML.

ПРИЛОЖЕНИЕ 5. КЛЮЧЕВЫЕ ЭЛЕМЕНТЫ СИНТАКСИЧЕСКОГО РАЗБОРА ЦЕПОЧЕК ПРЕОБРАЗОВАНИЯ В ЯЗЫКЕ 8ТБРТ НА ДИАГРАММЕ

ПОТОКОВ ДАННЫХ

ПРИЛОЖЕНИЕ 6. АКТ ВНЕДРЕНИЯ

МИНОЕРНАУКИ РОССИИ

федерглкиое государственное автономное образовательное учрежден** высшего образования ■Санкт-Петербургский политехнический университет Петра Великого» (ФГАОУ ВО .СПбПУ.)

ИНН 7804040077. ОГРН 1027102505279. ОХ ПО 02068574 Палитекиическак ул.. 29. Санкт-Петербург, 195251 тел -7(812)297 2095. «икс: -7(812)552 6080 оПке@зрб5Ти.ш

УТВЕРЖДАЮ

У /ж* об^азоиагелъ

■\о* г тЛ '

"Проректор Деятельности

М. Разинкина 202 г.

АКТ ВНЕДРЕНИЯ результатов диссертационной работы Кацмана Виктора Игоревича «Модели и методы автоматической проверки решений задач»

Результаты диссертационной работы Кацмана Виктора Игоревича внедрены в образовательный процесс в высшей школе прикладной математики и вычислительной физики физико-механического института ФГАОУ ВО «Санкт-Петербургский политехнический университет Петра Великого». А именно, разработанные в ходе исследования программные комплексы с весны 2018 года используются при преподавании дискретной математики для автоматической проверки решений учебных задач, а также для стимулирования студентов к решению этих задач и обеспечения более быстрой обратной связи по результатам проверки.

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

и. о. директора ВИН МВФ

Н. Г. Иванов