Кацман Виктор Игоревич Модели и методы автоматической проверки решений задач

Краткое описание

Кацман Виктор Игоревич Модели и методы автоматической проверки решений задач
ОГЛАВЛЕНИЕ ДИССЕРТАЦИИ
кандидат наук Кацман Виктор Игоревич
ВВЕДЕНИЕ

ГЛАВА 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. Логические утверждения - равенства и отношения порядка символьных выражений.

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