Логика вычислимости - Logics for computability

Логика вычислимости формулировки логики, которые охватывают некоторые аспекты вычислимость как основное понятие. Обычно это включает в себя сочетание специальных логические связки а также семантика который объясняет, как логика должна интерпретироваться вычислительным способом.

Вероятно, первое формальное рассмотрение логики вычислимости - это интерпретация реализуемости к Стивен Клини в 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.

внешняя ссылка

Смотрите также