出典: フリー百科事典『ウィキペディア(Wikipedia)』
|
|
17行目: |
17行目: |
|
* [[スコーレム標準形]] |
|
* [[スコーレム標準形]] |
|
|
|
|
|
[[Category:数学基礎論|とうしゆつ]]
|
|
{{DEFAULTSORT:とうしゆつ}} |
|
[[Category:形式手法|とうしゆつ]] |
|
[[Category:推論規則]] |
|
[[Category:数学に関する記事|とうしゆつ]] |
|
[[Category:数学基礎論]] |
|
|
[[Category:形式手法]] |
|
|
[[Category:数学に関する記事]] |
|
|
|
|
|
[[de:Resolution (Logik)]] |
|
[[de:Resolution (Logik)]] |
2008年10月22日 (水) 04:12時点における版
導出(どうしゅつ)とは、数理論理学における一つの演繹方法である。定理自動証明において一般的に使われる手法。
導出おいて二つの節より新しい節を導きだす演繹ルールを導出原理といい、一方の節に含まれる命題と、他方の節に含まれるその命題の否定をのぞき、その他の命題の論理和をとることで、新しい節を得ることをいう。式で表せば、命題が命題の否定である時、
と書ける。
導出は与えられた節の集合に、導出原理を当てはめ得られる新しい節をもとの節の集合に加える事を繰り返す事で行われる。命題論理、また述語論理いずれにも使う事が出来る。命題論理における導出は完全である。
プログラミング言語のPrologの基礎となる理論である。
関連項目