知識論理におけるKL証 明図のLJ化(修士論文)

「aはpが真であることを知っている」ことを表現するKnowledge-operatorを用いた知識命題においてGentzenスタイルに知識に関する推論規則を加えたKLK体系を提示し，Hilbertスタイルの演繹体系と同等の証明力を持つことを示した．さらに，コンピュータによる自動証明アルゴリズムを提案し，知識命題対する自動証明を可能とした．