Знайди книгу!

Опис:
Аввад М. Роль логіки в історії та філософії комп’ютерних наук. -
Кваліфікаційна наукова праця на правах рукопису.

Дисертація на здобуття наукового ступеня кандидата філософських наук
за спеціальністю 033 - Філософія - (Гуманітарні науки). Київський
національний університет імені Тараса Шевченка, Київ, 2021.

Результати цієї дисертації відповідають двом її основним
частинам. Перша присвячена дослідженню місця логіки у філософії
комп’ютерних наук та штучного інтелекту. Друга - це дослідження
впливу логіки на розвиток комп’ютерних наук та штучного інтелекту.

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


3

когнітивні логічні обчислення, які, наприклад, використовуються при
маніпулюванні знанням.

У цій частині ми наводимо критичні аргументи проти точки зору
радикального комп’ютаціоналізма, підкреслюючи різницю між
пізнанням як динамічною, але неточно визначеною людською
складовою та дуже чітко визначеною моделлю обчислень,
представленою в МТ. Цим припускається певна суттєва різниця між
пізнанням, яке можливо повністю виміряти / кваліфікувати, і машиною
Тюрінга, де це не можливо. Крім того, порівнюючи пізнання з
обчисленнями, ми торкнулися проблем сприйняття і свідомості як
понять з невизначеною обчислюваністю. Також пропонується
скептичний погляд щодо радикального гіперкомп’ютаціоналізма, який
ґрунтується на складностях відшукати переконливу цілісну
відповідність між людським пізнанням та гіперкомп’ютаційними
моделями.

Що стосується питання морального статусу та моральної
відповідальності роботів, то в даній дисертації ми стверджуємо, що
моральна відповідальність має бути наслідком існуючого морального
статусу. Крім того, ми вважаємо, що володіння свідомістю є необхідною
умовою для надання морального статусу. Тому, на думку автора,
інтелектуальні машини не мають жодного морального статусу за
відсутності свідомості. Отже, ми дійшли висновку, що роботи не несуть
ніякої етичної відповідальності, і ми показуємо небажані наслідки для
людей, якщо припустити протилежну ситуацію. Нарешті, ми піднімаємо
в цій частині проблему прозорості обчислень і показуємо, як обчислення


4

на основі логіки часто виявляється прозорішим, ніж за використання
інших методів, таких як складні нейронні мережі.

У другій головній частині цієї дисертації ми аналізуємо теоретичні
та практичні впливи логіки на комп’ютерні науки. Ми технічно
пояснюємо, як Булева алгебра логіки еволюціонувала у Булеву логіку
шляхом модифікації та адаптації своїх початкових законів. Потім ми
показуємо, як ця нова логіка мала вирішальне значення 1) при
проектуванні та аналізі сучасних схем, 2) при розробці криптографії, 3)
при використанні коректуючого коду.

Друга складова цієї частини присвячена впливам з боку логіки
предикатів Фреге. Описавши її високу виразність, ми детально
показуємо, як відповідність між інтерпретаціями Ковальського та
логікою предикатів призвела до фундаментальної семантичної
еквівалентності між диз'юнктами Горна та логічним програмуванням.
Потім ми надаємо докази ефективності правила резолюцій та диз'юнктів
Горна в логічних розрахунках, зокрема в автоматизованому доведенні
теорем. Одним із таких доказів є метод уніфікації, розгорнутий як
техніка створення реального часу, поки будується доказ теореми; ця
операція часто дозволяє уникнути експоненціального часу виконання.

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


5

ролі типу даних при низькорівневому представленні пам'яті та на
цілісності коду. Ми виокремлюємо вплив теорії типів на абстрагування
даних, поліморфізм та успадкування. Крім того, ми демонструємо
очевидність зв’язку між лямбда-численням та обмеженою
квантифікацією з субтипуванням.

Друга частина цього дослідження, серед іншого, досліджує вплив
логіки на штучний інтелект. Зокрема, ми показуємо роль логіки
предикатів в системах автоматизованого доведення теорем (AДТ) за
допомогою мов логічного програмування, таких як Пролог. У цьому
контексті ми намічаємо значну подібність між функціонуванням логіки
предикатів Фреге та логіки Пролог. Ми помічаємо, що Пролог створює
список істин та уніфікацій цілей, які досягаються, автоматично
використовуючи при цьому техніку пошуку з вертанням, щоб збільшити
кількість вирішень. Потім ми проводимо паралель з логікою Фреге, яка
спрямована на створення процесу генерування нових зростаючих істин
на основі засновків та набору правил. Після цього, ми підкреслюємо
різницю між машинно-орієнтованим і орієнтованим на людину
обчисленням правил у контексті процедури співставлення/створення.

Ми досліджуємо використання індуктивного логічного
програмування (ІЛП) у штучному інтелекті та представляємо вибірку
успішних застосунків. Зокрема, ми надаємо докази впливу логіки
першого порядку на методи пошукових систем, ігрові стратегії та
поведінку користувачів у мобільних царинах.

Крім того, ми простежуємо плідну взаємодію між штучним
інтелектом та теорією аргументації. Ми показуємо, які принципи


6

міркування теорії аргументації можливо застосувати у штучному
інтелекті. Немонотонна логіка тут представлена як типовий приклад
логіки, що з’явилася внаслідок розвитку комп’ютерних наук. Її роль
особливо підкреслюється в застосуваннях ШІ і відображена в
переконливих міркуваннях теорії аргументації.
Отримані нами результати в галузі історії обчислювальної логіки
в основному полягають у виокремленні та аналізі основних ідей
обчислення за допомогою логіки, що розвивалися в період від епохи
Ляйбніца і до ХХ століття. Ми окремо досліджуємо універсальну
обчислювальну машину Ляйбніца, яка мала бути практичною
реалізацією його універсальної мовної характеристики та універсальної
системи логічного числення (calculus ratiocinator) як символічної логіки.

Після відзначення провідної історичної ролі алгебри логіки Буля,
ми приділяємо особливу увагу прориву логіки предикатів, який Фреге
здійснив під час розробки програми логіцизму. Разом із цим, як уже
зазначалося, показано очевидність визначального впливу цих подій на
логіку та комп’ютерні науки. В історичному розгляді ми виявляємо
також і інші великі досягнення логіки, такі як теорія типів Рассела, теорія
доказів Гільберта, теореми Геделя про неповноту, а також зупиняємося
на принципах логіки, які узгоджуються з останніми досягненнями
комп’ютерних наук в двадцятому столітті.

Ключові слова: сучасна логіка, комп’ютерні науки (І), історія
логіки, філософія комп’ютерних наук, філософія свідомості, штучний
інтелект (ШІ), обчислення, інформація, Булева логіка, логіка предикатів,
теорія типів, логічне програмування, інтелектуальні агенти, індуктивне


7

навчання, машинне навчання, робототехніка, теорія аргументації,
нейронні мережі, пізнання, комп'ютаціоналізм, етичне обчислення.