Спектр логік часткових предикатів, орієнтованих на композиційнo-номінативні моделі програм - Автореферат

Київський національний університет імені Тараса ШевченкаОфіційні опоненти: академік НАН України, доктор фізико-математичних наук, професор ЛЕТИЧЕВСЬКИЙ Олександр Адольфович, Інститут кібернетики імені В.М.Глушкова НАН України, завідувач відділом теорії цифрових автоматів; доктор фізико-математичних наук, професор КРИВИЙ Сергій Лукянович, Київський національний університет імені Тараса Шевченка, професор кафедри інформаційних систем; доктор фізико-математичних наук, старший науковий співробітник ЯДЖАК Михайло Степанович, Інститут прикладних проблем механіки і математики імені Я.С.Підстригача НАН України, провідний науковий співробітник. Захист відбудеться 9 грудня 2010 р. о 14 годині на засіданні спеціалізованої вченої ради Д 26.001.09 Київського національного університету імені Тараса Шевченка за адресою: 03127, Київ, пр. акад. Для неокласичних логік побудовано і досліджено числення гільбертівського типу та ґенценівського (секвенційного) типу, для них доведені теореми коректності й повноти, отримано важливі наслідки теореми повноти. Запропоновано і досліджено різні формалізації відношення логічного наслідку для композиційно-номінативних логік часткових однозначних, тотальних та часткових неоднозначних квазіарних предикатів. На базі логіки квазіарних предикатів як основи побудови спеціальних логік запропоновано композиційно-номінативні модальні та темпоральні логіки, збудовано та досліджено логіки над ієрархічними номінативними даними.Зазначений підхід дає можливість застосування побудованих моделей як в програмуванні, так і в логіці, що дозволяє природним чином поєднати логіку з програмуванням. Основою такої побудови в дисертаційній роботі вибрано спільний для логіки і програмування композиційно-номінативний підхід. Дисертаційна робота виконувалась у відповідності до плану наукових досліджень кафедри теорії та технології програмування Київського національного університету імені Тараса Шевченка в межах таких науково-дослідних тем: "Дослідження універсальних та спеціалізованих прикладних логік" (1996-2000, ДР № 0197U003444), "Логіко-математичні та програмологічні засоби інформаційних технологій" (2001-2005, ДР № 0101U002163), "Розробка конструктивних математичних формалізмів для інтелектуальних систем прийняття рішень, обробки знань, еталонування мов сучасних СУБД і CASE-засобів" (2006-2010, ДР № 0106U005856), "Формальні специфікації програмних систем" (2008-2009, ДР № 08U002463). Відповідно до сформульованої мети, в дисертації ставляться такі задачі: - на основі спільного для логіки й програмування композиційно-номінативного підходу побудувати й дослідити класи логік часткових предикатів на різних рівнях абстрактності й загальності; проілюструвати можливості логіки квазіарних предикатів побудовою на її основі спеціальних логік: композиційно-номінативних модальних логік, а також логік, орієнтованих на опис поширених в програмуванні відображень над даними із складною структурою.Мотивовано необхідність перебудови логіки в семантико-синтаксичному стилі та обгрунтовано провідну роль алгебраїчних і композиційно-номінативних аспектів для побудови нових логік, орієнтованих на дослідження програм. Обмеження класичної логіки предикатів мотивують необхідність побудови нових логік, більше орієнтованих на потреби програмування. На цій основі можна зробити висновки, які є основоположними для побудови програмно-орієнтованих логік, вони визначають провідну роль для цих логік алгебраїчних та композиційно-номінативних аспектів. На цьому рівні модель світу задається певним класом D станів, які назвемо даними, класом предикатів Pr, заданих на станах світу, та операторами (композиціями) породження нових предикатів. Така система задає дві алгебри: алгебру (алгебраїчну систему) даних (D, Pr) та алгебру предикатів (Pr, C), терми якої трактуються як формули мови логіки.Позначимо nm(F) множину всіх предметних імен, які фігурують у символах реномінації формули F, s(F) - множину всіх предикатних символів формули F. Для формул РНЛ еквітонних предикатів встановлено (теорема 2.5) критерій неістотності предметних імен: XIV неістотне для F U для кожного VIV |= F« . Для загального випадку квазіарних предикатів теорема формулюється так: Теорема 2.9S. В загальному випадку це гарантує теорема 3.3S, для еквітонних предикатів-теорема 3.3: Теорема 3.3. Доводиться (теореми 3.13, 3.13S): для кожної F можна збудувати нормальну (стандартну нормальну) формулу ? таку, що |= F«?; для кожної F можна збудувати строго нормальну (стандартну строго нормальну) формулу ? таку, що F ~TF ?.На основі розвитку поняття даного виділено рівні розгляду, які визначають інтенсіональні моделі композиційно-номінативних логік. Запропоновано спектр таких логік за рівнем абстракції розгляду та за обмеженнями на клас квазіарних предикатів. Досліджено композиції та композиційні системи квазіарних функцій і предикатів на пропозиційному, реномінативному та першопорядкових рівнях: кванторному, кванторно-екваційному, функціональному, функціон

2. ОСНОВНИЙ ЗМІСТ