数理解析研究所講究録
927 巻 1995 年 56-65

56

命題様相論理の充足可能性問題の計算量について
名古屋工業大学大学院工学研究科

1(Matsuoka, Satoshi)

松岡聡

序様相論理の充足可能性問題の計算量の研究は. Ladner [6] により始められた。 [6]では S4 の充足可能性問題の計算量 (以下では論理と計算量のクラスが結びつけられる場
合は “充足可能性問題の計算量” という言葉は省略される) が PSPACE-complete, S5 が-complete であることが証明されている。
本稿では、 Ladner の手法を改良した Halpern と Moses の手法 [3] を用いて S42 がPSPACE-complete であることを証明する。 また、 様相論理が-complete であるた$\mathrm{R}.\mathrm{E}$$\mathrm{N}\mathrm{P}$$\mathrm{N}\mathrm{P}$めの十分条件を提示する。
本稿は次のように構成される。 2 節では計算量のクラスの定義を行う。 3 節では様相論理
が NP-complete であるための十分条件を提示する。 4 節では S4.2 が PSPACE-complete
であることを示す。

2

計算量のクラス
チューリングマシンの定義や計算量のクラスの定義は基本的には [8] にしたがう。

Definition 1 (決定性) チューリングマシンは 4 つ組 $M=(K, \Sigma, \delta, S)$ である。 ここでは状態の有限集合であり, は $s\in K$ であり、初期状態と呼ばれる。 は記号の有限集合で$I_{\acute{1}^{r}}$$s$$\Sigma$

ある。そしてを満たしている。また、 はそれぞれブランク、初期記号とよばれ“る記号をふくんでいる。 さらに\mbox{\boldmath $\delta$} はから (’, “no” )$K\cap\Sigma=\emptyset$$\mathrm{u},$$\Sigma$$K\cross\Sigma$$\triangleright$$K\mathrm{U}\{$への関数となっていなければならない。そして、 は\mbox{\boldmath $\delta$}(q,つ $D=arrow$ をみたしていなければならない。
$\delta$$\triangleright$$\}$$\mathrm{y}\mathrm{e}\mathrm{s}’$$\mathrm{x}\Sigma\cross\{arrow, arrow,-\}$). $=(p, q, D)$ ならば$\rho=\triangleright$“yes” と “no” は informal には、 それぞれ受理状態、拒否状態を表す。同じように$arrow,$か$arrow$

それに $-$ はそれぞれチューリングマシンのヘッドの左方向、右方向それに–時停止の動作を表している。
に対して\mbox{\boldmath $\delta$}(q, ) $=(p, q, D)$ ならば$\delta$$\triangleright$$\rho=\triangleright$

かつ $D=arrow$ であることを、満たすという条

件はチューリングマシンの動作は、入力はかならずで始まるの要素とし、チューリ
ングマシンのヘッドは最初にをみていて、状態は初期状態 で始められると定義されるためで、 をこのように定義する目的はの左側へはチューリングマシンのヘッドがいかないような定義したいということである。
$\Sigma^{*}$$\triangleright$, $s$$\triangleright$$\delta$$\triangleright$

57

で、ヘッドが移動した場所に記号が存在していない場合は次の出力の 3 番目がをみているという状態で遷によるチューリングマシンの状態の遷移ではヘッドはの移がおこる。テープの記号の並びの右端に が継ぎ足されるということになる。チューリ
ングマシンの動作の定義は次のように時点表示 (configuration) という概念を用いて定義さまた、$arrow$$\delta$$\mathrm{u}$$\delta$$\mathrm{u}$れる。

Definition 2 configuration は 3 つ組 $(q, w, u)$ である$\circ$

ここで$q\in(K\cup\{" \mathrm{y}\mathrm{e}\mathrm{s}’’, " \mathrm{n}\mathrm{o}^{;\prime}\})$

か

である。

つ $w,$ $u\in\Sigma^{*}$

