400年の難問、「ケプラー予想の証明」やっと100%終わる2014.08.13 22:0020,202 satomi コペルニクスが提唱した地動説を、天体運行法則で不動のものにした偉人ヨハネス・ケプラー。 そのケプラーが1611年に提唱した「球は、八百屋に山盛りのオレンジみたいにピラミッド型に並べると一番沢山入る」という説が、400年の歳月を経て、100%正しかったことがコンピュータの力で証明されました。 この立体最密充填の解答は、誰でも直感的になんとなく正しいことがわかります。けれども証明するとなると超厄介で、世界歴代の天才がいくら頭脳を結集しても証明できなくて、ずっと「定理」ではなく「ケプラー予想」と呼ばれ続けてきた難題中の難題です(参考)。 証明したのは、米ピッツバーグ大学のトマス・ヘールズ教授です。もともと氏が1998年に発表し、「フェルマーの最終定理以来の難問が解けた!」と世界中
セミナー 形式手法に関するセミナーを開催しています. 詳細につきましてはセミナーのページをご覧ください. SyncStitch: A Model Checker based on the Process Algebra CSP SyncStitch is a model checker based on the process algebra CSP (Communicating Sequential Processes). By using SyncStitch, you can check six types of properties of the system you are developping: Deadlocks Divergences (also known as livelocks) Refinement relation on traces semantics (sa
この本は Introduction to Programming in ATS の日本語訳です。 日本語訳の維持管理は JATS-UG - Japan ATS User Group が行なっています。 翻訳に参加するには ATS2公式マニュアルの日本語訳 を参照してください。 プログラミング言語としての ATS は豊かな構文と機能を両立しています。 この本では ATS の中心となる機能を読者に解説します。 それらは基本的な関数型プログラミング、単純な型、(再帰的に定義された) データ型、多相型、依存型、線形型、定理証明、定理証明によるプログラミング (PwTP)、そしてテンプレートを使ったプログラミングなどです。 一般的なプログラミングに馴染みのある読者を仮定してませんが、この本は相当のプログラミング経験のない読者には少し難しいかもしれません。 All rights are reserve
With the help of computational proof assistants, formal verification could become the new standard for rigor in mathematics. From the point of view of the foundations of mathematics, one of the most significant advances in mathematical logic around the turn of the 20th century was the realization that ordinary mathematical arguments can be represented in formal axiomatic systems in such a way thei
This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation. I'm following an unusual philosophy in this book, so it may be of interest even to long-time Coq users. At the same time, I hope that it provides an easier introduction for newcomers, since s
すべての Microsoft 製品 Global Microsoft 365 Teams Copilot Windows Surface Xbox セール 法人向け サポート ソフトウェア Windows アプリ AI OneDrive Outlook Skype OneNote Microsoft Teams PC とデバイス Xbox を購入する アクセサリ VR & 複合現実 エンタメ Xbox Game Pass Ultimate Xbox Live Gold Xbox とゲーム PC ゲーム Windows ゲーム 映画とテレビ番組 法人向け Microsoft Cloud Microsoft Security Azure Dynamics 365 一般法人向け Microsoft 365 Microsoft Industry Microsoft Power Platform W
Feit-Thompson true Feit-Thompson theorem has been totally checked in Coq Thursday 20 September 2012, 18:16. We received following mail from Georges Gonthier (see below). It concludes the proof in Coq of the Feit-Thompson theorem. This theorem, also named the Odd Order Theorem, is the first main result in the classification of finite groups. This work was achieved by the team formed by addressees o
The locally nameless representation with cofinite quantification is a pratical technique for representing binders in a formal settings. The locally nameless representation avoids the need for alpha-conversion and the need for shifting de Bruijn indices. The cofinite quantification is used to obtain strong induction principles. This approach has been successfully applied to formalize many type syst
This is a quick page I've thrown together for my Coq library formalizing basic category theory. The development follows Steve Awodey's book on category theory; the files are named after chapters and subchapters of that book for easy reference. Getting It The gitweb is here. You might also want to look at the README Design Decisions One of the difficulties with putting together a formalization of c
We are interested in the formal verification of low-level software. For this purpose, we have developed in the Coq proof assistant formalizations of Separation logic (as presented in the survey by John C. Reynolds). We have applied these formalizations to several use-cases, including: the verification of the heap manager of the Topsy operating system (paper) the verification of arithmetic function
This document discusses type classes in Coq. It begins by introducing polymorphism and monads. It then defines the Monad type class in Coq, with return, bind, and other laws. Instances are given for the identity, maybe, list, and cont monads. The MonadPlus type class is also defined, with instances for maybe and list.Read less
継続計算に対する仮想機械の導出 定理証明系Coqを使った各種継続計算の性質の証明 対称 λ 計算 shift/resetを含む部分評価器の実装 MinCamlコンパイラ,Caml Lightにおけるshift/resetの実装 証明木(ほか)の可視化 お茶大情報科学科の時間割自動作成 『四則演算インタプリタを作ろう!』 四則演算インタープリタをつくりましょう 末尾呼び出し(tail call)と継続渡し形式(Continuation Passing Style) lexer(字句解析器)と parser(構文解析器)の作成 (サンプルコード) 局所変数の導入 関数(closure)の追加 大域脱出(exit)の追加 再帰関数の追加 FelleisenのCオペレータ リストの追加 Promptの導入 control/prompt から shift/reset への拡張 対称 λ 計算 Coq
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く