「ホーン節」の版間の差分
ナビゲーションに移動
検索に移動
(新しいページ: '【ほーんせつ (Horn clause)】 リテラル(命題そのものか, またはその否定)が選言で結合された論理式を節と呼び, 正のリテラル(否定の...') |
|||
| 1行目: | 1行目: | ||
| − | 【ほーんせつ (Horn clause)】 | + | '''【ほーんせつ (Horn clause)】''' |
リテラル(命題そのものか, またはその否定)が選言で結合された論理式を節と呼び, 正のリテラル(否定のついていない命題)を高々1つ含む節のことをホーン節と呼ぶ. Prolog などの多くの論理型プログラムはホーン節の集合として構成される. 任意の論理式は等価な節集合に変換できるが, 特にホーン節のみからなる節集合に対しての定理証明手続きは, 線形導出などの効率的な手続きが存在することが知られている. | リテラル(命題そのものか, またはその否定)が選言で結合された論理式を節と呼び, 正のリテラル(否定のついていない命題)を高々1つ含む節のことをホーン節と呼ぶ. Prolog などの多くの論理型プログラムはホーン節の集合として構成される. 任意の論理式は等価な節集合に変換できるが, 特にホーン節のみからなる節集合に対しての定理証明手続きは, 線形導出などの効率的な手続きが存在することが知られている. | ||
2007年7月17日 (火) 13:37時点における版
【ほーんせつ (Horn clause)】
リテラル(命題そのものか, またはその否定)が選言で結合された論理式を節と呼び, 正のリテラル(否定のついていない命題)を高々1つ含む節のことをホーン節と呼ぶ. Prolog などの多くの論理型プログラムはホーン節の集合として構成される. 任意の論理式は等価な節集合に変換できるが, 特にホーン節のみからなる節集合に対しての定理証明手続きは, 線形導出などの効率的な手続きが存在することが知られている.