Loading article…
数理論理学において、深層推論とは、構造証明理論における一般的な概念であり、構造の概念を一般化することで、古典的なシーケント計算から脱却し、構造的複雑性の高い状況でも推論を可能にするものです。深層推論という用語は、一般的に構造的複雑性が無限である証明計算に限定して用いられます。本稿では、構造的複雑性がシーケント計算よりも高いものの、無限ではない計算を指すために、非浅層推論という用語を用いますが、これは現時点では確立された用語ではありません。
深層推論は、構造証明論以外の論理学では重要ではない。なぜなら、 深層推論を持つ形式体系の提案につながる現象はすべて、カット除去定理に関連しているからである。深層推論の最初の計算体系は、クルト・シュッテによって提案されたが[ 1 ]、そのアイデアは当時あまり関心を集めなかった。
ヌエル・ベルナップは、構造的証明論の本質を特徴づける試みとして、表示論理を提案した。構造計算は、非可換論理をカットフリーで特徴づけるために提案された。循環計算は、サブコンポーネントの共有の可能性を明示的に考慮できる深層推論システムとして開発された。