Coq에 비해 Isabelle 증명 보조의 강점과 약점은 무엇입니까?

Coq에 비해 Isabelle 증명 보조의 강점과 약점은 무엇입니까?

---

Isabelle / HOL 증명 도우미는 Coq에 비해 약점과 무릎이 있습니까?

---

저는 대부분 Coq에 익숙하고 Isabelle / HOL에 대한 경험이 많지 않지만 약간 도움이 될 수 있습니다. Isabelle / HOL에 대해 더 많은 경험이있는 다른 사람들이이를 개선하는 데 도움이 될 수 있습니다.

두 시스템 사이에는 두 가지 큰 차이가 있습니다. 기본 이론 과 상호 작용 스타일입니다 . 각 경우의 주요 차이점에 간략히 설명하겠습니다.

이론

Coq와 Isabelle / HOL은 모두 강력하고 표현력이 뛰어난 고차 논리를 기반으로합니다. 그러나 논리는 몇 가지 기능에서 기능합니다.

존재 유형

COQ 논리는의 유도 구조 의 미적분 ( 줄여서 CIC )으로 알려진 종속 유형 이론 입니다. 여기서 "종속 유형"은 Coq의 유형이 일반 값을 참조 할 수 있음을 의미합니다. 예를 들어 다음 mult과 같은 유형 의 많은 곱셈 함수 를 사용 합니다.

mult : forall (n m p : nat), matrix n m -> matrix m p -> matrix n p

이 함수의 유형은 두 개의 행렬 을 입력으로 취하고 ,는-dimensional 하나 n x m이고 다른 하나는-dimensional m x p이고, 행렬을 반환-dimensional 한다고 말합니다 n x p. 반면에 Isabelle / HOL 이론은 존재 유형을 가지고 있습니다. 따라서 mult위와 같은 유형 의 함수를 사용할 수 없습니다 . 대신 모든 종류의 주문에 대해 작동하는 함수를 작성 하고 올바른 종류의 인수를받을 때이 함수를 사후 특정 속성을 증명해야 합니다 . 즉, Coq 유형으로 명시되는 특정 속성은 Isabelle / HOL 작업 할 때 별도의 정리되어야한다고 주장합니다.

어떤 것에는 흥미롭지 만 일반적으로 유용한 것이 명확하지 않습니다. 내 인상은 어떤 사람들은 사용하기가 매우 복잡하고 유형 수준에서 특정 속성을 표현하는 것보다 별도의 정리로 수행 할 것의 이점이 추가의 가치가 있고 느낀다는 것입니다. 개인적으로 명확한 이유가있는 경우에는 존재하는 것을 좋아합니다.

기본 추론 원리

기본적으로 Coq의 이론은 배제 된 중간의 법칙 (즉, 비 구조적으로 추론 할 수있는 능력), 확장 성 (예 : 동일한 결과를 생성하는 함수를 말할 수 있음) 과 같이 수학적 실습에서 볼 수있는 론 원리가 많이 없습니다. 그들 자신은 동등 함), 그리고 선택의 공리. 반면 Isabelle / HOL에서는 기본적으로 내장되어 있습니다.

이론적으로는 큰 문제가 아닙니다. Coq의 논리는 사람들이 기본 추론 원칙을 추가 공리로 안심하고 신뢰할 수 있도록 설계되었습니다. 그럼에도 불구하고 Isabelle / HOL은 추론을 수행하는 것이 더 많은 것을 수행합니다. 논리가 처음부터이를 지원하기 위해 만들어 졌기 때문입니다.

(코크의 논리에서 기본 원칙을 벗어난 이유가 무엇인지 궁금 할 수 있습니다. 동기는 철학적입니다. Coq의 핵심 논리에서 증명은 논리에 건설적인 풍미를 부여하는 실행 가능한 프로그램으로 볼 수 있습니다. 제외 된 것을 거부하는 이유 중간 예를 들어, 그거 분리의 증명 A \/ B프로그램에 해당하는 반환 중 하나를 나타내는 비트 A또는 B사실입니다. 따라서, 제외 된 가운데이 존재하지 수있는 모든 수학 문제를 결정하는 프로그램에 해당하는을 구석으로 이 질문을 문제 에 대해 조금 더 논의합니다.)

상호 작용 스타일

Coq와 Isabelle / HOL은 모두 대화 형 정리 증명 입니다. 설명에 대한 정의와 증명을 작성하기위한 언어입니다. 이러한 증명은 실수가 없는지 확인하기 위해 컴퓨터로 확인됩니다. 두 시스템 모두 어떤 것을 증명하는 방법을 설명하는 명령을 제공하여 증명을 기록합니다. 그러나 그것은 각 시스템에서 발생하는 방식은 다양합니다.

Isabelle / HOL은 일반적으로 "푸시 버튼"증명 자동화에 대한보다 작성 지원을 제공합니다. 예를 들어, 그것은 sledgehammer정리를 증명하기 위해 여러 외부 자동 정리 증명 자와 해결 튼 호출 하는 유명한 전술 과 함께 제공 됩니다. COQ는 또한 많은 증거 증거 자동화 절차와 함께 제공 omega되지만 congruence, 일반적으로 적용되지 않습니다, 이자벨 / HOL에서 하나의 명령으로 해결 될 수있는 많은 정리가 COQ를 더 명시 적으로 제공합니다.

