@article{oai:ryotokuji-u.repo.nii.ac.jp:00000020,
 author = {和手, 正道 and Wate, Masamichi},
 issue = {1},
 journal = {了德寺大学研究紀要, The Bulletin of Ryotokuji University},
 month = {},
 note = {論理学におけるsequentとはある法則に従って並べられた文字列の事である.ここで許される文字は自由変数(a_0,a_1,a_2,……),束縛変数(x_0,x_1,x_2,……),関数記号(f_0,f_1,f_2,……)述語記号(P_0,P_1,P_2,……),論理記号(￢,∧,∨,→,∀,∃,〓)補助記号(カッコとコンマ)だけである.termとformulaは以下のように帰納的に定義される:1.自由変数はtermである.2.fが関数記号で,t_1,……,t_nがtermのとき,f(t_1,……,t_n)はtermである.3.Pが述語記号で,t_1,……,t_nがtermのとき,P(t_1,……,t_n)はformulaである.4.A,Bがformulaのとき,￢A,A∧B,A∨B,A→Bはformulaである.5.A(a)が自由変数aを含むformulaで,xがA(a)の中にない束縛変数のとき,∀xA(x),∃xA(x)はformulaである.6.1〜5以外の方法ではtermやformulaは得られない.sequentは「formulaの有限列〓formulaの有限列」という形の有限列の事である.sequentの証明と言うのは公理から出発して推論規則のみを用いて導き出す事である.(古典論理の公理と推論規則は本文を参照されたい.)Turing machineとはセルによって区切られた左右に無限に長いテープと読み取りヘッドと有限制御部からなる機械で,以下の条件を満たす理論上のデジタルコンピュータのことである.テープ上の各セルには1つのセルに1文字だけ書かれている.(空白文字も特殊文字の1つとみなす.)読み取りヘッドは各時点で1つのセルだけを見ている.各時点で,読み取りヘッドはセルから読み取った文字とその時点における有限制御部の内部状態との組み合わせによってその文字を書き換え,右隣または左隣のセルに移動し,内部状態を変化させ,次の時点へと移る.Turing machineに文字列を入力してから出力が得られるまでの時間は一般に入力が大きくなるほど時間を消費するので,その時間を入力文字列の長さnの関数で表す.もちろん,Turing machineの性能によって消費時間は異なる.例えば昔のコンピュータは遅いが最近のコンピュータは速い.しかし,この時間の違いは高々定数倍である.従って,定数倍の違いは無視する.すなわち性能による差は無視して,もっと本質的な処理時間について考える.また,nが比較的小さい場合は定数で押さえられるから小さいnは無視して,十分大きいnについて考える.例えば,処理時間が多項式a_0n^i+a_1n^<i-1>+……+a_<i-1>n+a_iの場合十分大きいnに対してはこの式は(a_0+1)n^iで押さえられ,a_0+1は定数だからこれをn^iと同一視する.古典論理において与えられたsequentが証明可能か否かの判定は時間をいとわなければ可能である事はよく知られている.しかしながら,sequentの証明可能性の判定に要する時間はどのくらい必要かということはあまり研究されていないようである.そこで,その判定時間を調べる事は興味深い事と思われる.本論分では2^<nlogn>ステップで(命題論理の場合は2^nステップで)これが可能である事を示した.(古典論理というのは古典述語論理の事であり,特に∀と∃を用いない論理を古典命題論理という.)},
 pages = {77--85},
 title = {Modified Decision Time of Classical Logic},
 year = {2007},
 yomi = {ワテ, マサミチ}
}