ひとり勉強会 RSSフィード

1900-01-05

| ■を含むブックマーク

ここ「ひとり勉強会」は、会と言いつつひとりで勉強した記録を残してます。

Coq の解説記事を書くために勉強しています。

(1)
forall A B: Prop, (A->B) -> A -> B.
CoqIDEのつかいかた。forall と -> の証明。
(2)
forall A B: Prop, ~(A ∨ B) -> (~A ∧ ~B).
and と or と not の証明。Inductive な命題。
(3)
forall n: nat, exists m, (n=2*m ∨ n=2*m+1).
自然数やリスト。再帰的 Inductive なデータ。= と 帰納法 と exists の証明。omega, ring, field による自動証明。標準ライブラリの使い方。
(4)
解説テキストリンク集
(番外編)
VSTTE 2012 Software Verification Competition

つづく...

トラックバック - http://d.hatena.ne.jp/hzkr/19000105

CC0
To the extent possible under law, the person who associated CC0 with this work has waived all copyright and related or neighboring rights to this work.