Логіка в інформатиці: відмінності між версіями

Вилучено вміст Додано вміст

Лінійно

Версія за 14:56, 7 червня 2013

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

На відміну від природничих наук, комп'ютерні науки отримали великий стимул від широкої і безперервної взаємодії з логікою. Особливу роль у комп'ютерних науках відіграють доказові методи розробки алгоритмів і програм з доказами їхньої правильності.

Тестування програм може виявити наявність помилок у програмах, але не може гарантувати їх відсутність. Гарантії відсутності помилок в алгоритмах і програмах можуть дати тільки докази їх правильності. Алгоритм не містить помилок, якщо він дає правильні рішення для всіх допустимих даних.

Серйозною проблемою для комп'ютерних наук та інформатики є наявність помилок в алгоритмах і програмах, що публікуються в підручниках і навчальних посібниках, а також невміння викладачів і вчителів інформатики виявляти і виправляти помилки в алгоритмах і програмах, складених учнями.

Єдиний шлях для подолання цих проблем-це вивчення систематичних методів складання алгоритмів і програм з одночасним аналізом їх правильності в рамках доказового програмування з самого початку навчання основам алгоритмізації і програмування.

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

В результаті програмісти пишуть програми з великим числом помилок, які вони не можуть ні виявити, ні виправити. Масоване тестування програм на ЕОМ приносить програмістам безперечну користь, проте не дає гарантій повного позбавлення від помилок.

Практика застосування та вивчення доказових методів програмування показала, що ця технологія цілком доступна студентам математичних факультетів, яким цілком під силу написання доказів правильності алгоритмів, після перевірки та тестування програм на ЕОМ.

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

Дивіться також

Посилання

↑ Halpern J.Y., Harper R., Immerman N., Kolaitis Ph.G., Vardi M.Y., and Vianu V. On the unususal effectiveness of logic in computer science. — January, 2001.
↑ Roussopoulos N.D. A semantic network model of data bases. — TR No 104, Department of Computer Science, University of Toronto, 1976.
↑ Scott D.S. The lattice of flow diagrams.-- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.-- Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp.~311-372.
↑ Codd E. F. Relational Completeness of Data Base Sublanguages. In: R. Rustin (ed.): Database Systems: 65-98, Prentice Hall and IBM Research Report RJ 987, San Jose, California, 1972.
↑ Peyton Jones S., Eber J.-M., Seward J. Composing contracts: an adventure in financial engineering. — ICFP 2000
↑ Asperti A, and Longo G. Categories, Types and Structures. Category Theory for the working computer scientist. — M.I.T. Press, 1991 (pp. 1-300)

Література

Вольфенгаген В. Э. Логика. Конспект лекций: техника рассуждений. 2-е изд., дополн. и перераб. — М: АО «Центр ЮрИнфоР», 2004. — 229 с ISBN 5-89158-135-3.

Це незавершена стаття з логіки.
Ви можете допомогти проєкту, виправивши або дописавши її.

[1] Halpern J.Y., Harper R., Immerman N., Kolaitis Ph.G., Vardi M.Y., and Vianu V. On the unususal effectiveness of logic in computer science. — January, 2001.

[2] Roussopoulos N.D. A semantic network model of data bases. — TR No 104, Department of Computer Science, University of Toronto, 1976.

[3] Scott D.S. The lattice of flow diagrams.-- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.-- Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp.~311-372.

[4] Codd E. F. Relational Completeness of Data Base Sublanguages. In: R. Rustin (ed.): Database Systems: 65-98, Prentice Hall and IBM Research Report RJ 987, San Jose, California, 1972.

[5] Peyton Jones S., Eber J.-M., Seward J. Composing contracts: an adventure in financial engineering. — ICFP 2000

[6] Asperti A, and Longo G. Categories, Types and Structures. Category Theory for the working computer scientist. — M.I.T. Press, 1991 (pp. 1-300)

[1]

[2]

[3]

[4]

[5]

[6]