시퀀트 계산
From Wikipedia, the free encyclopedia
시퀀트 계산(sequent calculus)은 1차 논리나 특수한 명제 논리에서 쓰이는 연역 계산법의 일종으로, 논리식으로 이루어진 특수한 열인 시퀀트를 이용한다. 유사한 수법까지 총칭하여 겐첸 체계(Gentzen system)라고도 불리며, 다른 것들과 구분하기 위해 LK라 특별히 일컫기도 한다.
자연 연역과 유사하게 이미 제시된 식들로부터 추론 규칙에 근거한 추론을 행하여 새로운 식을 이끌어내는 방식이며, 이는 공리에 근거하여 정리들을 나열하는 방식의 증명법을 가진 힐베르트 체계(Hilbert System)와는 대비된다.
시퀀트(sequent)란 논리식의 나열인데, 전건의 명제들의 논리곱을 전제로 삼고 후건의 명제들의 논리합을 귀결로 삼는 것이 특징이다. 곧, "A이고 B이고 C이고 D이고... 이면, (가)이거나 (나)이거나 (다)이거나 (라)이거나...이다."와 같은 식이다. 시퀀트 계산에서 증명은 일련의 시퀀트들의 나열로 기술되는데, 각 시퀀트는 증명과정에서 이미 출현한 시퀀트에 특정 추론규칙을 적용하는 것으로써 도출된다.