論理プログラミングのソースを表示

'''【ろんりぷろぐらみんぐ (logic programming)】'''

=== 概要 ===
知識や森羅万象の因果関係を論理記号と非論理記号を使って形式的に記述したものは論理式と呼ばれる. この中で一階述語論理式と呼ばれ, "それを成り立つようにするには, いくつかのそれぞれ異なる条件が満たされればよい" ことを記述する論理式集合の処理を対象として, ある論理式が成り立つかどうかの検証過程を計算過程とみなしたコンピュータプログラムを論理プログラム, このような計算原理に基づくプログラム法を論理プログラミングという.

=== 詳説 ===
　論理とは「推理の仕方, 論証の筋道」を意味し, 論理学とは「正しい認識を得るための規範となるべき思惟の法則及び形式を研究する学問一般」をいう. その中で [[記号論理学]] (symbolic logic) とは「論理の対象となる思考の終局的要素とその基本的な関係を数学の記号に類するもので表現し, 論理的操作を数学の演算に類する操作で行う論理学」であって, 論理計算, 数学的論理学と大体同義であるとされる [1]. 従って, 記号論理は[[論理推論]] (logical reasoning) 分野に属し, その研究はわれわれの興味の対象要素(思考の終局的要素)と対象間の論理的関係を操作し, 論証の道筋を検証し, 正しい認識を得ることに関する方法論の探究を意味する. 

　このことはわれわれが計算機を使って計算を行う, 問題を解く, あるいは, 対象を計算機で制御するなどの諸計算行為と多くの類似点をもつ. しかし, こうした (数値的) 計算行為には, 使用するプログラム言語のもつ諸規則 (文法など) や計算順序などを勘案しつつアルゴリズムを構築しプログラミングを行うことが要求されるため, こうした方法では, 知識としての論理の対象となる思考の終局的要素とその基本的な関係を, 直接表現し利用することは, 従来, 困難であった. 近年, 知識工学 (knowledge engineering) と呼称され, 知識を計算行為の対象, すなわち知識処理を対象とする分野が展開されてきた. これは知識を約束に従って記号化し, いわゆる知識ベースとして計算機の中にこれを蓄え, これらを利用しつつ, 対象問題 (ここでは命題) を解こうとする研究分野であって, 記号論理学がその理論的基礎を成す. 

　さて, 知識工学では, 理論・実用の両面にわたって特に多くの研究やシステム開発が, 一階述語論理(first-order predicate logic)を利用して行われている. 一階述語論理に基づく場合, 知識は記号列で表現され, 知識の操作は, 短い列から長い列を生成する構文的規則(syntax), 与えられた記号列を解釈する意味論的規則 (semantics), 構文的規則に基づく推論規則 (rule of inference) および系全体に関する公理 (axiom) に基づいて行われる. これは例えて言えば, アルファベットから単語が構成され, 単語群から文節が構成され文節群から文が構成される仕組である. 文法に相当するものとして構文的規則があり, 文字列としての単語や文節, 文章の意味解釈に相当する操作が意味論的規則に則って用意される. 

　記号論理的に見ると一階述語論理の記号列は, 論理記号 (結合子, 限定記号など) と非論理記号 (定数, 変数, 述語, 関数) からなり, 非論理記号に固有の意味を与えたとき, その解釈は一意的に決まる. このことを, 一階言語を定めたという. またここで言う述語 (predicate) は, その引き数である定数や変数の状態や性状 (つまり, ～である；～する, など) を記述する. 述語の解釈としての論理的意味付けには, ブール代数では0か1, 二値論理では真か偽, ファジィ論理では数値的真理値や言語的(linguistic)真理値を割り当てる. 変数や定数, さらに, 変数や定数をすべての引数に代入した関数を項 (term) と呼ぶ. <math>n\, </math>変数の述語の各引数に項を代入した論理式を原子論理式 (atomic formula) といい, これらを論理記号で結合したものも論理式という. さらに, 論理式同士を論理記号で結合したものも論理式という. 代表的論理式同士の関係を意味づけしたものがいわゆる真理値表 (truth table) を構成する. 

　論理式 <math>\phi\, </math> を真とするある解釈と項への値割り当てが存在するならば, この論理式は充足可能 (satisfiable) であるという. さらに論理式の集合<math>\Gamma\, </math> を充足する任意の解釈と割り当てがある論理式 <math>\phi\, </math> を充足するとき, この論理式 <math>\phi\, </math> は論理式集合 <math>\Gamma\, </math> の論理的帰結と呼ばれる. ゲーデルの完全性定理 (completeness theorem) によれば, ある論理式 <math>\phi\, </math> が論理式集合 <math>\Gamma\, </math> の論理的帰結であるならば, 論理式集合 <math>\Gamma\, </math> からその論理式 <math>\phi\, </math> を導く有限の長さの記号列を生成できる. これは論理式集合から有限回のステップで機械的に論理的帰結を導くことができるアルゴリズムの存在を言明している. ここから一階述語論理の推論規則として唯一定義されるモーダス・ポーネスが提示される. すなわち, "二つの論理式 <math>\phi\, </math> と <math>\psi\, </math> があり, 論理式 <math>\phi\, </math> が論理式集合 <math>\Gamma\, </math> の論理的帰結かつ「<math>\phi\, </math> ならば <math>\psi \, </math>」も <math>\Gamma\, </math> の論理的帰結ならば, <math>\psi\, </math> は <math>\Gamma\, </math> の論理的帰結である. "これは連続値を扱う[[ファジィ推論]] (fuzzyinference) [3] の場合にも前提, 条件および近似的帰結として成り立つ推論規則である. 