Definition 3 configuration $(q, w, u)$ が $(q’, w”, u)$ へ one-step 遷移 $((q, w, u)arrow M(q’, w”, u)$であらわされる) されるとは次の条件を満すことをいう:
を $w$ の最後の記号とし、 $\delta(q, \sigma)=(p, \rho, D)$ であると仮定する。 このとき $q’=p$ でなけ
ればならない。 $D$ は, のいずれかであるが、 $D=arrow$ ならば、 $w’$ は、 に–番最後$\sigma$$arrow,$ $arrow$$\mathrm{w}$–はに最初の記号の削除をほどこしで、で置き換えをほどこした
$w’$
は
で、
は
から最後の記号 を取り去ったたである。 $D=arrow$ ならば、での最後の記号の\mbox{\boldmath $\sigma$} をである。 $D=–$ ならば $w’$ はの最初に を付け加えたで、 $u’=u$ である。
置き換えた

記号の

$\sigma$を$u’$$\in\Sigma^{*}$$u$$\rho$$w$$\in\Sigma^{*}$$w$$\in\Sigma^{*}$$u$$\in\Sigma^{*}$$\sigma$$\rho$$u’$$\rho$$\in\Sigma^{*}$

決定性チュ $-$ リングマシンでは、 configuration $(q, w, u)$ からの one-step の遷移は存在しないか必ず 1 つだけ存在するかである。
configuration の k-step の遷移\rightarrow や、 reflexive transitive closure

も通常のように定義さ$M^{*}arrow$れる。

Definition 4(非決定性) チューリングマシンは 4 つ組 $N=(I\{’, \Sigma, \delta, S)$ である。 $N=$
についての条件は\mbox{\boldmath $\delta$} が関数ではなく-} という関係であることを除き、 あとは決定性チューリングマシンと同様である。
$\delta\subseteq(K\cross\Sigma)\cross(K\mathrm{U}\{" \mathrm{y}\mathrm{e}\mathrm{S}^{;;}, " \mathrm{n}\mathrm{o}^{\prime;}\})\mathrm{x}\Sigma\cross \mathrm{t}arrow$$(K, \Sigma, \delta, S)$$,$$arrow,$

