theorem-proving

1열

1답변

Agda에서 유형이 비어 있음을 증명하는 것

나는 agda에서 2 * 3! = 5를 증명하려고 노력하고있다. 이것을하기 위해 서명 2 * 3 ≡ 5 → ⊥를 갖는 함수를 정의 할 것입니다. 내가 1*3≡3 : 1 * 3 ≡ 3 1*3≡3 = (succ base) znn 및 3+3≡5 : 3 + 3 ≡ 5 → ⊥ 3+3≡5 (sns (sns (sns()))) 그러나 입증 data _*_≡_

theorem-proving agda 2013-08-09

---

1열

1답변

이사벨 행렬 산술 : 다른 표기법을 사용한 라이브러리의 det_linear_row_setsum

최근에 이사벨 이론 정리자를 사용하기 시작했습니다. 다른 보조 정리를 증명하기 위해 HOL 라이브러리에서 찾을 수있는 보조 정리 "det_linear_row_setsum"과 다른 표기법을 사용하고 싶습니다. 더 구체적으로, 나는 "χ i"대신에 "χ i j 표기법"을 사용하고자합니다. 나는 얼마 동안 동등한 표현을 공식화하려고 노력했지만 아직 이해할 수 없

matrix isabelle theorem-proving 2013-06-25

---

3열

3답변

자동 정리 증명

나는 이것을 증명할 수있는 자동 정리 증명 시스템을 찾고 있습니다. 악어가 사람을 데려갔습니다. 남자는 악어에게 아이를 먹지 말라고했다. 그러나 악어는 말했다 : 나는 네가 나에게 말할 것이면, 나는 그와 함께 무엇을 할 것인가? 이 같은 그의 외모에 분석 솔루션 : X - 악어는 아이에게 Y를 먹을 것이다 - 남자의 대답 : 악어가 아이 먹을 것이다 ~

prolog theorem-proving 2013-06-25

---

3열

1답변

Z3은 수작업으로 작성된 데이터 유형으로 대소 문자를 구분하지 않습니다

boolean은 SM32이고 내 기능은 boolean_and입니다. 내 추측은입니다 및 교환 법칙이 성립입니다 : (declare-sort boolean) (declare-const sk_x boolean) (declare-const sk_y boolean) (declare-const boolean_false boolean) (declare-cons

z3 theorem-proving 2013-03-18

---

0열

1답변

C++ 프로그램에서 z3 API 사용에 대한 도움이 필요합니다.

C++ 프로그램에서 z3 API를 사용하고 싶습니다. 내가 포함 할 헤더 파일을 궁금 방법 Z3 기능 등 내가 Z3의 소스 코드와이 파일을 실행하기 위해 오는 example.cpp 파일을보고이 포함 된 프로그램을 실행하기 위해, 나는에 make examples을 실행했다 내부적으로 명령 내가 어떤 프로그램을 만들 경우 지금 g++ -o cpp_example

compilation g++ z3 theorem-proving 2013-07-07

---

0열

1답변

C++에 대한 z3 정리 프로버 API에 대해 어디서 배울 수 있습니까?

C++ 용 z3 API를 배우고 C++ 프로그램에서 사용하는 방법을 배우고 싶습니다. 나는 튜토리얼을 찾으려고했지만 할 수 없었다. 어디에서 배울 수 있습니까? 튜토리얼 또는 무엇인가? 감사합니다. .

c++ logic z3 verification theorem-proving 2013-07-07

---

2열

1답변

Coq의 모듈 서명 외부에서 표기법을 어떻게 보이게합니까?

몇 가지 표기법을 정의한 Coq에서 모듈 서명을 정의했습니다. 그러나 서명 밖에서 이러한 표기법을 사용하려고하면 Coq가 실패합니다. 아래 코드는 간단한 코드입니다. 어떤 도움을 주시면 감사하겠습니다. Module Type Field_Axioms. Delimit Scope Field_scope with F. Open Scope Field

coq theorem-proving 2013-03-30

---

2열

2답변

Coq : 유도 성 목록의 문제

저는 Coq을 처음 접했지만 약간의 노력으로 다양한 유도 표제를 증명할 수있었습니다. 그러나 나는 다음과 같은 유도 정의를 사용하는 모든 운동에 박히 : 내가 가진 먼은 다음 보조 정리로했다 Inductive In (A:Type) (y:A) : list A -> Prop := | InHead : forall xs:list A, In y (cons

coq theorem-proving induction 2013-06-08

---

1열

1답변

레코드 유형이 주어진 클래스에 속해 있음을 확인하십시오.

레코드 유형을 으로하고 적절한 "하위 그래프"관계를 정의했습니다. 서브 그래프 관계와 함께 그래프 집합이 순서를 형성한다는 것을 보여주고 싶습니다. 즉, ord 클래스의 인스턴스입니다. 그러나 나는 그것을 작동시킬 수 없다. 내가 오류 얻을 theory John imports Main begin typedecl node record gra

isabelle theorem-proving 2013-07-31

---

2열

2답변

Coq을 사용한 사례 별 증명

사례별로 증명을 사용하여 증명하고자하는 간단한 정리가 있습니다. 예가 아래에 나와 있습니다. Goal forall a b : Set, a = b \/ a <> b. Proof intros a b. ... 어떻게 해결할 수 있습니까? 정확히 어떻게 평등 (True 또는 False)의 가능한 두 가지 값을 사용하여 사례별로 증명을 정

logic coq theorem-proving 2013-03-05

---