Логіка в інформатиці

Матеріал з Вікіпедії — вільної енциклопедії.

Логіка в інформатиці — це напрям досліджень та галузей знань, де логіка застосовується в інформатиці та штучному інтелекті. Використання логіки дуже ефективне в цих областях^[1].

Область застосування

Включаються такі основні застосування:

• дослідження в логіці, викликані розвитком комп'ютерних наук. Наприклад, аплікативні обчислювальні системи, теорія обчислень і моделі обчислень;

• формальні методи і логіка міркування про поняття. Наприклад, семантична мережа^[2], семантична павутина;

• булева логіка і алгебра для розробки апаратного забезпечення комп'ютерів;

• розв'язання задач і структурне програмування для розробки прикладних програм і створення складних систем програмного забезпечення

• доказове програмування — технологія розробки алгоритмів і програм із доказами правильності алгоритмів;

• фундаментальні поняття і уявлення для комп'ютерних наук, які є природною областю для формальної логіки. Наприклад, семантика мов програмування^[3];

• логіка знань і припущень. Наприклад, штучний інтелект;

• мова Пролог і логічне програмування для створення баз знань та експертних систем і досліджень у сфері штучного інтелекту;

• логіка для опису просторового положення і переміщення;

• логіка в інформаційних технологіях. Наприклад, реляційна модель даних, реляційні СКБД, реляційна алгебра, реляційне числення^[4];

• логіка обчислень з об'єктами. Наприклад, комбінаторна логіка, суперкомбінатори^[5];

• логіка для компілювання програмного коду та його оптимізації. Наприклад, категоріальна абстрактна машина;

• логіка для еквівалентного перетворення об'єктів. Наприклад, лямбда-числення;

• перевиклад логіки і математики в термінах, зрозумілих фахівцям в комп'ютерних науках^[6].

Цей список продовжує поповнюватися.

Ефективність логіки в комп'ютерних науках

На відміну від природничих наук, комп'ютерні науки отримали великий стимул від широкої і безперервної взаємодії з логікою. Особливу роль у комп'ютерних науках відіграють доказові методи розробки алгоритмів і програм з доказами їхньої правильності.
Тестування програм може виявити наявність помилок у програмах, але не може гарантувати їх відсутність. Гарантії відсутності помилок в алгоритмах і програмах можуть дати тільки докази їх правильності. Алгоритм не містить помилок, якщо він дає правильні розв'язки для всіх допустимих даних.
Серйозною проблемою для комп'ютерних наук та інформатики є наявність помилок в алгоритмах і програмах, що публікуються в підручниках і навчальних посібниках, а також невміння викладачів і вчителів інформатики виявляти і виправляти помилки в алгоритмах і програмах, складених учнями.
Єдиний шлях для подолання цих проблем-це вивчення систематичних методів складання алгоритмів і програм з одночасним аналізом їх правильності в рамках доказового програмування з самого початку навчання основам алгоритмізації і програмування.
Складність для викладачів і програмістів полягає в тому, що вони повинні вміти писати не тільки алгоритми і програми, а й докази правильності своїх алгоритмів і програм. На жаль, зараз це не вміють робити ні математики, ні програмісти.
В результаті програмісти пишуть програми з великим числом помилок, які вони не можуть ні виявити, ні виправити. Масоване тестування програм на ЕОМ приносить програмістам безперечну користь, проте не дає гарантій повного позбавлення від помилок.
Практика застосування та вивчення доказових методів програмування показала, що ця технологія цілком доступна студентам математичних факультетів, яким цілком під силу написання доказів правильності алгоритмів, після перевірки та тестування програм на ЕОМ.
Найбільший ефект в освоєнні технологій доказового програмування спостерігається в олімпіадах з інформатики та програмування, де переможцями та призерами стають ті студенти, які освоїли техніку тестування програм на ЕОМ і складання алгоритмів і програм без помилок.