isabelle

1熱度

2回答

這個問題related to my last question。在對我的問題的回答中，有一條陳述，「通常不是使用存儲庫版本爲您的工作」的說法。那麼我的問題是：使用mecurial存儲庫的開發版本最重要的缺點是什麼？我還說了resons爲什麼我決定使用開發版本：我的經驗是Isabelle2013-2簡直是完全無法使用。我得到非常沮喪，這不是好玩。它經常慢，並且太撞擊。隨着開發版的打字感

2熱度

2回答

Isabelle：在不同的機器上運行大錘，然後在我的正常PC上運行Isabelle/jEdit運行

我正在與我的labtop上的Isabelle/jEdit合作。我的筆記本電腦有4個核心，即4個CPU。但我在隔壁房間裏也有一臺服務器電腦。該服務器有20多個CPU。通常我平行運行sledgehammer和try，因爲有時試驗結果會給出大錘本身失效的大錘結果（請參閱my other question on this）。所以我想有很多可以並行運行的進程。但是，我無法在服務器上使用或運行Isab

17熱度

5回答

認證程序的定義

我看到了幾個不同的研究小組，至少有一本書談論了使用Coq設計認證程序。關於認證程序的定義是什麼，有共識嗎？從我所知道的情況來看，它的真正含義是該程序被證明是完整的並且類型正確。現在，程序的類型可能是一些非常奇特的東西，比如列表中有一個非空的證明，所有元素大於等於5，等等。然而，最終，這是一個認證的程序，只是Coq顯示的程序是完整的和類型安全的，所有有趣的問題都歸結爲最終類型中包含的內容？編輯1

2熱度

2回答

伊莎貝爾：調整引理，以形成所需的`rule`方法

我定義稱爲step_g感應關係。這裏的推理規則之一： G_No_Op: "∀j ∈ the (T i). ¬ (eval_bool p (the (γ ⇩t⇩s j))) ⟹ step_g a i T (γ, (Barrier, p)) (Some γ)" 我想援引證明這個規則，所以我鍵入 apply (rule step_g.G_No_Op) 但規則不能應用，因爲它的

0熱度

1回答

如何在感應證明中顯式綁定變量？

我有一個數據類型和在它的感應謂詞（實際上是一些過渡系統的一小步語義）： datatype dtype = E | A | B dtype inductive dsem :: "dtype ⇒ dtype ⇒ bool" where "dsem A E" | "dsem (B E) E" | "dsem d d' ⟹ dsem (B d) (B d')" 和也由殼體區分計算的函

4熱度

1回答

顏色代碼在Isabelle/jEdit中的含義是什麼？

Isabelle/jEdit中的顏色代碼是什麼意思？我在Isabelle/jEdit manual找不到他們的描述。它寫的唯一的事情是證明者反饋工作通過顏色，包裝盒，波浪下劃線，超支鏈接，彈出窗口，圖標，點擊輸出 - 全部基於由伊莎貝爾在後臺產生的語義標記。顏色用作校樣腳本背景和滾動條旁邊的豎條上。你能指出一些文檔或在這裏解釋嗎？

1熱度

1回答

在伊莎貝爾

加載預編譯堆圖像繼how-to-use-persistent-heap-images-to-make-loading-of-theories-faster-in-isabelle和另一個建議，我創建了標稱伊莎貝爾的圖像： isabelle build -v -b -d . Nominal2 堆圖像在〜/ .isabelle創建： .isabelle/Isabelle2013-2/heaps/p

1熱度

1回答

內部語法註釋中的雙引號

"字符放在Isabelle內部語法的雙引號片段中的註釋內部時，其行爲並不像我所期望的那樣。澄清：在下面的函數定義中，我期望the "at" sign被解析爲註釋。實際上，Isabelle將該註釋中的第一個"字符與該行開頭的"相匹配，從而導致語法錯誤。 fun reverse where "reverse [] = []" | "reverse (x#xs) = reverse xs @

0熱度

1回答

Isabelle：爲什麼我在試騎大錘時跑完全不同的結果

當我在大錘的結果中只看到時，的輸出經常給出大錘在跑步時的各種結果大錘直接給出零（！）結果。現在我知道了，大錘的設計目標不是確定性， as stated by Lawrence Paulson。然而，這個看似隨機的結果不理解爲什麼都有點不僅對我，而且還讓學生在幫助阻止項目對於初學者，。一個可能性是總是運行大錘並嘗試平行。我並不需要一個確切的答案，但沒有任何人有一個線索，爲什麼結果可

2熱度

2回答

如何提取Isabelle中的實例化變量？

我試圖證明在伊莎貝爾如下： theorem map_fold: "∃h b. (map f xs) = foldr h xs b" apply (induction xs) apply auto done 我怎樣才能獲得的h和b實例化的價值？