26
Z3과 coq의 차이점을 누군가가 알 수 있는지 궁금합니다. Coq는 증거 단계를 채우는 사용자를 요구한다는 점에서 증거 보조자 인 반면 Z3에는 해당 요구 사항이 없습니다. 하지만 coq도 Z3과 비슷한 자동 전술을 가지고있는 것 같습니다. 또는 coq의 증명 검색 기능이 Z3만큼 강력하지 않을 수 있습니까?Z3와 coq의 차이점
A
답변
49
Coq는 대화 형 정리 프로 우 저 (증명 보조자)입니다. 수학 정의, 알고리즘 및 정리를 쓸 수있는 언어를 제공합니다. 또한 기계 검사 증명을 작성하기위한 환경을 제공합니다. Coq는 수학적 정리를 형식화하고 프로그래밍 언어의 의미를 제공하는 데 사용되었습니다. 오늘날 Coq를 사용하는 POPL에서 많은 논문을 찾을 수 있습니다. 어떤 이들은 Coq와 같은 시스템이 미래에 수학자들에 의해 널리 사용될 것이라고 주장합니다. article은 수학의 공식 증명에 대한 매력적인 논쟁 거리입니다. 최근 Georges Gonthier 은 4 색 정리의 측량 가능한 증명을 만들기 위해 Coq를 사용했습니다. Coq은 작고 신뢰할 수있는 핵심을 가지고 있으며 높은 확신을 제공합니다.
Z3은 SMT (만족도 모듈로 이론) 솔버입니다. 이 언어는 산술, 비트 벡터, 데이터 유형, 배열 등과 같은 많은 정렬 된 1 차 논리 + 이론입니다.이 언어는 Coq에서 사용 된 것과 같이 표현이 쉽지 않습니다. Z3도 Coq와 같은 증명 관리를 지원하지 않습니다. Z3은 주로 소프트웨어 테스팅 및 검증에 사용됩니다. 제약 사항, 계획 문제, 퍼즐 등을 해결하는 데에도 사용할 수 있습니다. 만족할만한 공식을위한 모델 (즉, 솔루션)을 찾는 데 많은 부분이 중점을두고 있습니다. article은 Microsoft 및 기타 국가에서 많은 Z3 응용 프로그램을 설명합니다. Z3은 본질적으로 자동 정리 증명 기입니다. Z3에서 전술은 domain specific strategies을 지정하는 데 사용됩니다. 즉, 특정 응용 프로그램 도메인의 문제에 대한 사용자 지정 해결사입니다. Z3은 독립적으로 확인할 수있는 증명/인증서를 생성 할 수 있습니다. 그러나 증거 생성은 Z3 프로젝트의 주요 초점이 아닙니다. 또한 많은 모듈은 증명 생산을 지원하지 않으므로 사용자가 증명 생성을 요청할 때 비활성화해야합니다. Z3은 또한 Isabelle과 같은 증명 보조 장치에 통합되어 있으며 일부는 Z3을 Coq에 통합하는 작업을하고 있습니다. 이 아이디어는 매우 표현력이 강한 언어와 매우 훌륭한 자동화라는 두 가지 장점을 모두 가지고있는 것입니다. Z3은 대규모 응용 프로그램에 포함될 수있는 논리 추론 엔진으로 볼 수도 있습니다. 사실 지금까지 모든 Z3 응용 프로그램에 해당합니다. 최종 사용자는 Z3을 직접 사용하지 않습니다. Isabelle, Pex, VCC 등의 도구 안에 숨겨져 있습니다. Z3 용 new Python front-end은이를 변경하려고 시도합니다.