仮定の導入と解消

仮定の導入と解消は、条件付きの証明や背理法で一時的な前提を置き、一定の結論を得た後にその前提のスコープを閉じる操作である。

仕組みと確認

仮定に識別子を付け、どの規則で解消されたかを証明木へ残す。コードのスコープ、トランザクション、テストの前提も同じように開始と終了を明示すると追跡しやすい。

限界と注意点

仮定を解消し忘れると、外部では成立しない結論を導く。前提の漏れ、例外経路、ロールバック条件をレビューする。