정식 증명
Formal proof논리학 및 수학에서 형식 증명 또는 파생은 유한한 일련의 문장(정식 언어의 경우 잘 형성된 공식이라고 함)이며, 각각은 공리, 가정 또는 추론 규칙에 의해 시퀀스의 앞의 문장으로부터 이어진다.그것은 엄격하고 모호하지 않으며 기계적으로 [1]검증 가능하다는 점에서 자연어 논쟁과 다르다.만약 가정들의 집합이 비어있다면, 공식 증명의 마지막 문장은 공식 시스템의 정리라고 불립니다.정리라는 개념은 일반적으로 효과적이지 않기 때문에, 우리가 항상 주어진 문장의 증거를 찾거나 존재하지 않는다고 판단할 수 있는 방법이 없을 수도 있습니다.피치식 증명, 순차 미적분, 자연 연산의 개념은 [2][3]증명 개념을 일반화한 것입니다.
그 정리는 증명에 앞서 잘 형성된 모든 공식의 통사적 결과이다.잘 형성된 공식이 증명의 일부로서 인정되기 위해서는 (일부 정식 시스템의) 연역적 장치의 규칙을 증명 시퀀스의 이전의 잘 형성된 공식에 적용한 결과여야 한다.
형식 증명은 종종 대화형 정리 증명(예를 들어, 증명 검사 및 자동화된 정리 [4]검증기 사용을 통해)에서 컴퓨터의 도움을 받아 구성됩니다.중요한 것은, 이러한 증명은 컴퓨터를 통해서도 자동적으로 확인될 수 있다는 것입니다.공식 증명을 확인하는 것은 보통 간단한 반면, 증명(자동 정리 증명)을 찾는 문제는 일반적으로 사용 중인 공식 시스템에 따라 계산적으로 다루기 어렵거나 반감정만 가능하다.
배경
격식어
형식 언어는 기호의 유한한 일련의 집합이다.이러한 언어는 그 어떤 표현의 의미도 고려하지 않고 정의할 수 있습니다.해석이 할당되기 전, 즉 의미가 부여되기 전에 존재할 수 있습니다.공식 증명은 일부 공식 언어로 표현된다.
형식 문법
형식 문법(형성 규칙이라고도 함)은 형식 언어의 잘 형성된 공식에 대한 정확한 설명입니다.그것은 잘 형성된 공식들을 구성하는 공식 언어의 알파벳 위에 있는 문자열 집합과 동의어이다.단, 의미론(즉, 의미론)은 설명되지 않습니다.
정식 시스템
형식 시스템(논리 미적분 또는 논리 시스템이라고도 함)은 연역 장치와 함께 형식 언어로 구성됩니다.연역적 장치는 변환 규칙 집합(추론 규칙이라고도 함) 또는 공리 집합으로 구성되거나 둘 다 가질 수 있습니다.형식 시스템은 하나 이상의 다른 표현으로부터 하나의 표현을 도출하기 위해 사용된다.
해석
형식체계의 해석은 기호들에 의미를 부여하고, 형식체계의 문장에 진실값을 부여하는 것이다.해석에 대한 연구는 형식적 의미론이라고 불린다.해석하는 것은 모형을 구성하는 것과 동의어이다.
「 」를 참조해 주세요.
레퍼런스
- ^ Kassios, Yannis (February 20, 2009). "Formal Proof" (PDF). cs.utoronto.ca. Retrieved 2019-12-12.
- ^ 케임브리지 철학 사전, 추리
- ^ Barwise, Jon; Etchemendy, John Etchemendy (1999). Language, Proof and Logic (1st ed.). Seven Bridges Press and CSLI.
- ^ Harrison, John (December 2008). "Formal Proof—Theory and Practice" (PDF). ams.org. Retrieved 2019-12-12.
외부 링크
- "A Special Issue on Formal Proof". Notices of the American Mathematical Society. December 2008.
- 2tvsix.com: 논리 수학과 논리를 다루는 일련의 기사의 일부입니다.
- 형식 교정쇄의 아카이브
- Mizar 홈페이지
