核心概念
非良形式節約的証明システムを用いて、FP/polyクラスとFPクラスを特徴付けることができる。
摘要
本論文では、線形論理の変種である節約的論理(parsimonious logic)の文脈で、循環的および非良形式の証明の複雑性理論的側面を調査している。
- 節約的論理では、指数関数的モダリティ!を有限データ上のストリームのコンストラクタとして解釈する。
- 非良形式の節約的証明システムを提示し、FPクラスとFP/polyクラスを捕捉することを示す。
- 証明の健全性は、連続的な切断除去に関する多項式の連続性の上界によって確立される。
- 完全性は、多項式チューリングマシンとアドバイスの符号化に依存する。
- 証明手法の副産物として、様々な有限的証明システムに関する特徴付け結果を確立する。
統計資料
多項式時間チューリングマシンはFPクラスに属する。
多項式サイズの回路ファミリーはFP/polyクラスに属する。