Если у вас возникли сложности с курсовой, контрольной, дипломной, рефератом, отчетом по практике, научно-исследовательской и любой другой работой - мы готовы помочь.
Предоплата всего
Подписываем
–17 –
Київський національний університет імені Тараса Шевченка
Паскевич Андрій Юрійович
УДК 004.832.3
Засоби формалізації математичних знань та міркувань: теоретичні та практичні аспекти
01.05.01 —теоретичні основи інформатики та кібернетики
АВТОРЕФЕРАТ
дисертації на здобуття вченого ступеня
кандидата фізико-математичних наук
Київ —
Дисертацією є рукопис.
Робота виконана на кафедрі системного аналізу та теорії прийняття рішень факультету кібернетики Київського національного університету імені Тараса Шевченка.
Науковий керівник:
Кандидат фізико-математичних наук, професор
Донченко Володимир Степанович,
Київський національний університет імені
Тараса Шевченка, факультет кібернетики,
професор кафедри системного аналізу та
теорії прийняття рішень
Офіційні опоненти:
доктор фізико-математичних наук, професор
Провотар Олександр Іванович,
Київський національний університет імені
Тараса Шевченка, факультет кібернетики,
завідувач кафедрою інформаційних систем
Кандидат фізико-математичних наук,
Старший науковий співробітник
Гороховський Семен Самійлович
Національний університет
“Києво-Могилянська академія” МОН України,
доцент
Провідна установа:
Інститут кібернетики НАН України,
відділ обчислювальних рекурсивних машин
Захист дисертації вiдбудеться “15” грудня 2005 року о 14 годині на засiданнi спецiалiзованої вченої ради Д 26.001.09 Київського національного університету імені Тараса Шевченка (03127, м. Київ, пр. Глушкова, 2, корп. 6, ф-т кібернетики, ауд. 40, тел. 521-33-66, факс 529-70-44, e-mail: rada1@unicyb.kiev.ua)
З дисертацiєю можна ознайомитися у Науковій бiблiотецi Київського національного університету імені Тараса Шевченка (01033, м. Київ, вул. Володимирська, 58).
Автореферат розiсланий “14” листопада 2005 р.
Вчений секретар спецiалiзованої вченої ради
кандидат фізико-математичних наук, доцент В.П.Шевченко
ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ
Актуальність теми.
З кожним роком невпинно розширюється сфера застосування комп’ютерних програмних систем. Без використання новітніх інформаційних технологій сьогодні неможливо уявити успішне вирішення економічних і військових, банківських і технічних задач. Це висуває жорсткі вимоги щодо безпечності та надійності сучасного програмного забезпечення, призначеного для критично відповідальних задач, ці якості мають бути строго доведені, а не встановлені емпірично. Тому необхідність в ефективних та зручних системах автоматичного доведення виходить за межи суто наукових застосувань: при розробці, наприклад, систем реального часу, зайнятих у промисловості та транспорті, або захищених протоколів зв’язку, такі системи відіграють ключову роль. Необхідно відмітити, що складність цієї проблеми робить неможливою повну автоматизацію її вирішення. Тому надзвичайно важливою виявляється взаємодія людини з машиною, необхідна для розв’язання задач, що вимагають як обчислювальної потужності для громіздких рутинних побудов, так і інтелекту разом з інтуїцією, для вибору потрібного напрямку розв’язання.
Незалежно від їхнього походження, твердження, що мають бути перевірені, є, фактично, математичними твердженнями, сформульованими в деякій формальній теорії. Тому доцільно розглядати задачу перевірки цих тверджень не в сенсі побудови виведення в тій чи іншій формальній дедуктивній системі, а як задачу проведення математичного міркування. Середою для такого міркування виступатиме математичний текст, подібний до “природних” текстів, що публікуються в журналах та підручниках. Такий підхід дає можливість користувачеві співпрацювати з машиною в зручному та звичному для себе оточенні: запроваджувати ескізи доведень, відслідковувати шлях міркування програми, коригувати його. Важливість задачі вивчення та формалізації традиційних засобів подання математичного знання та схем математичного міркування для успішного широкого застосування інформаційних технологій і визначає актуальність даної дисертаційної роботи.
Зв’язок з науковими програмами, планами, темами.
Дисертаційне дослідження виконувалося в рамках наукової теми “Логіко-математичні та програмологічні засоби інформаційних технологій” (державний реєстраційний номер 01БФ015-07), яка виконувалась на факультеті кібернетики Київського національного університету імені Тараса Шевченка. Робота продовжує цикл досліджень за програмою “Алгоритм Очевидності” (АО), започаткованою В.М. Глушковим на початку 1970-х років в Інституті кібернетики АН УРСР.
Мета і завдання дослідження.
Головною метою роботи є побудова системи комп’ютерних засобів автоматичної перевірки коректності формалізованого математичного тексту. В роботі розробляється оригінальна дворівнева архітектура процедури автоматичного доведення, де верхній рівень (“міркувальник”) виконує високорівневі кроки доведення, імітуючи традиційні прийоми математичного міркування, а нижній рівень “закриває” породжені підцілі за допомогою комбінаторної процедури пошуку виведення в деякій формальній дедуктивній системі.
Відповідно до вказаної мети визначені основні завдання роботи:
запропонувати формальну мову для подання математичних текстів;
сформулювати систему понять, в рамках якої можна визначити коректність тексту, записаного цією мовою;
розробити “інструментарій” для перевірки коректності: комбінаторні процедури пошуку виведення, а також еврістичні методи доведення, що використовуватимуться на верхньому рівні системи.
Запропоновані рішення мають бути теоретично обґрунтовані та апробовані на практиці у серії експериментів.
Методика дослідження полягає у проведенні аналізу природних математичних текстів, вивчення засобів подання та міркування, що використовуються в них, та побудові формальних аналогів цих засобів. Для теоретичного обґрунтування запропонованих рішень використовувався апарат математичної логіки та теорії логічного виводу.
Описана в дисертаційній роботі мова запису математичних текстів ForTheL побудована на принципах, що закладені в мові TL, запропонованій К.П. Вершиніним2.
В основі табличних цілекерованих числень, що вивчаються в роботі, лежить процедура породження вспоміжних цілей (ПВЦ), запропонована Ф.В. Ануфрієвим та розвинута О.В. Лялецьким та А.І. Дегтярьовим3. Поняття допустимої підстановки було введено О.В. Лялецьким з метою оптимізації перебору відносно різних порядків застосування кванторних правил в разі відмовлення від сколемізації.
Для доведення повноти запропонованого у третьому розділі роботи цілекерованого табличного числення для класичної логіки першого порядку з рівністю було використано метод елімінації рівності та метод трансформації виведень.
Наукова новизна одержаних результатів.
На базі мови TL розвинуто формальну мову подання математичних текстів ForTheL, що є близькою за синтаксисом до природної англійської мови і може бути перекладена в мову першого порядку. Сформульовано поняття коректності тексту в мові ForTheL.
Запропоновано оригінальне поняття локальної істинності твердження в деякій позиції всередині формули першого порядку та досліджено його властивості. Зокрема, доведено, що коли еквівалентність двох формул є локально істинною в заданій позиції, ці дві формули є взаємозамінюваними в цій позиції. Поняття локальної істинності дозволяє обґрунтувати коректність різноманітних перетворень складних формул, таких як розкриття визначень або додання допоміжних тверджень всередині формули. Також в роботі запропонована процедура породження “відомостей” про окремі входження термів в досліджуваний ForTheL-текст; ці відомості є літерами, локально істинними в відповідному входженні, зокрема, вони несуть інформацію про тип терму. На базі цього апарату в роботі сформульовано декілька високорівневих схем доведення, які становлять “інструментарій” міркувальника.
Набули розвитку дослідження цілекерованих процедур пошуку виведення, що використовуються в програмі “Алгоритм Очевидності”. Дано нове доведення коректності поняття допустимої підстановки. Викладено цілекероване табличне числення, що оперує несколемізованими формулами. Доведено, що виведення в цьому численні можуть бути перетворені у виведення в класичному табличному диз’юнктному численні Model Elimination. Також доведена можливість зворотнього перетворення. Запропоновано нове табличне цілекероване числення з лінивою парамодуляцією для класичної логіки першого порядку з рівністю, доведено його повноту.
Практичне значення.
Результати дисертаційної роботи дозволили реалізувати систему автоматичного доведення САД (Система Автоматизації Дедукції), призначену для обробки формальних математичних текстів, зокрема, для перевірки їх коректності. Описана у роботі мова ForTheL може бути застосована як мова формалізації в багатьох задачах: верифікації специфікацій програмного та апаратного забезпечення, верифікації протоколів передачі даних, для створення баз математичного знання, для комунікації комп’ютерних математичних сервісів. Введене у роботі поняття локально істинного твердження може бути використано для формалізації природних прийомів математичного міркування. Техніка генерації літерних відомостей про входження термів може застосовуватись для скорочення пошуку доведення. Запропоноване цілекероване табличне числення з лінивою парамодуляцією може бути застосоване як базове числення при побудові універсального пруверу (програми автоматичного доведення) для логіки першого порядку з рівністю.
Особистий внесок здобувача.
Здобувачем особисто була розроблена граматика мови ForTheL, в якій формалізовано фрагмент англійскої мови. Синтаксис ForTheL-речень було розширено (порівняно з TL) багатьма новими оборотами (наприклад, негативний універсальний квантор “no” та дієслово “to have” в твердженнях типу the empty set has no elements), дозволяється символьна нотація, синонімія. Запропоновано оригінальний синтаксис і семантику доведень за різними схемами.
Здобувачеві належать оригінальне формулювання цілекерованого табличного числення в стилі ПВЦ та нове доведення коректності і повноти такого числення шляхом побудови рекурсивної процедури перетворення виведень в цьому численні в виведення в класичному численні Model Elimination; таким чином, встановлено зв’язок між двома підходами для класичної логіки першого порядку. Цілекероване табличне числення з правилом лінивої парамодуляції є оригінальною розробкою здобувача.
В роботі [2] здобувачем проведене порівняння двох запропонованих цілекерованих числень з точки зору побудови мінімальних виводів (розділ “Порівняння числень”). Для обох числень знайдено класи задач пошуку виводу, для яких мінімальне дерево виводу у одному численні має лінійний обсяг, а у іншому численні —експоненційний, по відношенню до обсягу задачі.
В роботі [4] здобувачем виконано програмну реалізацію системи САД, йому належить наведений у статті опис системи, а також процедури верифікації математичного тексту (розділи “Архитектура САД”, “Верификация в САД”).
В тезах доповідей [5] та [6] К.П. Вершиніну та О.В. Лялецькому належать належить постановка задачі та участь в обговоренні результатів.
В тезах доповіді [7] здобувачеві належать опис архітектури системи, мови ForTheL, демонстрація процедури верифікації тексту на прикладі доведення теореми Рамсея (розділи “System for Automated Deduction”, “Linguistic tools of SAD”, “Text verification in SAD”).
Апробація результатів дисертації.
Основні результати докладалися на наукових семінарах в Інституті кібернетики НАН України, на факультеті кібернетики Київського національного університету імені Тараса Шевченка, в лабораторії LACL університету Париж 12 (Франція), в дослідницькій групі OMEGA Саарландського університету (Німеччина), в лабораторії LORIA (Франція), в групі теоретичної інформатики та логіки Віденського технічного університету (Австрія), а також на наступних конференціях та семінарах:
Міжнародний семінар “Rewriting techniques and efficient theorem proving” (Київ, 2000);
Міжнародна конференція “Information Theories and Applications 2000” (Варна, Болгарія, 2000);
Міжнародний семінар “STRATEGIES 2001” (Сієна, Італія, 2001);
Міжнародний семінар “Implementation Technology for Computational Logic Systems” (Піза, Італія, 2003);
Міжнародна конференція “Mathematical Knowledge Management 2004” (Білосток, Польща, 2004).
Публікації.
Основні результати дисертації опубліковано у 7 роботах, з яких 4 —статті у фахових збірниках наукових праць, 3 —тези міжнародних конференцій.
Об’єм та структура роботи.
Робота складається з вступу, трьох розділів, висновків, списку використаних джерел та додатків. Загальний обсяг роботи —сторінка, обсяг основного тексту —сторінок, бібліографія —найменування.
ОСНОВНИЙ ЗМІСТ ДИСЕРТАЦІЙНОЇ РОБОТИ
В першій главі описано формальну мову для запису математичних текстів ForTheL (Formal Theory Language), наближену до природної англійської мови математичних публікацій.
Синтаксис речення в ForTheL імітує правила традиційної англійської граматики. Речення складаються з частин-юнітів: пропозицій, предикатів, понять (які позначають класи об’єктів) та термів (які позначають окремі об’єкти). Лексичним “будівним матеріалом” є синтаксичні примітиви: іменники, які формують поняття (subset of) або терми (closure of); дієслова та прикметники, які формують предикати (belongs to, compact); символьні примітиви, які дозволяють застосовувати коротку символьну нотацію для функцій та предикатів, а отже вживати звичайні формули першого порядку в якості тверджень ForTheL. Синтаксичні примітиви (за винятком прикметника equal to та декількох інших) мають бути введені безпосередньо в ForTheL-тексті. Синтаксичний примітив може бути введений як скорочення для комбінації вже існуючих примітивів, так, наприклад, дієслово belongs to може бути скороченням для is an element of.
Підставляючи терми в аргументні місця синтаксичних примітивів, ми отримуємо прості юніти. Прості юніти можуть групуватися в складні або перетворюватись на юніти іншого типу. Так, наприклад, маючи синтаксичний унарний примітив subset of та змінну S, ми утворюємо юніт поняття subset of S. Додавши прикметник nonempty, ми отримаємо поняття з атрібутом nonempty subset of S. Додавши до цього кванторне слово some, ми перетворимо поняття на терм: some nonempty subset of S. Застосовуючи до терму або сукупності термів предикат, ми будуємо просту пропозицію: some nonempty subset of S is infinite. Прості пропозиції можуть групуватися в пропозиційні комбінації або вставати під квантори, обмежені об’ємом деякого поняття (необмежені квантори не дозволяються мовою ForTheL). Звісно, граматика мови ForTheL відображає лише малу частину природної мови, або навіть її “математичного діалекту”.
Семантика речення ForTheL визначається процедурою переводу юніту пропозиції в деяку формулу першого порядку —формульний образ цієї пропозиції. Наприклад, проста пропозиція all closed subsets of any compact set are compact має наступний формульний образ:
В мові ForTheL є три типа речень: припущення, твердження, селекція. Припущення починаються зі слів assume that або let, за якими йде пропозиція. Наступні речення є типовими припущеннями: “Let S be a nonempty set.”, “Suppose that m is greater than n.”. Твердження формуються з пропозицій безпосередньо: “If p divides n-p then p divides n.”. Нарешті, селекції формуються з низки понять, перед якою стоять слова take або choose: “Take an even prime number X.”. Селекції стверджують непустоту об’ємів перелічених понять. Як припущення, так і селекції можуть декларувати нові змінні.
ForTheL-текст є послідовністю розділів верхнього рівня. Ці розділи —аксіоми, визначення, теореми та леми —відіграють в ForTheL ту ж саму роль, що й в звичайних математичних текстах. Будь-який розділ верхнього рівня складається з послідовності припущень, можливо порожньої, за якою йде твердження. Спеціальним розділом верхнього рівня є розділ “сигнатура”, де вказується область визначеності нового синтаксичного примітива —перелічуються поняття до об’єму яких мають належати його аргументи. В онтологічно коректному тексті (дивись нижче), кожен синтаксичний примітив має вперше з’явитися або в розділі “визначення”, або в розділі “сигнатура”.
Твердження в розділі “теорема” може супроводжуватись доведенням. Доведення в ForTheL —це послідовність припущень, селекцій та тверджень (які можуть мати власні доведення), а також розділів нижнього рівня: випадків та простих блоків. Послідовність розділів типу “випадок” має завершувати доведення за розглядом випадків. Прості блоки використовуються лише для структурізації доведення: для обмеження області дії припущень та декларацій змінних. Мова ForTheL підтримує декілька схем доведень: від суперечного, за розглядом випадків, за загальною індукцією. Речення ForTheL також вважаються розділами нижнього рівня, зокрема, твердження, що супроводжується доведенням, є одним складним розділом.
Ми не визначаємо семантику ForTheL-тексту —вона залежить від завдання, що поставлено системі: наприклад, перевірка коректності або пошук релевантних фактів стосовно заданого твердження. Ми лише вводимо базові властивості та відносини між елементами тексту, в термінах яких маємо описувати ту чи іншу “кінцеву” семантику.
По-перше, це поняття “логічного попередника”: ForTheL-розділ вважається логічним попередником розділу , якщо є максимальним відносно включення розділом, що знаходиться в тексті перед розділом . Припущення або декларація змінної, зроблені в реченні , діють на всі розділи тексту, для яких є логічним попередником.
Припустимо, наприклад, що наш текст складається з визначення , що містить припущення та твердження , та теореми , що містить припущення та твердження , яке, в свою чергу, супроводжується доведенням з трьох речень , , . Логічними попередниками речення в цьому тексті будуть розділи , та .
По-друге, ми вводимо процедуру нормалізації ForTheL-тексту. Нормалізація зводить доведення, проведені за різними схемами, до єдиного уніфікованого вигляду. Так, наприклад, в доведення за індукцією явно додається гіпотеза індукції, а в доведення за розглядом випадків —твердження вичерпності розгляду, самі ж розділи-випадки перетворюються на звичайні ForTheL-твердження, супроводжені доведенням.
Нарешті, кожному розділу (нормалізованого) ForTheL-тексту ми зіставляємо його формульний образ в мові першого порядку. Це дає нам можливість говорити про суто логічні відношення між елементами тексту. В попередньому прикладі, формульним образом розділу буде формула вигляду , де є формульним образом припущення (за визначенням, це формульний образ пропозиції в ), є формульним образом твердження (за визначенням, це формульний образ пропозиції в , доведення при цьому не враховується), а є змінними, декларованими в .
Друга глава присвячена поняттю коректності ForTheL-текста і методам перевірки коректності. На початку глави ми вводимо необхідний для подальшого технічний апарат. По-перше, нам потрібно вміти формулювати і перевіряти твердження про окремі терми всередині складних формул. Запропонований у дисертації підхід ґрунтується на понятті “локального образу”.
Ми використовуємо скінчені послідовності натуральних чисел для позначення позицій підформул та термів всередині формули. Наприклад, в формулі , пропозиційна буква знаходиться в позиції . Локальний образ формули в позиції в формулі (позначається ) —це формула першого порядку, що є формальним еквівалентом твердження “ є локально істинною в позиції в ”. Формула визначається рекурсією по структурі формули . Так, локальним образом в позиції в попередній формулі буде формула .
Адекватність цього поняття підтверджується його наступними властивостями:
—істинна формула є локально істинною в будь-якому оточенні ( тут означає універсальне замикання формули );
—“локальний modus ponens”;
—якщо два твердження є локально еквіва-лентними в деякій позиції формули, вони є взаємнозамінюваними в цій позиції ( означає формулу , де підставлено в позицію );
—аналогічно до попереднього, але тут є позицією терма.
Наведені властивості мають місце також в інтуіціоністській логіці першого порядку, що відрізняє запропонований підхід від попередніх робіт, присвячених локальним перетворенням.
Прикладом застосування цього апарату є розкриття визначень всередині формул. Розглянемо формулу, що визначає унарний предикат: . Нехай маємо формулу , де в позиції знаходиться атом . Якщо ми можемо довести формулу , то за правилом локального modus ponens, матимемо , а отже формула буде еквівалентною формулі .
Ще один технічний прийом, що у стає у нагоді під час перевірки тексту —це накопичення відомостей, пов’язаних з окремими входженнями термів. Ми кажемо, що літера є “відомістю” про деяке входження терма (йдеться про входження в формульний образ речення в нормалізованому ForTheL-тексті), якщо, по-перше, є одним з аргументів , по-друге, є локально істинною в позиції цього входження, і, по-третє, ця локальна істиність може бути встановлена певним “простим чином”. Точне визначення процедури породження відомостей є досить технічним, але, неформально кажучи, вона полягає у скінченій послідовності кроків гіперрезолюції, де головні диз’юнкти беруться з множини логічних попередників поточного речення, а сателіти —з множини вже накопичених відомостей про терм та його підтерми.
Розглянемо формульний образ простого твердження: forall x ((x is a divisor of N) implies ((x + 1) is a natural number)). Припустимо, що серед логічних попередників цього твердження є декларація змінної N як натурального числа, а також визначення поняття divisor of. Розглянемо терм x + 1. Його підтермами є x та 1; про перший з них маємо такі відомості: x is a divisor of N (береться з локального контексту входження) та x is a natural number (виводиться за один крок з попереднього факту, декларації змінної N та визначення дільника); про другий –is a natural number (береться з множини логічних попередників речення). Якщо серед логічних попередників також є твердження, що сума двох натуральних чисел є натуральним числом, то атом (x + 1) is a natural number буде виведений в один крок і стане відомістю про терм x + 1.
Зауважимо, що сукупності відомостей, які пов’язуються з входженнями термів, дають нам дуже просту, коректну, але, звісно, неповну процедуру “швидкої” перевірки атомарних цілей: маємо лише переглянути відомості про аргументи в цілі.
Тепер повернемось до поняття коректності ForTheL-тексту. Спочатку визначимо “онтологічну коректність”. Неформально, текст є онтологічно коректним, якщо, по-перше, кожному аргументному місцю кожного синтаксичного примітива, що вводиться в тексті, співставлено деяке поняття (тип), і, по-друге, будь-який терм, що зустрічається в цьому аргументному місці, належить до об’єму цього поняття. Сукупність типів аргументних місць фактично задає область визначеності відповідної функції, предиката або поняття. Інакше кажучи, в онтологічно коректному тексті всім синтаксичним примітивам може бути надана теоретико-множинна інтерпретація.
Перша умова задовольняється, якщо кожен синтаксичний примітив вводиться або в розділі “визначення”, або в розділі “сигнатура”. За правилами мови ForTheL, типи аргументних місць явно перелічуються в цих розділах. Визначення онтологічної коректності дозволяє певну омонімію: один синтаксичний примітив може бути введений декілька разів, але вимагається, щоб області визначеності таких омонімів не перетиналися: жоден кортеж аргументів не може одночасно задовольняти двом різним наборам типів.
Друга умова перевіряється наступним чином. Для кожного входження деякого предиката, функції або поняття в формульний образ речення в нормалізованому ForTheL-тексті, ми маємо знайти серед логічних попередників такий розділ типу “визначення” або “сігнатура”, в якому вводиться відповідний синтаксичний примітив, і необхідні твердження про належність аргументів цього входження до об’ємів поняттів-типів є локально істинними в позиції цього входження в формульному образі —тобто локальний образ твердження випливає з множини (формульних образів) логічних попередників .
Далі, ForTheL-текст вважається коректним, якщо він є онтологічно коректним, і, після нормалізації, кожне речення типу “твердження” або “вибір”, що зустрічається всередині розділу “теорема”, випливає з множини своїх логічних попередників (йдеться, звісно, про формульні образи ForTheL-речень та розділів). Зауважимо, що процедура нормалізації ForTheL-тексту має, зокрема, таку властивість: якщо в нормалізованому тексті деяке твердження супроводжується доведенням, і це доведення є коректним (в сенсі попередньої фрази), то й саме це твердження є коректним, тобто випливає з множини своїх логічних попередників. Таким чином, перевіряючи коректність тексту, ми можемо обмежитись лише тими реченнями типу “твердження” або “вибір”, які не супроводжуються доведеннями.
З наведених визначень видно, що встановлення коректності (як онтологічної, так і загальної) ForTheL-тексту зводиться до наступного: для кожного речення в нормалізованому тексті маємо перевірити, що певна сукупність тверджень (цілей) випливає з множини логічних попередників (контексту). Кожна така перевірка постає окремим завданням для ядра системи САД, так званого “міркувальника”.
Для виконання такого завдання в міркувальника є арсенал елементарних дій:
Направити поточне завдання пруверу, с вказанням ліміту часу на перевірку. Оскільки прувер в системі САД працює з формулами першого порядку, речення та розділи ForTheL замінюються їхними формульними образами. Якщо уявити, що в якості прувера ми маємо несхибного оракула, цієї елементарної дії цілком достатньо, і в міркувальнику, як такому, немає потреби. Втім на практиці, завдання, що постають в нетривіальних математичних текстах, виявляються, у їхньому початковому вигляді, занадто складними навіть для найкращих існуючих пруверів.
Якщо цілева формула в поточному завданні є літерою , застосувати “швидку” перевірку, тобто пересвідчитись, чи не міститься серед відомостей про терми-аргументи цілі.
Якщо цілева формула є пропозиціональною комбінацією декількох формул або ж формулою під універсальним квантором, застосувати класичні правила Е. Бета. Ця дія зводить початкове завдання до одного чи декількох (можливо) простіших завдань.
Скоротити контекст завдання, викресливши з нього деякі розділи-попередники.
Розкрити визначення для деякої сукупності входжень, за умови, що відповідний символ введений у розділі типу “визначення”, і онтологічна коректність входження вже перевірена.
Добавити в контекст завдання висновок деякої леми, після того, як перевірено її умови в поточному контексті.
Добавити в контекст деякі відомості про терми, що зустрічаються в завданні.
Послідовність цих дій та їхні параметри (входження, де розкриваються визначення; попередники, що видаляються з контексту; вибір лемм, що застосовуються, та інстанціювання універсальних змінних в них) визначаються в залежності від характеру та вигляду завдання за деяким алгоритмом. В перспективі розвитку системи САД цей алгоритм має надавати користувач системи —у вигляді програми, інтерпретатором якої виступатиме міркувальник.
В існуючій версії системи відповідний алгоритм запрограмовано безпосередньо в міркувальнику. Коротко перелічимо деякі його особливості.
Кожна цільова формула розщеплюється на підформули наскільки можливо.
Кожна літерна ціль перевіряється за “швидкою” процедурою перед тим, як до цього завдання будуть застосовані ще якісь дії. В разі перевірки онтологічної коректності, для літерних цілей ми обмежуємось “швидкою” процедурою.
Розділи типу “визначення” видаляються з контексту перед тим, як завдання віддається пруверу. Ми розраховуємо, що всі необхідні розкриття будуть зроблені міркувальником, і, у такий спосіб, можемо значно скоротити простір пошуку для прувера.
Порядок розкриття визначень встановлюється за такими критеріями, як місцезнаходження входження в тексті (символи, які зустрічаються в цілі, варто розкривати раніше, ніж ті, що взагалі не з’являються в “ближньому околі” поточного речення) та ієрархія визначень (якщо символ визначається за допомогою символу , варто розкривати входження перед входженнями ).
В третій главі вивчається і набуває подальшого розвитку підхід до автоматичного пошуку виведення, прийнятий у програмі “Алгоритм Очевидності”. В попередніх роботах, присвячених цій темі, опис дедуктивної процедури у системі САД ґрунтувався на спеціальних численнях секвенціального типу, що мали наступні характерні риси:
виведення йде у напрямку від цілевої секвенції до аксіом;
виведення є цілекерованим, тобто наступний крок виведення визначається формою формули-консеквента;
початкові формули-антецеденти не змінюються, до них додаються породжені атомарні “леми”;
підстановка у вільні змінні визначається за системою уніфікаційних рівнянь, накопичених впродовж виведення;
початкові формули не сколемізуються, натомість, сукупна підстановка у вільні змінні має задовольняти спеціальній умові припустимості.
Такі властивості системи виведення дозволяють природним чином викласти її у рамках табличного формалізму. Вивідним об’єктом табличного числення є дерево формул, окремий крок виведення полягає у доданні до деякої гілки у цьому дереві нових листів. Виведення починається з єдиної гілки —сукупності формул, чию суперечливість ми намагаємось довести. Виведення вважається завершеним, коли кожна гілка у отриманому дереві містить дві комплементарні літери. Таким чином, цілекеровані секвенціальні числення у стилі АО легко переформулювати як табличні:
початкова секвенція перетворюється на початкову гілку ;
один крок виведення у секвенціальному численні —породження однієї чи декількох секвенцій з консеквентами —відповідає одному кроку виведення у табличному численні —додання до деякої гілки листів , де є формула, комплементарна до ;
атомарні “леми”, накопичені в окремій секвенції, містяться у гілці над вузлом, що відповідає цій секвенції у дереві табличного виведення.
Перший розділ глави визначає поняття та нотацію, що використовуються надалі. У другому розділі викладається цілекероване табличне числення у стилі АО (у тексті —GDT) і встановлюються його зв’язки з традиційним табличним численням Clause Connection Tableau4, більш відомим як Model Elimination (у тексті —CT).
Спочатку доводиться, що за будь-якою підстановкою , припустимою в множині замкнених формул , можна побудувати відповідну підстановку для множини сколемізованих формул : якщо є уніфікатором двох термів з , то буде уніфікатором для відповідних сколемізованих термів (Твердження 2.2). Доведено й зворотне: за будь-якою підстановкою у змінні множини сколемізованих формул можна побудувати відповідну підстановку , припустиму у множині —якщо є є уніфікатором двох термів з , то буде уніфікатором для відповідних термів до сколемізації (Твердження 2.3).
Далі сформульовано рекурсивну процедуру переводу дерева виведення у численні GDT в дерево виведення у численні CT. Підкреслимо, що перше числення працює безпосередньо з множиною початкових формул , тоді як друге —з множиною диз’юнктів , отриманих з початкових формул після сколемізації.
Показано, що ця процедура переводить завершені GDT-дерева у правильно побудовані завершені CT-дерева (Твердження 2.9). Доведено й зворотне: будь-яке правильно побудоване завершене CT-дерево для множини є результатом застосування цієї процедури до деякого завершеного GDT-дерева для множини (Твердження 2.11). Ці твер-дження опосередковано доводять коректність та повноту числення GDT.
Завдяки результатам, отриманим у цьому розділі, чимала кількість відомостей про числення Model Elimination автоматично переноситься на числення GDT і, таким чином, взагалі на цілекерований підхід до пошуку виведення, прийнятий у програмі “Алгоритм Очевидності”. Варто зазначити, що у двотомнику “Handbook of Automated Reasoning”5 застосуванню Model Elimination у автоматичній дедукції присвячено окрему главу.
Третій розділ розповсюджує досліджуваний підхід на логіку з рівністю. Як відомо, класична бінарна резолюція, так само, як і класичне табличне числення, разом з правилом парамодуляції становить коректне і повне числення у класичній логіці першого порядку з рівністю. Але вже така природна стратегія резолюції, як множина підтримки, не є сумісною з парамодуляцією: числення буде повним лише за наявності аксіом функціональної рефлексивності. Обмеження, яке ця стратегія накладає на вибір посилок для чергового кроку виведення виявляється занадто сильним. Схожим чином, правило парамодуляції не може бути прямо перенесене у табличні числення, подібні до Model Elimination, де кожен крок виведення має “зв’язувати” диз’юнкт, що додається до дерева, з деяким вузлом в цьому дереві.
У дисертаційній роботі запропоновано підхід до цієї проблеми, заснований на спеціальному правилі “лінивої парамодуляції”. На відміну від класичної парамодуляції, де ліва частина рівності має бути уніфікована з термом , що заміщується, у лінивій парамодуляції ми вимагаємо лише часткової уніфікації (в запропонованому численні: співпадання головної функціональної літери в термах та ) і формуємо додаткову цілеву формулу (в термінах табличних числень: породжуємо додаткову гілку з листом ). Таким чином, обидва терми “залишаються в виведенні” і можуть бути об’єктами подальших парамодуляцій перед тим, як будуть остаточно уніфіковані. Звісно, часткова уніфікація лінивої парамодуляції дає значно більший простір пошуку ніж стандартна уніфікація в класичному правилі. Це є ціна, яку нам доводиться платити за обмеження перебору за рахунок цілекерованості числення.
В третьому розділі сформульовано числення LPCT —модіфікація числення CT з доданими правилами лінійної парамодуляції та порядковими констрейнтами на термах. Ми оперуємо деревами літер та диз’юнктами заради простоти формулювань і доведень; попередній розділ демонструє, як перейти звідси до числення, що матиме справу безпосередньо з початковими формулами. Для доведення повноти LPCT ми використовуємо один з варіантів методу елімінації рівності (також відомого як “метод модіфікації”). Сутність цього методу полягає у наступному: початкова сукупність диз’юнктів після серії синтаксичних модифікацій перетворюється на таку, що є несуперечливою у логіці без рівності тоді і лише тоді, коли початкова сукупність є несуперечливою у логіці з рівністю. У роботі використано метод елімінації рівності з констрейнтами (CEE), запропонований Бахмайром, Ганцингером та Воронковим6.
Повнота числення LPCT доводиться наступним чином. Початкова суперечлива множина диз’юнктів перетворюється за методом CEE у множину . Якщо є несумісною в логиці з рівністю, то множина може бути спростована у численні CT (з деякими вдосконаленнями) —це нам гарантує метод CEE. Спираючись на синтаксичні властивості диз’юнктів після CEE-перетворень, ми перебудовуємо CT-дерево у дерево спростування множини в численні LPCT.
ПРОВЕДЕНІ ЕКСПЕРИМЕНТИ
В процесі досліджень автором було проведено серію експериментів з формалізації нетривіальних математичних текстів та їхньої верифікації в системі САД. Зокрема, було формалізовано наступні тексти:
доведення нескінченого та скінченого варіантів теореми Рамсея, а також принципу компактності (R.L. Graham. Rudiments of Ramsey Theory. —AMS, 1981);
доведення стабільності відношення уточнення (refinement) над класом специфікаций програм відносно деяких операцій над спеціфікаціями (A. Mammar. Un environnement formel pour le développement d’application bases de données, äисертація на здобуття ступеню PhD, університет Клермон-Ферран, 2003);
доведення деяких властивостей скінчених груп (Ж.-П. Серр. Курс арифметики. —М., “Мир”, 1972);
доведення збіжності ряду зі знакозмінним загальним членом, що монотонно спадає за абсолютним значенням;
доведення ірраціональності квадратного кореня з простого числа;
доведення нерівності Коши-Буняковського для векторів над .
Кожен з цих текстів було записано в мові ForTheL та перевірено на коректність системою САД. Міркування, що проводяться в цих текстах, містять доведення за індукцією, математичні конструкції другого порядку (границі та суми послідовностей, об’єднання сукупностей множин), алгебраїчні та теоретико-множинні перетворення. В експериментах використовувався власний прувер системи САД, заснований на численні GDT, а також резолюційний прувер SPASS, розроблений в Саарбрюкенському університеті (Німеччина).
ВИСНОВКИ
В дисертації автором запропоновано сукупність засобів формального подання математичних знань та їхньої автоматичної обробки з використанням методів природного математичного викладення та міркування. Ці засоби втілено в програмній системі обробки та верифікації формальних математичних текстів.
При виконанні роботи були одержані такі результати:
Розроблено формальну мову ForTheL для запису математичних текстів, близьку до природної англійської мови. Речення та розділи мови ForTheL можуть бути переведені в формули мови першого порядку. Семантика тексту в цілому визначається поставленим завданням (наприклад, перевірити коректність) і ґрунтується на відношенні логічного передування та процедурі нормалізації тексту, яка зводить доведення, проведені за різними схемами, до єдиного уніфікованого вигляду. Визначено різні рівні коректності ForTheL-тексту.
Сформульовано поняття локальної істинності твердження в заданій позиції всередині формули першого порядку. Розглянуто властивості цього поняття, зокрема, показано, що правило modus ponens може застосовуватись локальним чином. Доведена основна властивість локальної істинності: якщо еквівалентність двох формул є локально істинною в заданій позиції, ці дві формули є взаємозамінюваними в цій позиції. Поняття локальної істинності використовується у визначенні онтологічної коректності ForTheL-тексту, а також для теоретичного обґрунтування коректності методів доведення, що застосовують перетворення всередині формул.
Викладено табличне числення GDT, що використовує поняття допустимої підстановки та стратегію цілекерованості в стилі програми “Алгоритм Очевидності”. Доведено коректність і повноту цього числення відносно класичного табличного диз’юнктного числення Model Elimination.
Запропоновано оригінальне цілекероване табличне числення з правилом лінивої парамодуляції LPCT, доведено його повноту.
Реалізовано програмну систему обробки та верифікації формальних математичних текстів, записаних у мові ForTheL. Ця система включає в себе процедури синтаксичного аналізу ForTheL-тексту, трансляції у внутрішнє нормалізоване подання, перевірки онтологічної та загальної коректності, генерації відомостей про окремі входження термів, розкриття визначень та спрощення складних цілей, а також комбінаторний прувер в класичній логіці першого порядку з рівністю, заснований на описаному у роботі цілекерованому табличному численні GDT.
Проведено серію експериментів з формалізації нетривіальних математичних текстів у мові ForTheL та верифікації в системі САД.
СПИСОК ПУБЛІКАЦІЙ
За темою дисертації автором опубліковано наступні роботи:
Паскевич А.Ю. Особливості реалізації мови високого рівня для запису математичних текстів // Вісник КНУ, серія: фізико-математичні науки ——т. 2 —С. 284–88.
Лялецький О.В., Паскевич А.Ю. Про деякі стратегії пошуку логічного виводу, керовані цілями // Вісник КНУ, серія: фізико-математичні науки ——т. 2 —C. 277–.
Паскевич А.Ю. Поняття локальної істинності та його застосування у автоматичному доведенні теорем // Вісник КНУ, серія: фізико-математичні науки — 2003 —т. 1 —C. 199-203.
Вершинин К.П., Лялецкий А.В., Паскевич А.Ю. Применение Системы Автоматизации Дедукции для верификации математических текстов // Научно-теоретический журнал “Искусственный интеллект” ——№3 —C. 57–.
Vershinin K., Paskevich A. ForTheL —the language of formal theories // Proc. of International Conference “Information Theories and Applications 2003” —Varna (Bulgary) ——P. 120–.
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) ——P. 3–.
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) ——P. 236–250.
АНОТАЦІЇ
Паскевич А.Ю. Засоби формалізації математичних знань та міркувань: теоретичні та практичні аспекти. —Рукопис.
Дисертація на здобуття вченого ступеня кандидата фізико-математичних наук за спеціальністю 01.05.01 —теоретичні основи інформатики та кібернетики. —Київський національний університет імені Тараса Шевченка, Київ, 2005.
Дисертацію присвячено вивченню та розробці засобів подання математичного знання та схем математичного міркування. Метою роботи є побудова системи автоматичної обробки формалізованих математичних текстів, зокрема, перевірки їхньої коректності. Мова подання цих текстів наближена до природної мови математичних публікацій; пошук доведення ведеться системою на двох рівнях: верхній рівень виконує великі кроки доведення, застосовуючи традиційні прийоми математичного міркування, а нижній рівень “закриває” породжені підцілі за допомогою комбінаторної процедури пошуку виведення в деякій дедуктивній системі. В дисертації описана формальна мова ForTheL, що імітує синтаксис англійскої мови; сформульовано поняття коректності ForTheL-тексту; розроблено “інструментарій” перевірки коректності: набір евристичних методів верхнього рівня, а також ефективну комбінаторну процедуру на базі цілекерованого табличного числення. Результати роботи втілені в програмному комплексі і апробовані у серії експериментів з нетривіальними математичними текстами.
Ключові слова: формалізація математичного знання, верифікація математичного тексту, автоматичне доведення теорем, цілекеровані числення.
Паскевич А.Ю. Средства формализации математических знаний и рассужденний: теоретические и практические аспекты. —Рукопись.
Диссертация на соискание ученой степени кандидата физико-математических наук по специальности 01.05.01 —теоретические основы информатики и кибернетики. —Киевский национальный университет имени Тараса Шевченко. —Киев, 2005.
Диссертация посвящена изучению и разработке средств представления математического знания и схем математического рассуждения. Цель работы состоит в построении системы автоматической обработки формализованных математических текстов, в частности, проверки их корректности. Язык представления текстов приближен к естественному языку математических публикаций; поиск доказательства ведется на двух уровнях: верхний уровень осуществляет крупные шаги доказательства, применяя традиционные приёмы математического рассуждения, а нижний уровень “закрывает” порожденные подцели с помощью комбинаторной процедуры поиска вывода в некоторой дедуктивной системе. В диссертации описан формальный язык ForTheL, имитирующий синтаксис английского языка; сформулировано понятие корректности ForTheL-текста; разработан “инструментарий” проверки корректности: набор эвристических методов верхнего уровня, а также эффективная комбинаторная процедура на основе целеуправляемого табличного исчисления. Результаты работы воплощены в программном комплексе и апробированы в серии экспериментов с нетривиальными математическими текстами.
Ключевые слова: формализация математического знания, верификация математического текста, автоматическое доказательство теорем, целеуправляемые исчисления.
Paskevich A.Yu. Methods of formalisation of mathematical knowledge and reasoning: theoretical and practical aspects. —Manuscript.
Thesis for the degree of the Candidate of Physics and Mathematics. Science in speciality 01.05.01 —theoretical foundation for the informatics and cybernetics. —Taras Shevchenko Kyiv National University. —Kyiv, 2005.
In the thesis, we study and develop means of presentation of mathematical knowledge as well as schemes of mathematical reasoning. Our research is aimed at constructing a system for automated processing of formalized mathematical texts; in particular, for verifying the text’s claims. The texts being processed are written in a formal language which is close to the natural language of real-life mathematical publications. Proof search is held on two levels of reasoning: the upper one tries to make large proof steps by applying traditional reasoning schemes —it simplifies the initial proof task and splits it into smaller subgoals; the lower one “closes” the generated subgoals using an exhaustive combinatorial inference search in some deductive formalism.
In the first chapter of the thesis, the language ForTheL, intended for representation of formalized mathematical texts, is developed. The syntax of a ForTheL follows the rules of English grammar (though, of course, just a small fragment of English is formalized). Affirmations in ForTheL can be supplied with proofs; special proof schemes like proof by contradiction, by case analysis, or by general induction are allowed. Sentences and sections of ForTheL can be translated into first-order formulas with a series of syntactical transformations. We also introduce a relation of logical precedence between ForTheL sections and define a procedure of proof normalization.
In the second chapter, we define different levels of ForTheL text’s correctness and describe procedures for correctness verification. In order to reason about parts of complex formulas, we introduce the notion of a locally true statement, a statement which can be considered true in a given position inside a given formula. We show that ordinarily valid statements are also locally valid anywhere in any surrounding formula. We introduce a local analogue of the modus ponens rule and prove its soundness. Finally, it is shown that a locally true equivalence is a sufficient condition for an equivalent replacement of a subformula or a subterm. The latter property gives us theoretical ground for definition expansion steps or for applications of simplifying lemmas.
A ForTheL text is said to be ontologically correct whenever the domain of any symbol occurring in the text is properly defined and, in any occurrence of such a symbol, its arguments fall into this domain. Note that the second part of this definition which deals with individual occurrences can be precisely expressed in terms of local validity. A ForTheL text is said to be correct whenever every claim in the text (after proof normalization) follows from its logical predecessors.
Then we describe the verification procedure and a number of heuristic proof methods used on the upper level of the system to transform and simplify proof search tasks before passing them to the lower level, a combinatorial prover.
In the third chapter, we formulate a goal-driven tableau calculus GDT which doesn’t require preliminary skolemization and uses the notion of admissible substitution instead. This calculus is proved to be sound and complete with respect to Model Elimination, a classical clause tableau calculus. Then we introduce an original goal-driven tableau calculus LPCT with lazy paramodulation rules and prove its completeness in the classical first-order logic with equality.
The results of the thesis are implemented in a software system for automated processing and verification of formal mathematical texts. This system, called SAD (System for Automated Deduction) includes ForTheL parser and translator, procedures for checking ontological and general text correctness, routines for collecting facts about particular occurrences of terms, for definition expansion and simplification of compound goals. SAD also includes a prover for classical first-order logic with equality based on the GDT calculus.
The proposed approach was approved in a series of experiments with non-trivial real-life mathematical texts that were formalized in ForTheL and then verified with SAD. These texts include Infinite and Finite Ramsey Theorems and the proof of the fact that the square root of a prime number is irrational.
Keywords: formalization of mathematical knowledge, verification of formal mathematical texts, proof assistance, automated theorem proving, goal-driven calculus.
2Глушков В.М., Вершинин К.П., Капитонова Ю.В. и др. О формальном языке для записи математических текстов. — Автоматизация поиска доказательства теорем в математике. Киев: ИК АН УССР, 1974.
3Дегтярев А.И., Лялецкий А.В. Логический вывод в системе автоматизации доказательств. — Математические основы систем искуственного интеллекта. Киев: ИК АН УССР, 1981.
4Handbook of Automated Reasoning, під редакцією A. Robinson та A. Voronkov — Elsevier Science, 2001, ст. 129–131
5Handbook of Automated Reasoning, під редакцією A. Robinson та A. Voronkov — Elsevier Science, 2001, ст. 2017–2116
6L. Bachmair, H. Ganzinger, A. Voronkov. Elimination of equality via transformation with ordering constraints. — LNAI 1421, Springer Verlag, 1998, ст. 175–190