Паскевич Андрій Юрійович. Засоби формалізації математичних знань та міркувань: теоретичні та практичні аспекти : дис... канд. фіз.-мат. наук: 01.05.01 / Київський національний ун-т ім. Тараса Шевченка. - К., 2005.
Анотація до роботи:
Паскевич А.Ю. Засоби формалізації математичних знань та міркувань: теоретичні та практичні аспекти.— Рукопис.
Дисертація на здобуття вченого ступеня кандидата фізико-математичних наук за спеціальністю 01.05.01 — теоретичні основи інформатики та кібернетики. — Київський національний університет імені Тараса Шевченка, Київ, 2005.
Дисертацію присвячено вивченню та розробці засобів подання математичного знання та схем математичного міркування. Метою роботи є побудова системи автоматичної обробки формалізованих математичних текстів, зокрема, перевірки їхньої коректності. Мова подання цих текстів наближена до природної мови математичних публікацій; пошук доведення ведеться системою на двох рівнях: верхній рівень виконує великі кроки доведення, застосовуючи традиційні прийоми математичного міркування, а нижній рівень “закриває” породжені підцілі за допомогою комбінаторної процедури пошуку виведення в деякій дедуктивній системі. В дисертації описана формальна мова ForTheL, що імітує синтаксис англійскої мови; сформульовано поняття коректності ForTheL-тексту; розроблено “інструментарій” перевірки коректності: набір евристичних методів верхнього рівня, а також ефективну комбінаторну процедуру на базі цілекерованого табличного числення. Результати роботи втілені в програмному комплексі і апробовані у серії експериментів з нетривіальними математичними текстами.
В дисертації автором запропоновано сукупність засобів формального подання математичних знань та їхньої автоматичної обробки з використанням методів природного математичного викладення та міркування. Ці засоби втілено в програмній системі обробки та верифікації формальних математичних текстів.
При виконанні роботи були одержані такі результати:
Розроблено формальну мову ForTheL для запису математичних текстів, близьку до природної англійської мови. Речення та розділи мови ForTheL можуть бути переведені в формули мови першого порядку. Семантика тексту в цілому визначається поставленим завданням (наприклад, перевірити коректність) і ґрунтується на відношенні логічного передування та процедурі нормалізації тексту, яка зводить доведення, проведені за різними схемами, до єдиного уніфікованого вигляду. Визначено різні рівні коректності ForTheL-тексту.
Сформульовано поняття локальної істинності твердження в заданій позиції всередині формули першого порядку. Розглянуто властивості цього поняття, зокрема, показано, що правило modus ponens може застосовуватись локальним чином. Доведена основна властивість локальної істинності: якщо еквівалентність двох формул є локально істинною в заданій позиції, ці дві формули є взаємозамінюваними в цій позиції. Поняття локальної істинності використовується у визначенні онтологічної коректності ForTheL-тексту, а також для теоретичного обґрунтування коректності методів доведення, що застосовують перетворення всередині формул.
Викладено табличне числення GDT, що використовує поняття допустимої підстановки та стратегію цілекерованості в стилі програми “Алгоритм Очевидності”. Доведено коректність і повноту цього числення відносно класичного табличного диз’юнктного числення Model Elimination.
Запропоновано оригінальне цілекероване табличне числення з правилом лінивої парамодуляції LPCT, доведено його повноту.
Реалізовано програмну систему обробки та верифікації формальних математичних текстів, записаних у мові ForTheL. Ця система включає в себе процедури синтаксичного аналізу ForTheL-тексту, трансляції у внутрішнє нормалізоване подання, перевірки онтологічної та загальної коректності, генерації відомостей про окремі входження термів, розкриття визначень та спрощення складних цілей, а також комбінаторний прувер в класичній логіці першого порядку з рівністю, заснований на описаному у роботі цілекерованому табличному численні GDT.
Проведено серію експериментів з формалізації нетривіальних математичних текстів у мові ForTheL та верифікації в системі САД.
Публікації автора:
За темою дисертації автором опубліковано наступні роботи:
Паскевич А.Ю. Особливості реалізації мови високого рівня для запису математичних текстів // Вісник КНУ, серія: фізико-математичні науки — 1999 — т. 2 — С. 284–288.
Лялецький О.В., Паскевич А.Ю. Про деякі стратегії пошуку логічного виводу, керовані цілями // Вісник КНУ, серія: фізико-математичні науки — 2001 — т. 2 — C. 277–285.
Паскевич А.Ю. Поняття локальної істинності та його застосування у автоматичному доведенні теорем // Вісник КНУ, серія: фізико-математичні науки — 2003 — т. 1 — C. 199-203.
Вершинин К.П., Лялецкий А.В., Паскевич А.Ю. Применение Системы Автоматизации Дедукции для верификации математических текстов // Научно-теоретический журнал “Искусственный интеллект” — 2003 — №3 — C. 57–69.
Vershinin K., Paskevich A. ForTheL — the language of formal theories // Proc. of International Conference “Information Theories and Applications 2003” — Varna (Bulgary) — 2000 — P. 120–126.
Lyaletski A., Verchinine K. Paskevich A. On Verification Tools Implemented in the System for Automated Deduction // Proc. Second CoLogNet Workshop “Implementation Technology for Computational Logic Systems 2003” — Pisa (Italy) — 2003 — P. 3–14.
Lyaletski A., Paskevich A., Verchinine K. Theorem Proving and Proof Verification in the System SAD // Proc. Third International Conference “Mathematical Knowledge Management 2004” — Bialystok (Poland) — 2004 — P. 236–250.
