母関数を用いた節集合のリネーミング法
スポンサーリンク
概要
- 論文の詳細を見る
節集合は導出原理に基づく証明法(導出法)の入力とされる論理式の集合である. 導出をより効率的に行うため, ホーン節集合がしばしば用いられる. 節集合を論理的に等価な形でホーン節集合へと変換するリネーミングを系統的に行う方法はこれまでにいくつか提案されている. 本研究では計数母関数を用いることにより, 与えられた節を任意の個数の正リテラルを持つ節へと変換するすべてのリネーミングが母関数の係数から同時にすべて求められることを示す. 言い換えれば, 母関数から節のリネーミング後の正リテラル数の状態に対応したリネーミングの分類を得ることが可能となるこの分類から, 対象とする節を0または1個の正リテラルを持つ節に変換するリネーミングだけを抽出することによって節のホーン化条件が得られる. さらに節集合の各要素に対する節のホーン化条件の共通部分を抽出することにより, 節集合のホーン化条件すなわち節集合をホーン節集合に変換するすべてのリネーミングが得られる. 本方法は, このようなリネーミングが一括して求まるという点で他の方法と大きく異なっている. さらに計数母関数の高次係数を用いることにより, 今まで系統的な方法の確立されていなかったホーン節集合よりも条件のゆるやかな節集合を, ホーン節を求めるためのリネーミング法の理論的拡張として求める手順が得られることを示す. そして, その具体例として節集合の分割問題への応用についても言及する.
- 一般社団法人情報処理学会の論文
- 1986-11-15