Loading article…
論理学、特に証明論において、与えられた論理体系に対する証明手続きとは、（証明可能な）命題の証明を何らかの証明計算体系で生成するための体系的な方法のことである。
証明計算にはいくつかの種類がある。最も一般的なのは、自然演繹、シーケント計算（ゲンツェン型システムなど）、ヒルベルトシステム、そして意味論的タブローまたはツリーである。特定の証明手順は特定の証明計算を対象とするが、多くの場合、他の証明スタイルで証明を生成するように再定式化することができる。
論理体系における証明手続きは、証明可能な各命題に対して証明を生成する場合に完全である。論理体系の定理は通常、再帰的に列挙可能であり、これは完全ではあるものの、通常は非常に非効率的な証明手続きの存在を意味する。しかし、証明手続きは、合理的に効率的である場合にのみ価値がある。
証明不可能な命題に直面した場合、完全な証明手続きは、その証明不可能性を検出して通知することに成功する場合がある。しかし、一般的には、証明可能性は半決定可能な性質に過ぎないため、これは不可能であり、手続きは分岐する（終了しない）。