"Conservative extensions, uniform interpolants, and modules"(Frank Wolter)
JAIST先端レクチャー・シリーズ"From Pure Logic to Ontology Engineering"の第二回目。
背景説明
医療用のカルテのオンライン・システム等の場合、病気を単に分類するだけでなく、病気などの分類（「概念」）を階層化しておいた方が便利なことが多い。例えば、「盲腸」で入院した患者は、同時に内科に入院した患者でもある。従って、「盲腸の患者⊆内科の患者」との概念の階層構造があれば、「内科の患者」で検索した際に、盲腸の患者も検索リストに登場する。このような階層化された医療用概念・用語集をつくることは、技術的に難しいことは何もなく、すでに実用化され（ほぼrelational databaseとどっこいどっこいである）、ヨーロッパの医療情報ネットワークで使用されている。
しかし、単なる階層化された用語集では情報量が足りず、物足りないことが多い。なによりも、たくさんの述語の階層構造を扱うため、一カ所定義を間違えると、システム全体がとんでもないことになりかねない。従って、システムのデザインが非常に困難である。
というわけで、最近、公理系によって医療用語を定義しようという動きが世界中（西ヨーロッパ・アメリカ･オーストラリア）で進んでいる。公理系ならば単なる階層構造よりもデザインが楽である（もちろん無矛盾性を確かめる必要があるが）。例えば、9カ国共同開発の SNOMED CT (the Systematized Nomenclature of Medicine, Clinical Terms)、40万以上の医療用語の定義を与えるためのシステムである。これは、ほぼ同数の40万（！）の公理系からなる一階述語論理上の公理系であり、医療用語は述語として定義されている。公理は、例えば
∀x（Appendicitis(x)→Disease(x)&∃(Associated_Morphology(x,y)&Inflammation(y))）
みたいな、いかにもという感じで記述される。また、患者がその医療用語に当てはまるかどうかは、標準的なタルスキ意味論の充足関係を使用して定義される。
さて、概念の階層構造は、この公理系から定理として導出される。その点で「公理から定理を自動的に導出する」操作が非常に重要となる。もちろん、定理の自動導出は非常に難しい分野だが、このシステムでは、言語の表現力を厳しく制限することで、導出の際の計算量の上限を制限している。
ちなみに、他にも色々な試みがあり、例えばFMEでは、導出された階層構造の例をweb上で確かめることが出来る。
注意： 記述論理 (description logic) について
ただし、「一階述語論理」といっても、技術的都合により、通常の学校で習う（変数を持ち、量化子を持つ）一階述語論理ではなく、そのバージョンである「記述論理 (description logic)」 を使用する*1。
（後で追加します）
今回の講演
システムに新しく情報や公理を追加した場合、最初に問題となるのは、その拡大が保存拡大*2となっているかどうかである*3。
保存拡大性は、数学であればrelative consistency、ソフトウェアの仕様書であれば使用の改訂（refinement）やモジュール構造化された仕様書の他のモジュールとの整合性の問題として考えられるだろう。ただし、記述論理の体系ALC・EL共に、モデル拡大性の検査は非常に決定が難しい（coNExpTime-complete）。
というわけで、モデル拡大性以外のもっと計算しやすい拡大性を定義する（例えば「もとのモデルへのbisimulationが存在する」と定義する」とか）。
他に、そのバージョンとして、replacement ALC-保存性なるものを定義する。これは、理論 T1 の拡大 T1uT2がreplacement ALC-extensionであるとは、任意のTに関してT1uT2uTのモデル上である概念の包含関係が成立するなら、同じ関係がT1uTのモデルでも成立する、と言うものである。この関係は、クレイグの補間定理・ロビンソンのjoint consistency、演繹定理とかなり同じ形の定義であり、同じような成果が期待できるだろう。
さて、授業終了後、Og先生が「以前補間定理について話をしたとき『何の役に立つのか』と聞かれてがっかりした記憶があるのだが、これからは『こんなに有用なのに知らないんですか』と逆襲してやれる」と喜んでいました。
