Кіріспе
Есептеу қабілеті үшін логика – есептеу қабілетінің кейбір аспектілерін негізгі ұғым ретінде бейнелейтін логикалық жүйелер. Бұл көбінесе арнайы логикалық байланыстардың жиынтығын, сондай-ақ логиканы есептеу тұрғысынан қалай түсінуге болады екенін түсіндіретін семантиканы қамтиды. Бұл саланың алғашқы ресми тұжырымдамасы, шамамен, 1945 жылы Стивен Клиннің жасаған іске асыру интерпретациясы болып табылады, ол интуициялық сан теориясын Тьюринг машинасының есептеулері арқылы түсіндірді. Оның мақсаты – Хейтинг-Брувер-Колмогоров (BHK) интерпретациясын нақтылау болды, сол интерпретацияға сәйкес математикалық тұжырымдардың дәлелдері конструктивті процедуралар ретінде қарастырылуы керек. Модальдық логика және сызықтық логика сияқты көптеген басқа логикалық жүйелердің, сондай-ақ ойын семантикасы сияқты жаңа семантикалық модельдердің пайда болуымен, есептеу қабілеті үшін логика бірнеше контексте қалыптастырылды. Осы жерде екеуін атап өтейік.
capture some aspect of computability as a basic notion. This usually involves a mix
of special logical connectives as well as a semantics that explains how the logic is to be interpreted in a computational way. Probably the first formal treatment of logic for computability is the realizability interpretation by Stephen Kleene in 1945, who gave an interpretation of intuitionistic number theory in terms of Turing machine computations. His motivation was to make precise the Heyting–Brouwer–Kolmogorov (BHK) interpretation of intuitionism, according to which proofs of mathematical statements are to be viewed as constructive procedures. With the rise of many other kinds of logic, such as modal logic and linear logic, and novel semantic models, such as game semantics, logics for computability have been formulated in several contexts. Here we mention two.
Есептеу қабілеті үшін модульдік логика
Клейннің бастапқы іске асырылатын түсіндірмесі есептеу және логика арасындағы байланысты зерттейтін мамандардың көп назарын аударды. 1982 жылы Мартин Хайланд оны толық жоғары реттік интуиционистік логикаға кеңейтті, ол тиімді топосты құрды. 2002 жылы Стив Аводей, Ларс Биркедал және Дана Скотт есептеуге қатысты модальдық логиканы формулирледі, ол "есептеу арқылы анықталған шындық" ұғымын білдіретін екі модальдық оператормен дәстүрлі іске асырылатын түсіндірмені кеңейтті.
Жапаридзедің есептеу логикасы
"Есептеу логикасы" – 2003 жылы Георгий Жапаридзе бастаған зерттеу бағдарламасын білдіретін есім. Оның мақсаты логиканы ойын теориялық семантика негізінде қайта құру. Мұндай семантика ойындарды интерактивті есептеу мәселелерінің формалды эквиваленті ретінде қарастырады, ал олардың "шындығын" алгоритмдік жеңіс стратегияларының болуымен байланыстырады. Есептеу логикасын қараңыз.