非決定性チューリングマシンの場合にも configuration が決定性の場合と同様に定義される。違いは configuration $(q, w, u)$ からの one-step 遷移は存在するか複数個存在するということである。 しかし無限個存在するわけではなくある定数 $k\geq 0$ が存在し、任意のconfiguration $(q, w, u)$ からの one-step 遷移の個数は で押えられることに注意。
$k$-tape 決定性チューリングマシンは決定性チューリングマシンの をに変更することで定義される。 -tape 非決定性チュー)
リングマシンも同様に定義される。 この場合の configuration は $(q, w_{1}, u_{1}, \ldots, w_{k}, uk)$ (こかつ) と変更される
こで$\delta$$k$$\{" \mathrm{y}\mathrm{e}\mathrm{s}’’, " \mathrm{n}\mathrm{o}’’\}$$k$$\cross(\Sigma\cross\{arrow, arrow, -\})^{k}$$q\in I\mathrm{s}^{\nearrow}\mathrm{U}\{" \mathrm{y}\mathrm{e}\mathrm{S}^{\prime\prime(}, ‘ \mathrm{n}\mathrm{o}\}\prime\prime$$\delta:K\cross\Sigma^{k}arrow(K\cup$$w_{1},$ $u_{1},$$\ldots,$$w_{k},$$u_{k}\in\Sigma^{*}$$0$への関数とする。チューリングマシン $M$ が operating within
Definition 5 を から
time $f(n)$ であるとは、任意の input に対して $M$ が f(国) 以内に停止すること、すな
かのかから $f(n)$ ステップ以内に
わち、 configuration
configuration への遷移が存澆垢複海箸髪い A$f$$\mathrm{N}$$\mathrm{N}$$x$$(S, X, \in \mathrm{i})$$(” \mathrm{y}\mathrm{e}\mathrm{s}’’, w, u)$$(” \mathrm{n}\mathrm{o}’’, w, u)$58

であることは、 ある $k>1$ があり operating within time $f(n)$ である-tape 決定性チューリングマシン $M$ が存在し $M$ がを受理することと定義する。

$L\in \mathrm{T}\mathrm{I}\mathrm{M}\mathrm{E}(f(n))$$k$$L\subseteq\Sigma^{*}$

も非決定性チューリングマシンに変更して同じように定義される。

$L\in \mathrm{N}\mathrm{T}\mathrm{I}\mathrm{M}\mathrm{E}(f(n))$

Definition 6 チューリングマシン $M$ とこれに対する入力 に対して
(ただし $H\ni\{$ “) であるとする。このとき space required by $M$ on input は\Sigma j
であると定義される。
をからへの関数とすると、チュ $-$ リングマシン $M$ が operating withing space bound$f(n)$ であるとは任意の入力に対し、 space required by $M$ on input が $f(|X|)$ で押え$x$$(s, \triangleright, X, \triangleright, \mathit{6}, \ldots, \triangleright, \epsilon \mathrm{i})M^{*}arrow(H, w_{\iota}, u_{1}, w_{2}, u_{2}, \ldots, wk, u_{k})$$=1|w_{i}u_{i}|$$x$$\mathrm{N}$$\mathrm{y}\mathrm{e}\mathrm{s}^{\prime\prime(},‘ \mathrm{n}\mathrm{o}’’\}$$f$$\mathrm{N}$

$x$

$x$

られることをいう。
であることは、 ある $k>1$ があり operating within space bound $f(n)$-tape 決定性チューリングマシン $M$ が存在し $M$ がを受理することと定$L\in \mathrm{S}\mathrm{P}\mathrm{A}\mathrm{c}\mathrm{E}(f(n))$

である

$k$

$L\subseteq\Sigma^{*}$義する。
$L\in \mathrm{N}\mathrm{S}\mathrm{P}\mathrm{A}\mathrm{C}\mathrm{E}(f(n))$

も非決定性チューリングマシンに変更して同じように定義される。

よく知られている計算量のクラスは次のように定義される。

Definition 7$\mathrm{P}^{\mathrm{d}}\equiv^{\mathrm{e}\mathrm{f}}\bigcup_{0j>}\mathrm{T}\mathrm{I}\mathrm{M}\mathrm{E}(n^{j})$NP$\mathrm{d}\mathrm{e}\mathrm{f}\equiv\bigcup_{j>0}\mathrm{N}\mathrm{T}\mathrm{I}\mathrm{M}\mathrm{E}(n^{j})$PSPACENPSPACE
EXP$\mathrm{d}\mathrm{e}\mathrm{f}\equiv\bigcup_{j>0}\mathrm{s}\mathrm{P}\mathrm{A}\mathrm{C}\mathrm{E}(n^{j})$$\mathrm{d}\mathrm{e}\mathrm{f}\equiv\bigcup_{j>0}\mathrm{N}\mathrm{S}\mathrm{P}\mathrm{A}\mathrm{C}\mathrm{E}(n^{j})$$\mathrm{d}\mathrm{e}\mathrm{f}\equiv\bigcup_{j>0}\mathrm{T}\mathrm{I}\mathrm{M}\mathrm{E}(2n^{j})$また NP-complete や PSPACE-complete などの計算量のクラスは次のように定義される。

Definition 8 言語から
(p-time) reducible であるとは、あるへの関数で決定性チューリングマシンで TIME
for some で computable なものが存在し、すべての入力 に対して
$L_{1}$

が$L_{2}$

へ$\Sigma^{*}$$R$$(n^{i})$$\Sigma^{*}$

$i$

$x$

$x\in L_{1}$iff $R(x)\in L_{2}$ .

が成立することをいう。
を計算量のクラス, $L\in C$ としたとき が -complete であるとは、任意の $L’\in C$ がへ (p-time) reducible であることである。

$C$

$L$

$C$

$L$

59

3

NP-completeness であるための十分条件

様相論理の基本的な用語は [2] にしたがう。
を可算個の命題変数集まり、 $Fma(\Phi)$ を, ロを用いて通常のように から生成されを構成するの部分論理式の集まりとする。 $|A|$ でる論理式とする。 $Sf(A)$ を論理式の要素) をあらわす。
際に使用された記号の数 (記号は, (, ),$\Phi$$\perp,$$\Phi$$arrow$$A$$A$$\Phi\cup\{\perp,$

Proposition 1 論理式
証明

$A$

$A$

$arrow$$\square \}$の部分論理式の個数を $||Sf(A)||$ であらわすと $||Sf(A)||\leq|A|$の構成に関する帰納法による。口クリプキフレームは通常のように空でない集合 $M$ と $M$ 上の 2 項関係 $R$ の対 $(M, R)$ である。 S4 や S5 などのよく知られている命題様相論理は $R$ に関してある性質 ( $R$ が transitiveであるとか reflexive であるとか) が成り立つクリプキフレームのクラスに関して健全かつ完全になることはよく知られている。 さらに、 丘 ltration method を用いて、 $M$ を有限集合に制限したクリプキフレームのクラスに関して健全かつ完全になることを示すことができることもよく知られている。 ffltration method を用いれば、 よく知られた様相論理 (S4個以下の可能が充足可能かどうか調べるのにや S5 など) では、与えられた論理式
世界の個数をもつクリプキフレームについてのみの充足可能性を調べればよいことがわか$2^{|A|}$$A$る。

の充足可能性を $R$ がある first order formula で記述され、 $M$ が $p(|A|)$ 個以下 ( はある多項式) であるようなクリプキフレームのクラスに関する充足可能性に還元できるような論理は NP に属すことである。 (normal な) 様相論理
ここで示すことは、与えられた論理式

$A$

$p$

が古典論理の保守的拡大になっていることと古典論理の充足可能性問題が-complete に属すことがわかる。
であることから NP に属する (normal な) 様相論理が$\mathrm{N}\mathrm{P}-Complete$$\mathrm{N}\mathrm{P}$$M$の可能世界の個数を $||M||$ であらわすことにする。

Proposition 2 任意のに対して、が存在し、任意の論理式
に対してあるのみをもつ first order で特徴づ$||M||\leq|A|^{c}$ である $(M, R)$ が述語として 2 項述語 $R,$をもつかどうかという問題は TIME $(|A|^{C’})$ に属す。
けられる性質
$c$

$A$

$c’$

$=$

$\phi$$P_{\phi}$の構成に関する帰納法による。
証明
原子論理式の場合は $xRy$ か $x=y$ の形であるが、 すべての $x,$ $y\in M$ について $xRy$ や
回 $xRy$ や $x=y$ が成り立つかど$x=y$ が成り立つかどうか調べるためにはせいぜいうかの判定をすればよいので $c’:=2c$ として問題が TIME $(|A|^{C’})$ に属すことがわかる。
$\phi$$|A|^{2\mathrm{c}}$$\phi$

が$\neg\psi,$ $\psi_{1}\wedge\psi_{2},$$\phi$

が$\forall x.\psi$などの場合は帰納法の仮定を用いれば明らか。
が成り立つかどうかのが成り立つかどうかの判定がそのまま$\psi_{1}\psi_{2},$ $\psi_{1}arrow\psi_{2}$の場合は$\psi$$\forall x.\psi$

判定となる。
がの場合は. ということは $\exists x\in M$ . ということで、 $||M||\leq|A|^{c}$ が成り立ってが成り立つかどうかという問題は\psi が成り立つかどうかという問題と同じいるのでクラスに属すことがわかる。口$\phi$$\exists x.\psi$$\exists x.\psi$$\exists x$

60$(M, R)$ が与えられたときから上の付値 $V$ はへの関数である。 $V$ が与えられたとき $M$ の要素と論理式の間の 2 項関係
は通常のように定義される。 $(M, R, |=)$のことをクリプキモデルという。
$2^{M}$$\Phi$$(\mathrm{M},\mathrm{R})$$\vdash-$Proposition 3 ある論理式$(M, R, V)\vdash-_{a}A$$A$と $(M, R, \vdash-)$ が与えられたときが成り立つような $a\in M$ があるかどうかという問題は TIME $(||M||^{3}\cdot|A|)$

に属する。
証明

$(M, R, V)$ から論理式 $A$ の部分論理式と任意の $M$ の可能世界との 2 項関係$\models$

をTIME $(||M||^{2}\cdot|A|)$ で判定できれば命題が証明できることは明らか。
$B\in Sf(A)$ と $s\in M$ があたえられたときであるかどうかを TIME $(||M||^{2}\cdot|B|)$ で判定できることを論理式の複雑さに関する帰納法で証明する。 $B:=$ 口 C の場合のみが問$\vdash-_{s}B$題となる。 $sRt$ が成り立つ$\mathcal{O}((||M||^{2}\cdot|C|)\mathrm{X}||M||^{2})$$t$について $|=_{t}C$ を調べればよいわけだが、 これはかかるわけでなく、 $\mathcal{O}((||M||^{2}\cdot|C|)+||M||^{2})$ で判定できることに注意。 $|C|+1=|B|$ なのでTIME $(||M||^{2}\cdot|B|)$ に属す。口$\vdash-_{s}B$が成り立つかどうかという問題は.

Theorem 1normal modal logicが次の条件をみたすならば、
NP-complete である : ある $c>0$ が存在して、$L$$\psi_{L}\neg A$

証明

実際に

$\Leftrightarrow$$\Leftrightarrow$$L$の充足可能性問題はある first-order formula で特徴づけられる
クリプキモデルのクラス $F$ に属する$||M||\leq|A|^{c}$ である structure $(M, R, V)$があり
ある $a\in M$ で $(M, R, V)|=_{a}A$ が成り立つ。

の右の条件が成り立つかどうかを判定するための非決定性多項式時間限定チューリングマシンを構或してみればよい。
まず個以下の可能世界をもつクリプキフレームを非決定的に列挙する。
個以下の可能世界をもつクリプキフレームの個数はせいぜい個以下でこれは$|A|^{c}$$|A|^{c}$$2^{|A|^{3\cdot c}}$$|A|^{C}\cdot 2^{|A}|^{C}\cdot|A|^{C}$

で押さえられるので、多項式時間で非決定的に列挙することは可能である。
列挙されたクリプキフレームの–つを $(M, R)$ とする。論理式の $(M, R)$ におけるとり$A$

うる可能な付値の個数はせいぜい 2IIM 旧阿 (A)I 個であるが、 $||M||\leq|A|^{c}$ かつ$|Sf(A)|\leq|A|$よりこれは$2^{|A|^{c+1}}$

で押さえられるので、$A$と $(M, R)$ についての可能な付値を列挙することは多項式時間で非決定的に可能である。
と $(M, R)$ についての列挙された付値をとする。 $(M, R, V)$ はに出現しない命題
変数に関する付値を適当に決めておくことでクリプキモデルとみなせる。 が与えられたを特徴づける first order formula の性質を満たすかどうかの判定は $||M||\leq|A|^{c}$ より命
題 2 より多項式時間で判定できる。そして同じように が $(M, R, V)$ で充足可能かどうか判定することも命題 3 より多項式時間で判定できる。
したがって以上のことからの右の条件が成り立つかどうかを判定するための非決定性
多項式時間限定チューリングマシンが構成できることが示された。 口
$A$

$V$

$A$

$R$

$\mathcal{F}$$A$$\Leftrightarrow$61など$[7],$,
実際にこの条件を満たしている様相論理としてはが知られている。これらのどれも与えられた論理式 のこの論理での充足可能性問題をの中のロ B という形の部分論理式の個数 $\leq Sub(A)\leq|A|$ の可能世界のクリプキモデルに( は任意の定数) 個以下の可能世界のクリ
ついての充足可能性に還元できる。 またプキモデルについての充足可能性問題に還元できる論理も知られている [1]。
$\mathrm{S}5[6],$$\mathrm{K}45$$\mathrm{S}4.3$$\mathrm{K}\mathrm{D}45[3]$

$A$

$A$

$k$

$|A|^{k}$4S4.2 が PSPACE-complete であること

4.1

S4.2 が PSPACE-hard であること

S4.2 は$\mathrm{S}4$に公理スキーマ◇口 A$\supset$

口◇ Aを加えた体系である。 canonical model の手法により

reflexive:transitive:
weakly directed:$\forall x.xRx$$\forall x,$$\forall x,$.

$y,$ $z.(xRy\wedge yRzarrow xRz)$ .
$y,$$z.(xRy\wedge xRzarrow\exists w.(yRw\wedge zRw)$.

で特徴づけられるクリプキフレ $-$ ムに関し健全かつ完全になっていることが示される。 さらに generated frame の概念と filtration method を用いることにより reflexive, transitive
かつ

directed:$\forall x,$$y.\exists z.(xRZ\wedge yRz)$.

で特徴づけられる有限クリプキフレームに関し S42 が健全かつ完全になっていることが示される [5]。
ここでは [3] で S4 に対して適用された手法を S42 について適用することにより、PSPACE-hardness を示す。その方法は、 PSPACE-complete であることが知られていへの多項式時間変換
から様相論理式
る 2 階の古典命題論理 QBF $[4, 8]$ の論理式
を定義し、
$A$

$(A)^{\mathrm{o}}$$()^{\mathrm{o}}$QBF $|=A$$\Leftrightarrow$reflexive, transitive, directed で特徴づけられる
有限クリプキフレームのクラスの中のクリプキフレーム $(M, R)$ が存在して$(M, R)|=(A)^{\mathrm{o}}$ .
$\mathcal{F}$を示すという方法である。
最初に、 QBF formula $A=Q_{1}p_{1}\ldots Q_{m}pmA’$ から$(A)^{\mathrm{o}}$を作る。

$(A)^{\mathrm{o}}$に出現する命題変

62

数は$p_{1},$$\ldots,p_{m},$$d_{0,\ldots,1}dm+$depthに限られる。

$\mathrm{d}\mathrm{e}\mathrm{f}\equiv\bigwedge_{i=1}^{m+}(d_{i}1\supset d_{i-1})$

determined$(A)^{\mathrm{o}}$の部分論理式を定義する。

.

$(d_{i}\supset((p_{i}\supset\square (d_{i}\wedge\neg d_{m+1}\supset p_{i}))$$\mathrm{d}\mathrm{e}\mathrm{f}\equiv\bigwedge_{i=1}^{m}$$\wedge(\neg p_{i}\supset\square (d_{i}\wedge\neg dm+1\supset\neg p_{i})))$

branchA.

$\mathrm{d}\mathrm{e}$$\equiv^{\mathrm{f}}$$(\text{◇}(di+1^{\wedge}\urcorner di+2\wedge pi+1)$$i+ \bigwedge_{\{i|Q1=\forall\}}((d_{i}\wedge\urcorner di+1)\supset$$\wedge\text{◇}(d_{i}+1\wedge\neg di+2\wedge\neg p_{i+1})))$$(\text{◇}(d_{i+1^{\wedge d)}}\neg i+2^{\wedge pi1}+$$\{i|Q_{i+}\bigwedge_{1=}(\exists\}(d_{i}\wedge\neg d_{i1}+)\supset$$\vee\text{◇}$これらの部分論理式を用いて$(A)^{\mathrm{o}}$($di+1\wedge\urcorner d_{i}+2$A$\neg p_{i+1}$

) .
$))$

を次の論理式と定義する :$d_{0}\wedge\urcorner d_{1}\wedge\square (depth\wedge determined\wedge branChingA\wedge(d_{m}\wedge\neg d_{m+1}\supset A’))$

Theorem 2 任意の 2 階古典命題閉論理式
QBF $|=A$$\Leftrightarrow$

$A$

.

に対し

reflexive, transitive, directed で特徴づけられる
有限クリプキフレームのクラス$\mathcal{F}$の中のクリプキフレーム

valuation$V$と$(M, R, V)\vdash-_{S}(A)^{\mathrm{o}}$

証明

(

と

$(M, R)$$s\in M$ が存在して

.

の証明)

$\Rightarrow$$A=Q_{1}p_{1}\ldots Q_{m}p_{m}A’$とし、 QBF $|=A$ を仮定する。

枝分かれが 1 か 2 かである有限木の reflexive transitive closure $(M, R)$ を考える。すな
わち:$M$は有限集合であり、$\mathrm{R}$は$\forall x\in M.xR_{X}$$\forall x,$

$y,$

.

$z\in M.(xRy\wedge yRzarrow xRz)$ .

$\forall x,$$y\in M.(xRy\wedge yRxarrow x=y)$ .

$\forall u,$$v\in\{y|yR^{-1}x\}\subseteq M.(uRv\vee vRu)$

.

さらに
$x$

succ

$y^{\mathrm{d}\mathrm{e}\mathrm{f}}\equiv XRy\Lambda\forall z\in M.((xR_{Z}\wedge y\neq z\wedge x\neq z)arrow\chi_{ZRy))\wedge}\chi yR_{X})$succ$x1\wedge x$

.

と定義して
$x$

succ

$x2\wedge x$

succ $x3arrow(x1=x2x2=x3x3=x2)$ .

63を満たしているものとする。
さらに $(M, R)$ から $a\not\in M$ である

をとり、

$a$

で定義される $(M’, R’)$ はに属しreflexive, transitive, directed で特徴づけられる有限クリプキフレームのクラスの中で $(M, R)$ の高さが $m$ であるものを考えるとこの中にている。 このようなを true に、 $i\leq j$ で$M$ の root $r_{0}\in M$ で “ $i\leq i$ ならば高さが高さの可能世界でが true, $i\leq j$ でが高さ の可能世界で falseの可能世界で true ならば高さ でもが存在してが false” を満たすような valuation
ならば高さ でも$\forall x,$$y\in M\cup\{a\}.(xR\prime yrightarrow xRyy=a),$ $M’=M\cup\{a\}$$\mathcal{F}$$(\dot{M}’, R’)$

$j$

$j$

$p_{i}$

$i$

$j$

$i$

$d_{i}$$p_{i}$$p_{i}$$V$$p_{i}$$(M’, R’, V)|=_{r_{0}}(A)^{\mathrm{o}}$となるような $(M’, R’)$ が存在する。
なぜなら QBF $|=Q_{1P}1\ldots QmpmA^{;}$ なので $Q_{1}p_{1}\ldots Q_{m}Pm\cdot A^{J}$ を$\bullet$$\bullet$\forall pi.B(乃) ならば$\exists p_{i}.B(p_{i})$

QBF
QBF

].

「

$B[p_{i}/\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}]/B$$p_{i}/\mathrm{f}\mathrm{a}1_{\mathrm{S}}\mathrm{e}$

