変換手順
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2022/08/01 10:08 UTC 版)
古典的な一階述語論理の論理式を節標準形に変換する手順は以下の通りである。 論理式を否定標準形にする。 スコーレム化 -- 外から内に向かって、存在量化変項をスコーレム定数に置き換え、全称量化変項をスコーレム関数に置き換えていく。具体的には次のような置換を行う。 を とする。ここで は新規導入。 を とする。ここで は新規導入。 全称量化子を削除する。 論理式を連言標準形にする。 を に置換。それぞれの論理積は という形式になり、これは と等価である。m=0 かつ n=1 なら、Prolog における事実となる。 m>0 かつ n=1 なら、Prolog における規則となる。 m>0 かつ n=0 なら、Prolog におけるクエリとなる。 最後に各論理積 を に置換する。 n = 1 の場合をホーン節と呼び、これは万能チューリング機械と同等の計算能力を有する。 完全な等価でなくとも、同等(equisatisfiable)な節標準形で十分であることが多い。その場合、指数関数的増大を防ぐには、Tseitin transformation を使用し、定義(definitions)を導入して論理式の一部を改名(rename)すればよい。
※この「変換手順」の解説は、「節標準形」の解説の一部です。
「変換手順」を含む「節標準形」の記事については、「節標準形」の概要を参照ください。
- 変換手順のページへのリンク