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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

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

Область застосування[ред.ред. код]

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

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

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

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

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

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

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

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

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

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

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

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

Див. також[ред.ред. код]

Посилання[ред.ред. код]

  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)

Література[ред.ред. код]

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