Система для розв’язання геометричних задач на основі секвенційного реномінативного числення

Швець М. Система для розв’язання геометричних задач на основі секвенційного реномінативного числення : кваліфікаційна робота … бакалавра : 122 Комп’ютерні науки / Швець Михайло. – Київ, 2023. – 64 с.

У результаті виконання дипломної роботи було розроблено програмний продукт для автоматизації доведення геометричних тверджень.
Проведено аналіз наявних продуктів з даної тематики на ринку і зроблено висновок, що продуктів, які поглиблено спеціалізуються на геометрії, наразі немає.
Проведено аналіз найчастіше вживаних інструментів розробки та обрано оптимальні варіанти, які і були використані при написанні програми.
Розроблено детальну архітектуру програмної системи, а також формально записано алгоритми потрібні для її роботи, внаслідок чого швидкість написання коду збільшилась.
Здійснено програмну реалізацію продукту з урахуванням результатів отриманих раніше.
Завдяки дотриманню принципів SOLID можливе доопрацювання та розширення розробленого продукту, наприклад додавання можливості для розв’язання діофантових рівнянь за допомогою оператора мінімізації. Також, за потреби, є можливість повної зміни предметної області для пошуку доведень, оскільки основна структура, де реалізоване секвенційне числення, не потребуватиме змін в такому разі. Також можливим є створення повноцінного користувацького інтерфейсу для полегшення роботи з програмою для кінцевого користувача.

Ключові слова : автоматизація доведення теорем, геометрія, проєктування, реномінативна логіка, розробка, секвенційне числення, система рівнянь та нерівностей.