ならば

] ならば
] ならば

$|=B\mathrm{r}p_{i}/\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$B[p_{i}/\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}]$$|=B\mathrm{r}p_{i}/\mathrm{f}\mathrm{a}1_{\mathrm{S}}\mathrm{e}$,$B[p_{i}/\mathrm{f}\mathrm{a}1_{\mathrm{S}}\mathrm{e}]$.

と展開する。
$p_{i},$$\ldots,p_{m}$$Val=${の (古典論理の) valuation の集まりを$\rho_{i}|i\leq 2^{m},$$\rho_{i}$:$\{p_{1},$$\ldots,p_{m}\}arrow\{\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$, false}} と書くと、 ある $Valo\subseteq Val$ が存在しは正しいフ “ $-$ 式にて展開 $\text{された論理式は}\bigwedge_{\rho}\in Val0A’\rho$ と書ける。そしてそれぞれのなっている。 が ならば高さ $i-1$ の可能世界から高さ の可能世界への枝分かれは 2が ならば高さ $i-1$ の可能世界から高さ の可能世界への枝分かれは 1 つという
つ、の valuation が \rho \in Val0 を満
ような $(M, R)$ を選び、 高さ $m$ の可能世界でのでたすような valuation $V$ を選んでやれば $(M’, R’, V’)$ が root
$A’\rho$$i$$\forall$$p_{i}$$i$$\exists$$p_{i}$$p_{1},$$\ldots,p_{m}$$r_{0}$$(M’, R’, V)|=_{r_{0}}(A)^{\mathrm{o}}$となることは簡単に確かめられる。
( の証明)の中の
reflexive, transitive, directed で特徴づけられる有限クリプキフレームのクラスとタリプキフレーム $(M, R)$ と valuation $V$ と $r_{0}\in M$ が存在してを $Q_{j+1p_{j+}..Q_{m}A}1\cdot p_{m}.$’ からなっていると仮定する。 を任意の $t\in M$ とする。と $p_{i}\not\in V(t)$ ならばに対して $p_{i}\in V(t)$ ならば$i<j$ であるすべてのは $A’\text{に可能}$と置き換えてできる QBF の論理式とする。 $A_{0}^{t}=A$ であり、に関するある (古典論理の) valuation をほ
世界 での valuation にしたがいであることに注意。 $(M, R, V)\models_{r_{0}}\square (d_{m}\supset A’)$ が成立っているので、 $r_{0}Rt$
どこしたは true である。
かつ $(M, R, V)\vdash-tdm$ ならば.
についての簡単な帰納法により、 $r_{0}Rt$ かつ $(MR, V):\vdash-tdm-j\wedge\neg dm-j+1$ ならば QBF
が true であることを示すことができる。 $(M, R, V)\vdash-r_{0}d_{0}\wedge\neg d_{1}$ なので $A_{0}^{S}=A$ はtrue であることがいえたことになる。口$\Leftarrow$$\mathcal{F}$$(M, R, V)\models_{r_{0}}(A)^{\mathrm{o}}$$t$$A_{j}^{t}$$p_{i}=\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$p_{i}$$A_{m}^{t}$$p_{i}=\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}$$t$$p_{1},$$A’\rho$$A_{m}^{t}$$j$$A_{m-j}^{t}$$\ldots,p_{m}$$\rho$

