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

Тому необхідність в ефективних та зручних системах автоматичного доведення виходить за межи суто наукових застосувань: при розробці, наприклад, систем реального часу, зайнятих у промисловості та транспорті, або захищених протоколів звязку, такі системи відіграють ключову роль. Тому доцільно розглядати задачу перевірки цих тверджень не в сенсі побудови виведення в тій чи іншій формальній дедуктивній системі, а як задачу проведення математичного міркування. Дисертаційне дослідження виконувалося в рамках наукової теми “Логіко-математичні та програмологічні засоби інформаційних технологій” (державний реєстраційний номер 01БФ015-07), яка виконувалась на факультеті кібернетики Київського національного університету імені Тараса Шевченка. В роботі розробляється оригінальна дворівнева архітектура процедури автоматичного доведення, де верхній рівень (“міркувальник”) виконує високорівневі кроки доведення, імітуючи традиційні прийоми математичного міркування, а нижній рівень “закриває” породжені підцілі за допомогою комбінаторної процедури пошуку виведення в деякій формальній дедуктивній системі. розробити “інструментарій” для перевірки коректності: комбінаторні процедури пошуку виведення, а також еврістичні методи доведення, що використовуватимуться на верхньому рівні системи.Лексичним “будівним матеріалом” є синтаксичні примітиви: іменники, які формують поняття (subset of) або терми (closure of); дієслова та прикметники, які формують предикати (belongs to, compact); символьні примітиви, які дозволяють застосовувати коротку символьну нотацію для функцій та предикатів, а отже вживати звичайні формули першого порядку в якості тверджень FORTHEL. По-перше, це поняття “логічного попередника”: FORTHEL-розділ вважається логічним попередником розділу , якщо є максимальним відносно включення розділом, що знаходиться в тексті перед розділом . Припустимо, наприклад, що наш текст складається з визначення , що містить припущення та твердження , та теореми , що містить припущення та твердження , яке, в свою чергу, супроводжується доведенням з трьох речень , , . В попередньому прикладі, формульним образом розділу буде формула вигляду , де є формульним образом припущення (за визначенням, це формульний образ пропозиції в ), є формульним образом твердження (за визначенням, це формульний образ пропозиції в , доведення при цьому не враховується), а є змінними, декларованими в . Для кожного входження деякого предиката, функції або поняття в формульний образ речення в нормалізованому FORTHEL-тексті, ми маємо знайти серед логічних попередників такий розділ типу “визначення” або “сігнатура”, в якому вводиться відповідний синтаксичний примітив, і необхідні твердження про належність аргументів цього входження до обємів поняттів-типів є локально істинними в позиції цього входження в формульному образі - тобто локальний образ твердження випливає з множини (формульних образів) логічних попередників .В дисертації автором запропоновано сукупність засобів формального подання математичних знань та їхньої автоматичної обробки з використанням методів природного математичного викладення та міркування. Ці засоби втілено в програмній системі обробки та верифікації формальних математичних текстів. При виконанні роботи були одержані такі результати: Розроблено формальну мову 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.