Розроблено систему взаємопов'язаних адекватних моделей символьної обробки (СО). Моделі відображають семантику програм СО як функцій над символьними даними визначеної структури. Досліджено визначні конкретні різновиди структури символьних даних (літерну зіставленість, конкатенацію, ієрархію) та відповідні їх засоби обробки. Запропоновано узагальнену математичну модель поняття структури символьних даних у термінах операції синтезу та аналізу. За методом композиційного програмування змодельовано типові засоби побудови програм СО та логіки їх структурної організації. Для моделей суттєво різних типів СО показано можливість виразити одну в одній, чим підтримується концептуальна єдність предмета. Моделі грунтуються на аналізі суті та змісту предмета для їх точного відображення. Відзначено, що розроблені моделі СО є конкретизаціями моделей загальнозначущих структур програмування, що забезпечує їх інтеграцію в середовище моделей інших галузей програмування.

  Скачати повний текст

На базі мови TL розвинуто формальну мову подання математичних текстів ForTheL, що є близькою за синтаксисом до природної англійської мови і може бути перекладена в мову першого порядку. Сформульовано поняття коректності тексту у мові ForTheL. Запропоновано оригінальне поняття істинності твердження у деякій позиції всередині формули першого порядку та досліджено його властивості. Доведено, що за умов еквівалентності двох формул, що є локально істинною у заданій позиції, ці дві формули є взаємозамінюваними у цій позиції. Відзначено, що поняття локальної істинності дозволяє обгрунтувати коректність різноманітних перетворень складних формул, а саме: розкриття визначень або додання допоміжних тверджень всередині формули. Запропоновано процедуру породження "відомостей" про окремі входження термів у досліджуваний ForTheL-текст; ці відомості є літерами, локально істинними у відповідному входженні, зокрема, вони несуть інформацію про тип терму. На базі цього апарату сформульовано декілька високорівневих схем доведення, які становлять "інструментарій" міркувальника. Проведено дослідження цілекерованих процедур пошуку виведення, що використовуються у програмі "Алгоритм Очевидності". Запропоновано нове доведення коректності поняття допустимої підстановки. Викладено цілекероване табличне числення, що оперує несколемізованими формулами. Доведено, що виведення у цьому численні можуть бути перетворені у виведення у класичному табличному диз'юнктному численні Model Elimination. Доведено можливість зворотнього перетворення. Запропоновано нове табличне цілекероване числення з лінивою парамодуляцією для класичної логіки першого порядку з рівністю, доведено його повноту.

  Скачати повний текст

Розроблено, досліджено та використано нові методи в теорії мовних перетворювачів, які застосовуються під час вирішення проблем, пов'язаних з різними напрямками інформатики, а також теорії та практики моделювання систем. Розроблено методологію використання теоретико-категорних форм для дослідження проблем теорії формальних мов і перетворення мовної інформації. Ця методологія дозволяє здійснювати категорне подання синтаксису та семантики мов, побудову категорних автоматів, аналіз проблем обчислюваності категорій. Запропоновано декілька різних варіантів мовних перетворювачів, які використовують різні схеми пам'яті. Розроблено метод категоріальних систем, що дозволяє послідовно будувати перетворювачі з заданими ознаками та досліджувати їх особливості. Вирішено проблему розв'язуваності існування несинхронного скінченного перетворювача, який відображає одну регулярну мову на іншу. У загальному вигляді вирішено проблему еквівалентності детермінованих магазинних автоматів, що дозволило вирішити певні інші проблеми, які належать до різних напрямків теоретичної інформатики - теорії мов, схем програм, теорії формальних граматик. Розроблено методологію застосування мовних перетвоювачів до проблем автоматизації проектування систем управління, пов'язаних з задачами моделювання систем і формалізацією процесів автоматизованої обробки інформації.

  Скачати повний текст

Розроблено спеціалізовану програмну алгебру, носієм якої виступають функції, а в якості сигнатурних операцій використовуються композиції (оператори), що задає множину семантичних функцій мови SQL, базуючись на структурі мови, а також враховує такі властивості SQL, як задання таблиць на базі мультимножин, невизначені значення та трьохзначну логіку. Одержані результати застосовано для уточнення семантики мови SQL, у побудові навчальних курсів, що читаються в Київському національному університеті імені Т. Шевченка, в Ніжинському державному університеті імені М.В. Гоголя та Кіровоградському державному педагогічному університеті імені В. Винниченка, під час уточнення семантики складних запитів до реляційних баз даних.

  Скачати повний текст

Розглянуто нові природні визначення збіжності спрямованості над частково впорядкованою множиною з "достатньою кількістю" супремумів і інімумів. На підставі цих визначень введено поріднені, але різні поняття неперервної функції через властивість функції зберігати відповідні ліміти спрямованостей. Проведено порівняльний аналіз цих понять з їх загально відомими аналогами, такими як неперервність за Скоттом, (о)-неперервність і топологічна неперервність. Наведено абстрактні теоретико-порядкові характеризації властивості функції "бути неперервною" в контексті кожного з нових понять. На основі нових понять неперервної функції за допомогою характеризаційних теорем досліджено можливість побудови за методом К. Койманса нових моделей теорії лямбда. Встановлено, що одне з цих понять призводить лише до тривіальних лямбда-моделей, в той час як інші два нові поняття індукують нові "неперервні" лямбда-моделі. Побудовано приклади "неперервних", але нетопологізуючих моделей теорії лямбда.

  Скачати повний текст