theorem-proving

3열

1답변

Agda : 스택과 함께 설치할 때 std-lib를 찾을 수 없습니다.

Agda 파일을 컴파일하려고하는데 표준 라이브러리를 찾는 데 문제가 있습니다. 문서 here을 보았습니다. 나는 그것을 설치하는 스택을 사용했습니다 : > which agda /home/joey/.local/bin/agda 을 그리고 난 내 AGDA 디렉토리를 환경 변수를 설정 한 : 올바른 파일로 채워집니다 > echo $AGDA_DIR /home

functional-programming agda dependent-type theorem-proving agda-mode 2017-10-27

---

0열

2답변

Isabelle에 "Power.thy"의 추가 버전이 있습니까?

Isabelle에서 함수를 정의했습니다. f:'a -> nat 여기서 'a은 monoid (즉, 그룹, 반올림, 반지, 정수 도메인, 필드 등)를 확장하는 일부 대수 구조입니다. 다른 구성에서는 내 유형 'a에 대해이 기능의 출력을 "계수"로 사용하고 싶습니다. 즉, x:'a과 n:nat이라면, 내가 n·x = x + x + ... + x이라는 Isabel

isabelle theorem-proving 2017-10-31

---

0열

1답변

무한 반전 루프 Coq

에 붙어 있습니다. 아래에 표시된 접미어과 같은 유도 관계가 있습니다. 나는 관련 theorem suffix_app을 증명하려고 노력하고 있습니다. 내 일반적인 생각은 xs가 ys와 같거나 몇 가지 일련의 요소임을 나타내는 접미사 xs ys이라는 사실을 사용하는 것입니다. cons ' Require Import Coq.Lists.List. Import L

coq theorem-proving 2017-04-26

---

2열

1답변

Z3에서 완전히 평가 된 결과?

Z3은 종종 중간 기능 묶음으로 정의 된 백 모델을 제공합니다. 그래서 (define-const myArray (Array Bool Int) (_ as-array f)) (define-fun f (x Bool) Int (f!10 (k!26 x))) ... 그리고 예를 들어, 그것은 (내 잘못된 구문을 용서) 다음을 참조하는 것이 일반적이다. 라이브러리

z3 smt theorem-proving formal-verification 2017-11-13

---

0열

3답변

z3의 계승을 포함하여 수학적 진술을 증명할 수 있습니까? (더 놀라움을 그 증거를 제시하지 않더라도

나는 다음 울프 람 알파를 증명하는 것이 참으로 true임을 식별 할 수있을 것으로 보인다 노력하지 있어요 및 최대 값을 결정할 수 없습니다 가) : declare(n, integer) $ assume(n > 0) $ is(equals(2^n - n - 1 - sum(binomial(n,k), k, 2, n), 0)); => unknown 지금 나

z3 maxima theorem-proving wolframalpha 2017-01-23

---

-1열

1답변

FOL 모델의 일관성 검사

1 차 로직으로 모델을 개발 중입니다. 일관성이 있음을 증명하고 싶습니다. 가능한가? 이 작업을 수행하는 데 사용할 수있는 무료 도구가 있습니까? 또는 Godel 정리로 인해 불가능합니다. 감사합니다.

logic theorem-proving model-checking theorem 2017-03-17

---

3열

1답변

Coq는 선택 모나드가 응용 프로그램과 모나드임을 증명합니다.

저는 coq에 처음 접했고 지금까지 손으로 증명할 수있는 것들만 증명할 수있었습니다. 그래서 셀렉션 모나드를 만나서 그것을 haskell에서 구현하기로 결정했을 때, 좋은 운동이 될 것이라고 생각했지만 붙어있었습니다. 누군가가 coq에서 선택 모나드가 응용 프로그램이자 모나드라는 증거를 보여줄 수 있습니까? 다음은 functor의 haskell 구현입니다.

functor coq applicative theorem-proving 2017-02-09

---

1열

1답변

COQ 아래와 같이 나는 다음과 같은 정리에 대한 해결책을 받았다 유도 가설

를 생성하지 : Require Import Coq.Lists.List. Import ListNotations. Inductive suffix {X : Type} : list X -> list X -> Prop := | suffix_end : forall xs, suffix xs xs | suffix_step : foral

coq proof theorem-proving 2017-05-21

---

2열

1답변

Z3 : 대수 선형 표현

매트릭스와 벡터가 포함 된 표현식의 특성을 증명하고 싶습니다 (크기는 고정적이지만 크기는 고정적 일 수 있음). 나는 식의 결과가 대각 행렬이나 삼각 행렬이, 또는 명확한 긍정적임을 입증 할 예를 들어 ... 내가 인코딩 잘 알려진 속성을 원하는이를 위해 및 ||x + y|| <= ||x|| + ||y|| (A * B) * C = A * (B * C)

z3 smt formal-languages theorem-proving 2017-11-07

---

1열

1답변

AGDA는 <a href="https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Base.agda" rel="nofollow noreferrer">the standard library</a>에서 <code>ℕ</code> 및 <code>_≟_</code>를 사용하여 목표 유형

의 발현을 감소 만들기, 나는 open import Data.Nat open import Relation.Binary.PropositionalEquality open import Relation.Nullary foo : ℕ -> ℕ -> ℕ foo x y with x ≟ y foo x .x | yes refl = x foo x y | no co

agda dependent-type theorem-proving 2017-05-15

---