64

Theorem 3 S4.2 の充足可能性問題は PSPACE-hard である。

S4.2 が PSPACE に入ること

4.2

Theorem 4 S4.2 の充足可能性問題は PSPACE に属す。
証明 [10] の Theorem 4.4. の–部である、任意の論理式 $A$ に対して

S4$.2 \vdash A\Leftrightarrow \mathrm{S}4\vdash\bigwedge_{\square B\in sf(A)}(\text{◇口}B\supset\square \text{◇口}B)\supset A$.

を用いる。 $||Sf(A)||\leq|A|$ なので からく。B\in Sf(A)(◇口 B\supset 口◇口 B)\supset A への変換は線形時間で可能である。そして S4 が PSPACE-complete であることから S42 が bf
PSPACE に属すことがわかる。口
$A$

定理 3 と定理 4 より

Theorem 5 S4.2 の充足可能性問題は PSPACE-complete である。

5

謝辞
本研究に際し、 さまざまな助言をしていただいた日本大学の志村立矢さんに感謝します。

参考文献
[1]

. Chagrov and M. V. Zakharyashchev. An essay in complexity aspects of intermediate calculi. Proceedings of the Fourth Asian Logic Conferences, 1990.
$\mathrm{A}.\mathrm{V}$[2] R. Goldblatt. Logic for Time and Computation. Second edition. Center for the Studyof Languages and Information, 1992[3]

