kt3k 日記

スポンサーサイト

上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

立ち話

DJ、FLASHer、考究仲間の(qre)さんと2時間ぐらい立ち話した。

今日は考究が途中で中断して、みんなでゾロゾロ歩いて、
コレを聞きに行った。ACL2という証明器で、quicksort がソートできている
事を証明するデモなんかを眺めた。Ruben Gamboa さんという人が実装したという、
ACL2(r)というACL2の拡張で、解析学の定理を証明した話の紹介が興味深かった。

考究では、論理以外の公理を持たない理論の中で、existential な論理式が定理である
ためには、その論理式の matrix のインスタンス達を or でつないだもののうちで、
quasi-toutology になるものが存在することが必要十分であるということ(棒読み)を証明した。
(consistency theorem とか、prenex operation の基本的性質が証明済みなので、そこまで
難しくない。)

shoenfield


コメント


管理者にだけ表示を許可する
 

 

トラックバック

上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。