有限モデル性
『コンピュータサイエンスにおける様相論理』.icon p.23
次の2条件は同じことを主張しており、この性質をLの有限モデル性(finite model property)と呼ぶ
(A) 任意のL論理式$ \varphiに対して次が成り立つ. $ \varphiがL充足可能ならば, $ \varphiはある有限Lモデルで充足される
(B)任意のL論理式$ \varphiに対して次が成り立つ. $ \varphiがL恒真でないならば, ある有限Lモデルとその中のある状態で$ \varphiが偽になる
ここでのLとは以下のいずれかのこと
K
CTL
様相ミュー計算
PDL
このいずれの体系でも上記の性質が成り立つ
『コンピュータサイエンスにおける様相論理』.icon p.23