標準形 (Normal Forms)

標準形は、論理式を一定の構文パターンへ変換した形である。CNFやDNFのように、比較・自動推論・ソルバー入力の目的に応じて選ぶ。

仕組みと確認

対象の論理体系と意味保存の規則を定め、元の式と変換後の式を真理値表またはモデルで比較する。式の大きさ、補助変数、可読性、ソルバー性能を評価する。

限界と注意点

標準形は一種類ではなく、変換によって式が指数的に膨らむこともある。目的を明示し、等価性を保つ変換と充足可能性だけを保つ変換を区別する。