この記事はTheorem Prover Advent Calendarの22日めの担当記事です．今年の僕の持ちネタの一つですが，ipc_bot というTwitter botを作りました．https://twitter.com/ipc_botこのbotは直観主義命題論理の命題を投げると解いてくれるbotです． 仕組み 証明を…

情報オリンピックの予選に参加しました．(予選は誰でも参加できます)次のような制約で解くことにしていました． 1番は Wolf RPGエディター 2番は TeX 3番は Scratch 4番は Excel 5番は APL 6番は Bash 結局1と4を解きました． 1番 Wolf RPGエディターで解き…

来年やる人が同じ失敗をしないために色々書いておきます途中で「です・ます」調でなくなっているのは息切れです。めんどくさいので直していません 参加記 端的にまとめます 場所：今年は埼玉の準山奥でやりました。2009年に僕が生徒として参加したときと同じ…

2013/08/26 - 08/30の間、夏季セミナーというのにチューターとして参加していました。以下はその記録として参照できる各種媒体へのリンクです。参考：去年のリンク集 募集案内 実施の概要 参加者のtwitterリスト 発表会の様子(Togetter) その1(AI) その2(グ…

チーム名 qnighy メンバー qnighy (計1名) 記録 08/06 ICFPCの登録期限が目前に迫っていたのでEasyChairに登録する。 08/07 EasyChairに登録するだけではだめで、ICFPCという名前のカンファレンスに論文を登録したことにしないといけないことを知り、論文の…

CMS (Contest Management System) の最近の動向について書いてみようかなと思います企画2週目 DBモデルの修整とインポーターのダイエット lerks(Luca) がDBモデルの細かい問題点をチェックし、修整しています。例えば、アクセス元の許可リストとしてIPアドレ…

CMS (Contest Management System) の最近の動向について書いてみようかなと思います クロアチアと日本での採用 CMSが次の大会で採用されました。 クロアチアの3段階ある国内大会 日本の国内大会のうち、代表選抜合宿 クロアチアでの採用を報告したメールによ…

CoqのtacticをOCamlで書いてみたので、同じようなことをしたい人のためにメモ。なお私はOCamlについてはそれほど詳しくないので、そこの正確性については注意が必要。 同じ事をしているtacticがないか探す 同じようなことを考えている人は必ずいるはず。とい…