물론 편의 시설에도 대가가 있습니다. 시스템이 자체적으로 많은 일을하기 때문에 Isabelle / HOL 자신의 증명을 제어하는 ​​것이 더 어렵다는 말을 들었습니다. 이 간단한 정리를 증명할 때 문제가 없지만 증명 자동화가 충분히 강력하지 않고 정리 증명 자에게 더 자세히 알립니다.

사용자 정의 증명 자동화 절차를 지원할 수있는 상황이 절차를 지원합니다. Coq는 자체 프로그래밍 언어 인 Ltac으로 내장 된 증명 작성 을 위해 전술 한 언어 와 함께 제공 됩니다. Ltac에는 몇 가지 설계 문제가있어 사용자는 상당히 복잡한 증명 자동화 절차를 가벼운 방식으로 인코딩 할 수 있습니다. 더 무거운 작업의 경우 Coq는 사용자가 Coq의 구현 언어 인 OCaml로 사용할 수도 있습니다. Isabelle / HOL은 Ltac과 같은 고급 자동화 언어가 사용자가 사용자 정의 증명 자동화 절차를 프로그래밍 할 수있는 유일한 방법은 사용하는 것입니다.

---

Isabelle / HOL의 "푸시 버튼"효능에 대한 한 가지는 Cantor의 고전적인 "대각 화"주장을 자동화 한 것 입니다 (이는 자연에서 그 힘 집합에 대한 예측이 의미합니다. 또는 더 일반적으로 파워 세트에 대한 모든 세트).

theorem Cantor: "∄f :: 'a ⇒ 'a set. ∀A. ∃x. A = f x"
proof
  assume "∃f :: 'a ⇒ 'a set. ∀A. ∃x. A = f x"
  then obtain f :: "'a ⇒ 'a set" where *: "∀A. ∃x. A = f x" ..
  let ?D = "{x. x ∉ f x}"
  from * obtain a where "?D = f a" by blast
  moreover have "a ∈ ?D ⟷ a ∉ f a" by blast
  ultimately show False by blast
qed

제가 방금 여러분에게 제시 한 것은 Cantor의 고전적 주장을 Isabelle / HOL로 번역 한 것입니다. 의심 할 여지가 없습니다. 이자벨 / HOL 은이 증명 에서도 인사이트를 자동화 할 수 있습니다 .

theorem "∄f :: 'a ⇒ 'a set. ∀A. ∃x. f x = A"
  by best

theorem "∄f :: 'a ⇒ 'a set. ∀A. ∃x. f x = A"
  by force

증명 시스템은 Cantor의 진술을 자동으로 증명할 수 있습니다. 연구원에게는 도움이되지만 양날의 검이라는 느낌이 있습니다. 내 정리가 더 정교 해지기 때문에 대각 화 주장처럼 복잡한 진정한 진술이 Isabelle / HOL 내부적으로 입증 될 수 있다는 것이 도움이 될 수 있습니다. 다른 한편으로, 컴퓨터의 자동화 가능한 발전에 의해 연구를 진행할수록 정리가 진실 인 이유 또는 원리에 대해 점점 더 적게 설명 할 수 있습니다. 컴퓨터 만이 그 이유를 알고 있습니다.

---

질문에서 "Isabelle / HOL"이 정확 해 지므로 Isabelle에서 사용하는 HOL 논리에 대해 이야기하겠습니다.이 논리는 Coq와 비교하는 데 가장 적합하다고 생각합니다. 나는 타입 시스템과 로직의 전문가는 아니지만 여기서 말하는 것이 적어도 대략적으로 옳다고 생각합니다. 이것은 또한 확실히 맛의 문제입니다 ;-) 내 대답은 주관적 일 수 있습니다.

가장 큰 차이점은 유형 시스템과 논리에 있습니다.

ML 제품군의 기능적 언어를 아는 사람 (그리고 SML을 아는 사람에게는 더욱)이 더 자연스러워지고 실용적인 접근 방식을 사용하여 문제를 해결하는 것이 강점이라고 말하고 싶습니다. 기초. 유형 시스템은 Hindley Milner의 시스템에 가깝고 기본적으로 종료됩니다 (사용자가 수정하지 않은 경우).

반면에 Coq는 더 엄격하고 직관적 인 논리를 사용합니다. 여러 순서를 가진 특수 유형 시스템을 가지고 있으며 처리하기 까다로울 수 있고 일부 상황에서 종료되지 않을 수있는 유형 종속성을 허용합니다. 또한 Isabelle에서는 직접적으로 불가능한 증명 (비교적 비효율적 일 수 있음)에서 프로그램을 추출 할 수 있습니다.

참고 URL : https://stackoverflow.com/questions/30152139/what-are-the-strengths-and-weaknesses-of-the-isabelle-proof-assistant-compared-t