2009-01-01から1年間の記事一覧

「ω-矛盾な真理理論について」

Outline 目的: 真理理論の「計算的」内容について考察を加える 題材: PAŁTr2 無制限な T-図式と全域的な真理述語を持つ 論理式の循環的な定義を許す 問題: PAŁTr2 は ω-矛盾である [R93][HPS00]。 疑問: 制限なしの真理述語を持っているという点で、PAŁT…

明日より

研究集会・科学哲学会(残念ながら、初日の午後早めに帰ります)・ワークショップのため、更新が遅れる可能性があります。ご了承ください。

寒い日。一日中、発表の準備。帰宅途中、地下鉄に乗ったら、梅田と間違え中津で降りてしまった。疲れているんだろうか。寒くなったせいかヘルペスの痕も傷む。 帰宅後、夕食は昨日のスープとスモークサーモンのオープンサンドイッチ。

引き続き寒い。今年始めて、厚めのコートを着て出勤する。 昼間の会議で、○○○○な知らせに、出席者一同驚愕する。まるで独ソ不可侵条約のニュースを聞いたポーランド国民みたいな気分、我らが組織の明日はどっちだ…。 プレゼン原稿を準備したり、SMT ツールを…

「ω-矛盾な真理理論について」

11月21日(土)に、科学哲学会大会で以下の発表をします。 嘘つきのパラドックスにより、古典論理上の公理的真理理論は部分的な真理述語 T のみを持つ。しかし、真理述語に関する制限は、真理述語の全域性だけではない。すなわち、十分な表現力を持つ真理理…

 "Specification check tool S3 and its mathematical model"

11月20日(金)に、TPP (Theorem Proving and Prover) meeting 2009 研究集会(websiteはこちら)において、 以上のタイトルで発表をします。

寒い日。朝は雨、夕方には止む。今年始めてセーターを着て出勤。研究所でSMTツールの続き。午後は非常勤先で授業、本日は矛盾律と矛盾許容論理について。Gの空手着の写真が一部に妙に受けていた。帰宅して夕食は回鍋肉丼。

急に寒くなる。出勤してSMTツール、うまく動かず悩む。他に色々、とっくに送ったはずのメールが、実は宛先の記入漏れのため、届いていなかったことを知って慌てる。帰宅して夕食、本日はキムチ焼き豚丼。食後は各種雑用、明日の授業準備や某書類関連。

昼に美容院に出かける。それ以外は一日某書類書き、やっと一区切り。夜にCが帰宅、夕食はお土産の焼き豚丼とシューマイ。

昼頃におき、一日中某書類書き。本日はCが東京のため、夕食はトマトソースパスタを作るが、間違えてパスタのゆで汁を規定量の三倍入れてしまった(あんなに入っているとは思わなかった)ため、水っぽくなってしまった。残念。

共同研究先と会議

午前は晴れ、夕方から雨。出勤して午前は雑用。午後は大阪市内で会議、ついに共同開発していたツールのα版リリース。ついでに5分プレゼンを行う。帰宅して、夕食はペンネ。

午前から会議二つ。午後は翌日のプレゼン準備。ほかにいろいろ打ち合わせ。 本日夜からCが東京なため、夜は同僚らと飲みに行く。軽く飲むはずが帰宅は24時。

朝は雨、昼から曇り(夕方、傘を忘れて帰る)。出勤して各種準備と雑用。帰宅後、夕食はトマトソースのペンネ。

曇り、湿度の高い日。夕方から降りだし、深夜には大雨となる。出勤して打ち合わせ、プレゼン内容について承認をもらう。午後は非常勤先の授業、証明の正規化の話。その後セミナー二つに出て帰宅、夕食はクリームシチューのマカロニ入れ。

暖かい日、昼には多少汗ばむ。本日は大阪で共同研究先と会議。夕方研究所に顔を出し、色々打ち合わせ。帰宅後、夕食は娼婦風スパゲティ。

