label{sec:moti}アスペクト(aspect;相)とはある一つの事象(eventuality;イベント)についてのある時間的側面を述べたものである．しかしながら同時にアスペクトとは言語に依存してそのような統語的形態，すなわち進行形や完了形などと言った構文上の屈折・語形変化を指す．本稿で形式化を行うのは，このような固有の言語に依存したアスペクトの形態ではなく，言語に共通したアスペクトの意味である．アスペクトの概念はどうしても固有の言語の構文と結び付いて定義されているため，用語が極めて豊富かつ不定である．同じ完了と言っても英語のhave＋過去分詞形と日本語のいわゆる「た」という助詞とはその機能・意味に大きな差異がある．したがって形式的にアスペクトの意味を述べるためにはまずこうした用語・概念の整理・統合を行った上で，改めて各概念の定義を論理的に述べる必要がある．このような研究では，近年では数多くのアスペクトの理論がイベント構造の概念によって構築されてきた．すなわち，すべての事象に共通な，アスペクトをともなう前の原始的・抽象的な仮想のイベント構造を考え，アスペクトとはこのイベント構造の異なる部位に視点(レファランス)を与えることによって生じるものとする説明\footnote{\cite{Moens88,Gunji92,Kamp93,Blackburn96,Terenziani93}他多数．個々の理論については第\ref{sec:akt}節で詳述する.}である．本稿のアスペクトの形式化も基本的にはこのイベント構造とレファランスの理論から出発する．しかしながらこのイベント構造とレファランスを古典的な論理手法によって形式化しようするとき，以下のような問題が伴う．まず，(1)時間の実体を導入する際に点と区間を独立に導入すると，アスペクトの定義においては，点と区間，点と点，区間と点の順序関係や重なり方に関して関係式が量産されることになる．次に，(2)アスペクトとは本来それだけで存在しうるものではなく，もともとある事象から派生して導き出されたものである．したがってアスペクトを定義する際にその条件を静的に列挙するだけでは不十分であり，もとにある事象の原始形態からの動的な変化として提示する必要がある．本稿では言語に共通なアスペクトのセマンティクスを形式化するために，アロー論理\cite{Benthem94}を導入する．第\ref{sec:arw}章で詳述するが，アロー論理とは命題の真偽を云々する際に通常のモデルに加えてアローと呼ばれる領域を与える論理である．アロー論理では，アロー自身に向きが内在しているために，(1)の問題でいうところの順序関係に関して記法を節約することができる．さらに動的論理(dynamiclogic)にアローを持ち込むことにより，動的論理の中の位置(サイト)と状態移動の概念を時間の点と区間の概念に対応づけることができる．このことは，アスペクトの仕様記述をする際に点と区間の関係が仕様記述言語(アローを含む動的論理)の側で既に定義されていることを意味し，さらに記述を簡潔にすることができる．本稿では，アスペクトの導出をこのような点と区間の間の制約条件に依存した視点移動として捉え，アスペクトの付加を制約論理プログラミングの規則の形式で記述する．したがって(2)の問題でいうところの動的な過程は，論理プログラミングの規則の実行過程として表現される．本稿は以下の構成をとる．まず第\ref{sec:akt}章では，言語学におけるアスペクトの分類と形式化を行い，先に述べた用語と概念の混乱を整理する．次にイベント構造とレファランスに関わる理論について成果をサーベイする．次に第\ref{sec:arw}章では，アロー論理を導入する．この章では，引き続いて，われわれの時間形式化に関する動機がアロー論理のことばでどのように述べられるかも検討する．すなわち，アローを向きをともなった区間とみなし，アスペクトの導出規則の仕様を定める．続く第\ref{sec:acc}章では，この仕様を完了や進行などさまざまなアスペクトに適用し，それらに関する導出規則を定義する．第\ref{sec:discus}章では，導出規則におけるアスペクトの付加についてその有用性と応用可能性を検討し，本研究の意義をまとめる．