WikiDer > Логика вычислимости
Логика вычислимости формулировки логики, которые охватывают некоторые аспекты вычислимость как основное понятие. Обычно это включает в себя сочетание специальных логические связки а также семантика который объясняет, как логика должна интерпретироваться вычислительным способом.
Вероятно, первое формальное рассмотрение логики вычислимости - это интерпретация реализуемости к Стивен Клини в 1945 году, который дал интерпретацию интуиционистской теории чисел с точки зрения Машина Тьюринга вычисления. Его мотивацией было уточнить Интерпретация Гейтинга-Брауэра-Колмогорова (БХК) интуиционизма, согласно которому доказательства математических утверждений следует рассматривать как конструктивные процедуры.
С появлением многих других видов логики, таких как модальная логика и линейная логикаи новые семантические модели, такие как семантика игры, логика вычислимости была сформулирована в нескольких контекстах. Здесь мы упоминаем два.
Модальная логика для вычислимости
Первоначальная интерпретация реализуемости Клини привлекла большое внимание тех, кто изучает связи между вычислимостью и логикой. Он был расширен до полной высшей степени интуиционистская логика к Мартин Хайланд в 1982 году, который построил эффективные топосы. В 2002, Стив Awodey, Ларс Биркедал, и Дана Скотт сформулировал модальная логика для вычислимости который расширил обычную интерпретацию реализуемости двумя модальными операторами, выражающими понятие «вычислимо истинного».
Логика вычислимости Джапаридзе
«Логика вычислимости» - это имя собственное, относящееся к исследовательской программе, инициированной Георгий Джапаридзе в 2003 году. Его цель - перестроить логику из теоретико-игровой семантики. Такая семантика рассматривает игры как формальные эквиваленты интерактивных вычислительных задач, а их «истину» - как существование алгоритмических выигрышных стратегий. Видеть Логика вычислимости.
Рекомендации
- S.C. Kleene. Об интерпретации интуиционистской теории чисел. Журнал символической логики, 10: 109-124, 1945.
- J.M.E. Хайленд. Эффективные топосы. В A. S. Troelstra и Д. Ван Дален, редакторы, The L.E.J. Столетний симпозиум Брауэра, страницы 165-216. Издательство Северной Голландии, 1982.
- С. Аводи, Л. Биркедал и Д.С. Скотт. Топозы локальной реализуемости и модальная логика вычислимости. Математические структуры в информатике, 12 (3): 319-334, 2002.
- Г. Джапаридзе, Введение в логику вычислимости. Анналы чистой и прикладной логики 123 (2003), страницы 1–99.
внешняя ссылка
- Логика типов и вычислений в CMU
- Домашняя страница Computability Logic
- Георгий Джапаридзе
- Семантика игр или линейная логика?