一日某書類書き。夜になってCと外出、三宮に行き、「ボルカノ」でボロネーゼを食べる。

よく晴れた日。11時に起床、昼食はキャベツとアンチョビーのオイルパスタ。午後はずっと某書類書き、多少は書き慣れてきたか。夜になってCと外出、自由権で牡蠣フライを食べる。帰宅後は書類の続き。

よく晴れた日、気温は低め。出勤して検査機構について色々打ち合わせ、てんやわんやの挙げ句、もうちょっと時間をかけた方がいいという結論に(お騒がせしました)。他にも各種事務仕事が色々。 帰宅後、夕食はマグロ丼。

一昨日に比べれば暖かい。午前は共同研究先の企業と会議、プレゼンをする。地下鉄駅の近くのビアホールで昼食にビーフカツ定食を食べるが、なかなか。午後から研究所、会議後は型検査の時間短縮に血眼になる。その後帰宅して夕食、今日は焼き肉。

晴れているが肌寒い。出勤してコード書きと打ち合わせ。Agdaコードの「改良」をしたが、改良の結果遅くなったかもしれない。 帰宅して夕食、トマトスープにリゾーニを入れる。

外出もせず、部屋の掃除と書類整理の後、一日中某書類書き。昼食は昨日のシチューの残り、夕食はツナとブロッコリーのトマトソースパスタ。

「ザ・コールデスト・ウインター 朝鮮戦争」(上)(デイヴィッド・ハルバースタム)

朝鮮戦争でなぜアメリカは中国の参戦を予想できなかったのかを、マッカーサーを中心に描いたノンフィクション。ちまたでは「マッカーサー神話に終止符を打つ本」として流行っているようですが、たしかにマッカーサーのイメージが変わります。現代日本史に興…

リゾーニ

長さ0.5cmぐらいの小さなマカロニなんですが、シチューに入れると素晴らしい味です。 [rakuten:otokonodaidokoro:10001492:detail]

急に寒くなる。コートを着て出勤。 出所してSMTツールの勉強、コードを書いてみるが色々面倒。他に打ち合わせ各種。寒風の中帰宅、夕食はクリームシチュー(マカロニ入り)。

晴れた日。出勤して昨日の続き、徐々に全貌が明らかになって来た。他にメールを色々書く(が、深夜になって日付が間違っていることを指摘され、慌てる)。帰宅して夕食はスモークサーモンとホタテのトマトクリームパスタ。

今日も晴れる。出勤し、午前は各種打ち合わせ。午後は会議と打ち合わせ、28時間かかっていた検査が18秒で終了するようになったとの報告を受け、驚愕する。その後、SMT ツールの勉強。帰宅後、夕食はイカそうめん丼。

よく晴れた日。しかし気温は肌寒くなって来た。 本日は共同研究先と会議。一回研究所に顔を出してから共同研究先の会社へ。会議は色々面倒な話が出る。また研究所に寄ってから帰宅(帰りの阪急電車が、あたかもいつもより速いスピードで走っているかのように…

昼間は比較的暖かく、昼食にラーメンを食べいただけで汗だくになってしまった。しかし日が暮れるととたんに寒くなる。 午前中は研究所、明日のプレゼン内容について説明を行う。午後に非常勤先の大学に向かい、授業。本日はM君が出席していて、Belnap の uni…

曇り空。台風が太平洋上を通り過ぎたせいで、雨が降ったり、夜になって強風が吹いたりする。 一日中各種事務処理およびマニュアル書き。山積みになっていた宿題を一部片付けることができた。帰宅は21時半、夕食は鶏肉のすき焼き風。

曇り空、気温は低め。朝から引き続き書類整理、押し入れ奥から大学時代のノートやら何やらが出てくる。昼は砂肝のチャンプル、午後は某書類および非常勤授業の準備。夕方、Cと外出するも、自由軒が臨時休業だったため、JR駅の中華料理店で夕食。Tsutaya に寄…