계산가능성에 대한 로직

Logics for computability

계산가능성에 대한 로직은 기본적인 개념으로서 계산가능성의 어떤 측면을 포착하는 논리학의 형식이다.이것은 일반적으로 논리가 계산적인 방법으로 해석되는 방법을 설명하는 의미론뿐만 아니라 특별한 논리 결합을 포함한다.

아마도 계산가능성에 대한 논리의 첫 공식적 처리는 1945년 스테판 클린의 실현가능성 해석일 것이다. 그는 튜링 머신 계산의 관점에서 직관적 숫자 이론을 해석했다.그의 동기는 직관주의에 대한 Heyting-Brower-Kolmogorov(BHK) 해석을 정밀하게 하는 것이었는데, 이 해석에 따르면 수학적 진술의 증거는 건설적인 절차로 간주된다.

모달논리와 선형논리와 같은 많은 다른 종류의 논리학, 그리고 게임 의미론 같은 새로운 의미론적 모델들이 부상하면서, 계산가능성에 대한 로직들은 몇 가지 맥락에서 공식화되었다.여기서 두 가지를 언급한다.

계산가능성에 대한 모달 논리학

클린의 독창적인 실현 가능성 해석은 연산성과 논리성의 연관성을 연구하는 사람들 사이에서 많은 관심을 받아왔다.그것은 효과적인 토포를 만든 1982년 마틴 하이랜드에 의해 완전 고차원의 직감적 논리로 확장되었다.2002년에 스티브 어워디, 라스 버커달, 다나 스콧은 "컴퓨터로 진실"이라는 개념을 표현하는 두 모달 연산자로 일반적인 실현가능성 해석을 확장하는 계산가능성에 대한 모달 논리를 공식화했다.

Japaridze의 계산가능성 논리

'컴퓨팅 로직'은 2003년 기오르기 자파리제가 시작한 연구 프로그램을 가리키는 고유 명사다.그것의 야망은 게임 이론적 의미론에서 논리를 재개발하는 것이다.그러한 의미론들은 게임을 대화형 컴퓨터 문제의 공식적 등가물로 보고, 그 "진리"를 알고리즘 승리 전략의 존재로 본다.자세한 내용은 계산 가능성 논리를 참조하십시오.

참조

외부 링크

참고 항목