1. Kyoto University Research Information Repository
  2. 400　数理解析研究所
  3. 1.講究録
  4. 2228 証明と計算の理論と応用
このアイテムのアクセス数: 211

    このアイテムの引用には次の識別子を使用してください: http://hdl.handle.net/2433/279725
このアイテムのファイル:
ファイル 記述 サイズフォーマット 
2228-05.pdf4.22 MBAdobe PDF見る/開く
完全メタデータレコード
DCフィールド値言語
dc.contributor.author益岡, 幸弘ja
dc.contributor.alternativeMasuoka, Yukihiroen
dc.date.accessioned2023-03-14T02:54:14Z-
dc.date.available2023-03-14T02:54:14Z-
dc.date.issued2022-08-
dc.identifier.urihttp://hdl.handle.net/2433/279725-
dc.description.abstract循環証明体系とはその証明図がサイクル付きの木の形になっている証明体系である．J. Brotherstonは帰納的定義付き一階述語論理に対する循環証明体系CLKIDWを提案した[4]．彼はCLKIDWにおけるカット除去性が成り立たないと予想した[2]．その予想が正しいことを示した[11]の内容を紹介する．証明は反例を与えることによって行われる．つまり，CLKIかでカットありでは証明可能であるが，カットなしでは証明できないシークエントを具体的に与える．反例となるシークエントには2種類の帰納的述語が出現する．これらの帰納的述語は盾感的にはどちらも自然数の加法を定義していると解釈される．反例となるシークエントがカットありで証明可能なことは具体的な証明図を与えることで示す．反例となるシークエントがカットなしで証明できないことは，そのシークエントのカットなし証明図の存在を仮定し，CLKIDWの証明図の有限性に矛盾させることで示す．ja
dc.language.isojpn-
dc.publisher京都大学数理解析研究所ja
dc.publisher.alternativeResearch Institute for Mathematical Sciences, Kyoto Universityen
dc.subject循環証明体系ja
dc.subjectカット除去ja
dc.subject帰納的定義ja
dc.subject帰納法ja
dc.subject証明論ja
dc.subjectcyclic/circular proof systemen
dc.subjectcut-eliminationen
dc.subjectinductive definitionen
dc.subjectinductionen
dc.subjectproof theoryen
dc.subject.ndc410-
dc.title循環証明体系におけるカット除去の反例について (証明と計算の理論と応用)ja
dc.typedepartmental bulletin paper-
dc.type.niitypeDepartmental Bulletin Paper-
dc.identifier.ncidAN00061013-
dc.identifier.jtitle数理解析研究所講究録ja
dc.identifier.volume2228-
dc.identifier.spage47-
dc.identifier.epage58-
dc.textversionpublisher-
dc.sortkey05-
dc.address総合研究大学院大学複合科学研究科情報学専攻ja
dc.address.alternativeThe Graduate University for Advances Studies (SOKENDAI)en
dcterms.accessRightsopen access-
dc.identifier.pissn1880-2818-
dc.identifier.jtitle-alternativeRIMS Kokyurokuen
出現コレクション:2228 証明と計算の理論と応用

アイテムの簡略レコードを表示する

Export to RefWorks


出力フォーマット 


このリポジトリに保管されているアイテムはすべて著作権により保護されています。