導出
出典: フリー百科事典『ウィキペディア(Wikipedia)』
導出(どうしゅつ)とは、数理論理学における一つの演繹方法である。定理自動証明において一般的に使われる手法。
導出おいて二つの節より新しい節を導きだす演繹ルールを導出原理といい、一方の節に含まれる命題と、他方の節に含まれるその命題の否定をのぞき、その他の命題の論理和をとることで、新しい節を得ることをいう。式で表せば、命題aiが命題biの否定である時、
と書ける。
導出は与えられた節の集合に、導出原理を当てはめ得られる新しい節をもとの節の集合に加える事を繰り返す事で行われる。命題論理、また述語論理いずれにも使う事が出来る。命題論理における導出は完全である。