Детальная информация

Объектом исследования является процесс автоматизированной проверки формализованных решений задач по планиметрии. Цель работы — разработать программный модуль, выполняющий пошаговый анализ решения, проверку ссылок и обоснований, контроль достижения цели и формирование диагностического отчета. В ходе работы определены требования к формализованному представлению задачи и решения на языке ToKnow Geometry, разработана внутренняя модель задачи и решения, описаны алгоритмы формирования контекста, проверки шагов решения, анализа обоснований, проверки ссылок, контроля достижения цели и формирования диагностических сообщений. В работе использованы методы формализации предметной области, нормализации объектов и утверждений, моделирования контекста и экспериментальной проверки. Результатом работы стал программный модуль, реализованный на языке TypeScript. Модуль выполняет проверку формализованного решения: проверяет, следует ли каждый шаг из исходных данных, ранее полученных результатов и указанного основания, выявляет неподтвержденные переходы, а также фиксирует случаи, когда все шаги решения приняты, но требуемая цель задачи не достигнута. Результатом проверки является отчет с итоговым статусом и диагностическими сообщениями. Экспериментальная проверка показала работоспособность реализованных механизмов и позволила выявить ограничения текущего набора поддерживаемых правил вывода. Разработанный модуль может применяться в проекте ToKnow Geometry и в образовательных системах, использующих язык TKG. Сделан вывод, что разработанный модуль обеспечивает автоматическую проверку решений и может быть расширен за счет добавления новых правил школьной геометрии, о которых система еще не знает.

The object of the study is the process of automated verification of formalized solutions to plane geometry problems. The aim of the work is to develop a software module that performs step-by-step analysis of a solution, checks references and justifications, verifies goal achievement, and generates a diagnostic report. The work defines requirements for the formalized representation of a problem and its solution in the ToKnow Geometry language, develops an internal model of the problem and solution, and describes algorithms for context construction, solution step verification, justification analysis, reference checking, goal achievement verification, and generation of diagnostic messages. The methods used in the work include domain formalization, normalization of objects and statements, context modeling, and experimental evaluation. The result of the work is a software module implemented in TypeScript. The module verifies a formalized solution by checking whether each step follows from the initial data, previously obtained results, and the specified justification. It detects unsupported transitions and also identifies cases in which all solution steps are accepted, but the required goal of the problem is not achieved. The result of verification is a report containing the final status and diagnostic messages. The experimental evaluation demonstrated the operability of the implemented mechanisms and made it possible to identify limitations of the current set of supported inference rules. The developed module can be used in the ToKnow Geometry project and in educational systems that use the TKG language. It is concluded that the developed module provides automated solution verification and can be extended by adding new geometric rules.