　次に, [[論理プログラミング]] (logic programming) において重要な「証明」の概念を述べる. 論理式の列 <math>\phi_\iota (\iota=1, 2, . . n)\, </math> が存在し, 全ての <math>\phi_\iota\, </math> が公理か, 論理式集合 <math>\Gamma\, </math> の元か, または列のそれ以前に位置する他の論理式からモーダ・ポーネスによって導かれたか, のいずれかが成り立つとする. この時, 論理式の列 <math>\phi_\iota\, </math> は論理式 <math>\phi_n\, </math> の証明と呼ばれ, 論理式 <math>\phi_n\, </math> は論理式集合 <math>\Gamma\, </math> から証明可能である, といわれる. 

　以上の議論の結果として形式的知識表現としての論理式はプログラムに, その推論過程としての証明は計算に対応することが理解できる. 現実的視点から一階述語論理のある制限されたクラスのみを対象としてプログラミング環境を実現したものを論理プログラミングという. そのような制限されたクラスとして[[ホーン節]]がある. 一般に論理プログラミングでは, 与えられた論理式の否定(<math>\phi_1\, </math>)からトップダウン的またはボトムアップ的に[[導出原理]]を利用して演繹的に空節(<math>\phi_n\, </math>)を導くという証明の手続きが利用される. このようにして <math>\phi_1\, </math> の充足不可能性を証明することによって, 元の論理式が真であることを証明するのである. 論理プログラミングにおける代表的プログラム言語がPROLOGであり, わが国の第５世代コンピュータ計画をはじめとして知識工学, 人工知能分野に多くの影響を与えている. 

　論理プログラミングの直接的応用としてはパズル, 定理証明などが知られているが, その実際的応用はいわゆる各種[[エキスパートシステム]] (expert system) の構築にある. エキスパートシステムでは, 事実や専門家の知識を論理式, 特にホーン節形式で表現して知識ベースとして蓄え, 知識ベースの内容を論理式集合 <math>\Gamma\, </math> として, 与えられた問題 (論理式) に対して論理的帰結を自動的に得る手続きを論理プログラミングが受け持つ [4]. 論理プログラミングによる証明の解釈そのものが, エキスパートシステムにおいては人間への自動説明機能となる. このようなエキスパートシステムの持つ宿命的課題は必要十分な知識をいかに獲得するかである. [[知識獲得]] (knowledge acquisition) の方法として人手による方法ばかりではなく自律的学習機能を導入する研究もなされている. さらに, 実用上の問題として蓄えた知識の上の推論の非単調性 (non-monotonicity) の問題, すなわち新しく入力された知識が以前の知識と矛盾するような結果を引き起こす現象がしばしば起こることが指摘されている. これに対する有力な方法は未だに確立されていないが, 実際にはこのような場合でも[[非単調推論]] (non-monotonic reasoning) と呼ばれる方法が利用される. 

　論理プログラミングが人の論理的知識を蓄積し利用しようとするものであるのに対して, [[定性推論]] (qualitative inference) は物理法則に基づいた因果関係を基本として, 対象とする系の動的挙動を定性的に推論し, 理解しようとする [5]. 通常は微分方程式で表わされ解析され理解されるところの物理現象を, 素朴に理解しようとするものと考えることができるが, 計算機の数値計算能力に依存する部分がある. 定性推論は物理現象に対して素直に抱く疑問「なぜ?」, 「こうなったらどうなる?」に答えるのに有効な推論方式と考えられる. 

　ここで取り上げた伝統的な記号論理的推論に基づく論理プログラミング, 曖昧さを導入したファジィ推論, あるいは知識の直接利用を狙ったエキスパートシステム, さらには, 物理現象の動的振る舞いを対象とする定性推論を有機的に結合することにより, 真に有効な人工知能が実現されることを期待したい. 



----
'''参考文献'''

[1] 新村出編, 『広辞苑(第5版)』, 岩波書店, 1998. 

[2] 森下真一, 『知識と推論』, 情報数学講座10, 共立出版, 1997. 

[3] 水本雅晴, 『ファジィ理論とその応用』, サイエンス社, 1988. 

[4] 安部憲広, 滝寛和, 『エキスパート・システム入門』, 共立出版, 1987. 

[5] 溝口文雄, 古川康一, 安西祐一郎, 『定性推論』, 知識情報処理シリーズ別巻1, 共立出版, 1989.


[[category:近似・知能・感覚的手法|ろんりぷろぐらみんぐ]]