. Halpern and Y.Moses. A guide to completeness and complexity for modal logics
of knowledge and belief. Artificial Intelligence, 54:319-379, 1992.

[4]. Ullman. Introduction to Automata Theory, Languages andComputation. Addison-Wesley, 1979.

[5]
[6]

$\mathrm{J}.\mathrm{Y}$$\mathrm{J}.\mathrm{E}$. Hopcroft and$\mathrm{G}.\mathrm{E}$. Hughes and$\mathrm{J}.\mathrm{D}$$\mathrm{M}.\mathrm{J}$. Cresswell. A Companion to Modal Logic. Methuen, 1984.

. Ladner. The computational complexity of provability in systems of modal propositional logic. Siam. J. Comput., 6:467-480, 1977.
$\mathrm{R}.\mathrm{E}$65[7] H. Ono and A. Nakamura. On the size of refutation Kripke models for some linear
modal and tense logics. Studia Logica, 39:325-333.
[8]$\mathrm{C}.\mathrm{H}$. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.

[9] T. Shimura. Cut-free systems for the modal logic S4.3 andematical Logic, 25:57-73, 1991.

$\mathrm{S}4.3\mathrm{G}\mathrm{r}\mathrm{z}$. Reports on Math-[10] T. Shimura. Cut-free systems for some modal logics containing S4. Reports on Mathematical Logic, 26:39-65, 1992.
[11] R. Statman. Intuitionistic Propositional Logic is Polynomial-Space Complete. Theoretical Computer Science, 9:67-72, 1979.