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

俗に上流段階とも呼ばれる、要求定義段階の仕様書は、普通自然言語で書いてありますが、そのため曖昧性・多義性に満ちており、同一の語が別の意味で使われるなんてざらだと言われています。そのため、曖昧な表現を皆が自分勝手なやり方で解釈するのですが、…

イギリスから研究所を訪問しに来た大学院生二人のミニ・セミナーに出る。プログラムとユーザのインタラクションの意味論を、ゲーム意味論で与え、線型論理で公理化しようという話。線型論理は良い表示的意味論があり、それがインタラクションを線型論理の枠…

本日、緊急に会議が招集され、所員全員が出席するよう指示された。議題は新型インフルエンザ、拡大した場合の行動指針について上司が演説。緊急でない出張は避けること、 各自が家で缶詰などの保存食・水を確保しておくことなどの指示が出る。また、発生した…

オントロジーの階層的構造の表示自体は、最近GUIなツールがいくつも出ている。ヨーロッパではOWLのグラフィカルな表示ツールがあるし、日本でも大阪大学の「法造」などがある（こちら参照）。しかし、論理体系によるアプローチでは、そもそも階層的構造は導…

JAIST先端レクチャー・シリーズ"From Pure Logic to Ontology Engineering"の第三回目。 今回は、異なるバージョン同士の理論の間の違いをどう効率的に表示するか、という話。のサイズが10万の時、通常のやり方だと10分かかるところ、モデルを作る順番を逆に…

JAIST先端レクチャー・シリーズ"From Pure Logic to Ontology Engineering"の第二回目。 背景説明 医療用のカルテのオンライン・システム等の場合、病気を単に分類するだけでなく、病気などの分類（「概念」）を階層化しておいた方が便利なことが多い。例え…

業務論文です。pdf版はこちら。要旨は以下の通り。 In the extended abstract, our on-going research project Verification Tool and Unified Specifications for Embedded Software is explained. In the project, we are developing an upper-process sup…

というタイトルで、某氏作成の述語論理の実装と、私作成のホーア論理のインチキ実装を紹介しました。皆様、ご静聴ありがとうございます。 質疑応答 Q.なんか、Agdaで証明を書いていると、手で証明を書いた後、Agdaで清書しているだけのように感じるのですが…

勤務先の研究所は情報科学関連であり、形式技法関連の参考図書をたくさん買っています。この本、新着書コーナーで形式技法による検証関連の場所に並んでいたのですが、よく見てみると…「文学研究における形式技法」。それに著者がバフチーンじゃないか。共著…

研究チーム5人の共著論文。論文は こちら、スライドはこちら。 組込みソフトの仕様書の形式化と、入力を簡単にするツールの開発計画について。発表の出来はそれなり、また色々ご意見をいただく。ありがとうございます。

明日、共同研究先でプレゼンがあるので、最近は準備にかかり切りだ。 それで昨日、上級研究員のOさんから「君はこれまで、どれくらい（学会・研究集会での）発表をしているの？」と聞かれた。「国際学会も入れて、1年に4〜5回です」と答えると、「うん、決定…

いつのまにか、私は様相述語論理の専門家ということになってしまった。内容は面白い。っていうか Kripke frame が役に立たない。だから証明論的な体系をコンピューター上の定理証明支援系(Agda)に実装することになる。・・・これって、「意味論」と呼んでい…