Паскевич А. Ю. Засоби формалізації математичних знань та міркувань: теоретичні та практичні аспекти

Дисертацiю присвячено вивченню та розробцi засобiв подання математичного знання та схем математичного мiркування. Метою роботи є побудова системи автоматичної обробки формалiзованих математичних текстiв, зокрема, перевiрки їхньої коректностi. Мова подання цих текстiв наближена до природної мови математичних публiкацiй; пошук доведення ведеться системою на двох рiвнях: верхнiй рiвень виконує великi кроки доведення, застосовуючи традицiйнi прийоми математичного мiркування, а нижнiй рiвень "закриває" породженi пiдцiлi за допомогою комбiнаторної процедури пошуку виведення в деякiй дедуктивнiй системi. В дисертацiї описана формальна мова ForTheL, що iмiтує синтаксис англiйскої мови; сформульовано поняття коректностi ForTheL-тексту; розроблено "iнструментарiй" перевiрки коректностi: набiр евристичних методiв верхнього рiвня, а також ефективну комбiнаторну процедуру на базi цiлекерованого табличного числення. Результати роботи втiленi в програмному комплексi i апробованi у серiї експериментiв з нетривiальнимиматематичними текстами.