Науковий керівник доктор фізико-математичних наук Летичевський Олександр Олександрович

Мета роботи. Автоматичне доведення тверджень, як виведення властивостей із множини аксіом та доведених тверджень, є відомим напрямом штучного інтелекту. Початок досліджень в цій галузі було започатковано В.М,Глушковим у Інституті кібернетики. Починаючи із простих теорій, таких як лінійна арифметика, в сучасній індустрії програмних систем було створено велика кількість машин доведення та машин розв’язувачів. 

В зв’язку із ростом складності алгебраїчних систем виникає проблема ефективності виведення та експоненціального вибуху станів. Машинне навчання є одним із ефективних способів тренування моделей виведення. Створення моделі класифікації відносно структури формул властивостей систем, які треба довести, дозволить спрямувати автоматичне виведення та раціональне використання вже раніше доведених тверджень. Задача може бути розширена до використання алгебраїчного моделювання в рамках заданих транзиційних систем.

Задачі полягають в аналізі властивостей формул в різних теоріях (лінійна арифметика, теорія символьних типів даних та інші) та створення моделі класифікації, яка має бути натренована різними техніками виведення в теорії з використанням найбільш ефективних алгебраїчних перетворень та використання раніш доведених фактів. Розглядаються створення моделей класифікацій як в рамках однієї теорії та комбінацій різних теорій.