近年の意味解析における照応解析では，語の間の意味的類似度を用いて照応表現(apaphoricexpression)の先行詞を同定するといった深層学習・機械学習によるアプローチが主流となっている．一方，依存型意味論(DependentTypeSemantics,DTS)は，依存型理論による自然言語の意味論の一つであり，特に照応(anaphora)と前提(presupposition)はDTSが説明できる意味現象の中枢となっている．この論文では，DTSの未指定型(underspeciﬁedtypes)を用いて照応表現の可能な先行詞を全て探索し，その前後の文脈から照応が可能な先行詞のうちどの対象が整合性が取れているかを判定する手法を提案する．また，提案する手法が，どれだけの照応解析の問題を解くことができるかを評価する．

DTSでは近年，未指定型(underspeciﬁedtypes)と呼ばれる新たな理論的装置が導入された[1]．DTSにおける照応解析は，未指定型を介した証明探索として再定式化され，未指定型を介した照応解析が実装された[2]．一般的に照応解析とは，英語を例にとれば，テキストの中にあるitやheなどの照応表現の先行詞を同定するタスクである．一方，DTSに限らず形式意味論における照応理論のタスクは（照応表現の先行詞を同定することではなく）どの表現が照応表現の先行詞になりうるか（到達可能性）を予測すること，および照応表現の到達可能なすべての表現について，その表現が先行詞である場合の意味を与えることである．本研究の目的は，DTSの照応理論のそのような性質を利用して，照応表現の先行詞を同定する手法を提案・実装することである．到達可能な表現が照応表現の先行詞であるか否かは，そこから得られた意味表示に前後の文脈との整合性があるか否かで判定することができる．証明支援系(proofassistants)の一つであるCoq[3]を用いて，DTSの未指定型を介した照応解析を実装する．まず，Coqが提供するrefineタクティクと本研究が実装する自動照応探索タクティクを用いて到達可能な先行詞を全て探索する．次に，照応表現を含むテキストに照応表現に到達可能な先行詞を当てはめたテキストを生成する．最後に，接続詞と用法ごとに分類した手法により生成したテキストの推論を行い，推論が証明可能であるか証明不可能であるかにより，対象の前後の文脈との整合性を判定する．