命題論理の決定可能性

命題論理は、有限個の命題変数と真理関数的な結合子で構成された式について、恒真性・充足可能性・論理的帰結をアルゴリズムで判定できる。真理値表は単純な決定手続きだが、変数数に対して行数が指数的に増える。

仕組みと確認

式の構文を確認し、恒真性ならすべての割り当て、充足可能性なら少なくとも一つの割り当てを調べる。大きな式ではSATソルバーやCNF変換を使い、モデル・反例・タイムアウトを結果として分けて保存する。

ソフトウェア工学との接続

機能フラグ、アクセス条件、テスト生成、構成探索を命題制約として検査できる。決定可能であることは、入力規模に対して十分速いことや、制約の翻訳が正しいことを保証しない。

限界と注意点

真理値表は意味論を明示するが、現実の状態・時間・副作用を表さない。制約の範囲、変数の意味、未定義値の扱い、ソルバーのバージョンを仕様とともに管理する。