프루프 네트

증명 이론에서, 증명 그물은 증거를 구별하는 두 가지 형태의 관료주의를 제거하는 기하학적 방법이다: (A) 자연적 추론 미적분학, 순열 미적분학 등 정규 증명 미적분학의 관계없는 구문론적 특징과 (B) 파생에서 적용되는 규칙의 순서.이와 같이 증명정체성의 형식적 성질은 직관적으로 바람직한 성질에 더욱 밀접하게 대응한다.증명 그물은 장 이브 지라드가 도입했다.

예를 들어, 이 두 개의 선형 논리 증명서는 동일하다.

$\displaystyle \vdash }$ A,B,C,D $\displaystyle \vdash }$ A⅋B,C,D $\displaystyle \vdash }$ A⅋B,C⅋D

$\displaystyle \vdash }$ A,B,C,D $\displaystyle \vdash }$ A,B,C⅋D $\displaystyle \vdash }$ A⅋B,C⅋D

그리고 그들의 그에 상응하는 그물도 같을 것이다.

정확성 기준

몇 가지 정확성 기준은 순차적 증명 구조(즉, 증명망으로 보이는 것)가 실제로 구체적인 증명 구조(즉, 선형 논리로 유효한 파생을 인코딩하는 것)인지 확인하는 것으로 알려져 있다.첫 번째 그러한 기준은 장 이브 지라드가 설명한 장거리 기준이다^[1].

참고 항목

• 선형 논리학
• 루딕스
• 교호작용 기하학
• 일관성 있는 공간
• 깊은 추론
• 인터랙션 네트

참조

원천

• 증명 및 유형.Girard J-Y, Lafont Y, 그리고 1989년 Taylor P. Cambridge Press.
• 로베르토 디 코스모와 빈센트 다노스, '선형 논리 입문서'
• Sean A. Fulop, 하부구조물 로직의 교정망 및 행렬 조사