出典: フリー百科事典『ウィキペディア(Wikipedia)』
|
|
1行目: |
1行目: |
|
'''導出'''(どうしゅつ)とは、[[数理論理学]]における一つの[[演繹]]方法である。[[定理自動証明]]において一般的に使われる手法。 |
|
'''導出'''(どうしゅつ)とは、[[数理論理学]]における一つの[[演繹]]方法である。[[定理自動証明]]において一般的に使われる手法。 |
|
|
|
|
|
導出おいて二つの[[節]]より新しい節を導きだす演繹ルールを導出原理といい、一方の節に含まれる命題と、他方の節に含まれるその命題の否定をのぞき、その他の命題の[[論理和]]をとることで、新しい節を得ることをいう。式で表せば、命題<math>a_i</math>が命題<math>b_i</math>の否定である時、 |
|
導出おいて二つの[[節]]より新しい節を導きだす演繹ルールを導出原理といい、一方の節に含まれる命題と、他方の節に含まれるその命題の否定をのぞき、その他の命題の[[論理和]]をとることで、新しい節を得ることをいう。式で表せば、命題<math>a_i</math>が命題<math>b_j</math>の否定である時、 |
|
|
|
|
|
<math>\frac{ |
|
<math>\frac{ |
2008年5月29日 (木) 03:35時点における版
導出(どうしゅつ)とは、数理論理学における一つの演繹方法である。定理自動証明において一般的に使われる手法。
導出おいて二つの節より新しい節を導きだす演繹ルールを導出原理といい、一方の節に含まれる命題と、他方の節に含まれるその命題の否定をのぞき、その他の命題の論理和をとることで、新しい節を得ることをいう。式で表せば、命題が命題の否定である時、
と書ける。
導出は与えられた節の集合に、導出原理を当てはめ得られる新しい節をもとの節の集合に加える事を繰り返す事で行われる。命題論理、また述語論理いずれにも使う事が出来る。命題論理における導出は完全である。
プログラミング言語のPrologの基礎となる理論である。
関連項目