<テクニカルレポート>
Infiniteness of proof $ left( alpha \right) is polynomial-space complete

作成者
本文言語
出版者
発行日
雑誌名
出版タイプ
アクセス権
概要 The infiniteness problem is investigated for the set proof $ left (alpha \right) $ of closed $ lamda -terms in \beta-normal $ form which has a as their types. The set is identical to the set of normal... form proofs for $ alpha $ in the natural deduction system for implicational fragment of intuitionistic logic. It is shown that the infiniteness is determined by checking Aterms with the depth at most $ 2 mid alpha mid^2 $. Thus the problem is solved in polynomial-space. The bound is obtained by an estimation of the length of an irredundant chain of sequents in type assignment system in sequent calculus formulation. Then the non-emptiness problem of $ proof left( alpha\right) $, which is identical to the provability of $ alpha $, is deduced to the problem of infiniteness problem by a transformation of types. Since the provability is polynomial- space complete (Statman, Theoret. Comput. Sci. 9 (1979) 97-105), the infiniteness problem is polynomial-space complete.続きを見る

本文情報を非表示

rifis-tr-92 pdf 537 KB 80  

詳細

レコードID
査読有無
関連情報
タイプ
登録日 2009.04.22
更新日 2017.01.20