タブローの構築規則

タブローの構築は、論理式が充足可能か、または妥当かを、式を分岐・展開した木で調べる方法である。枝が閉じれば矛盾、開いた枝が残ればモデルの候補を表す。

仕組みと確認

結合子・量化子ごとの展開規則、枝の閉鎖条件、同じ式の再展開防止を定める。開いた枝から具体的な割り当てや反例モデルを取り出し、入力仕様と照合する。

限界と注意点

展開が停止しない量化や無限モデルでは、手続きの完全性・停止性・探索制限を別に扱う。タイムアウトを反証や充足不能と取り違えない。