代数的証明論と余代数的証明論

2012 年度 研究成果報告書

• 研究課題/領域番号: 21700014
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: 情報学基礎
• 研究機関: 京都大学
• 研究代表者: 照井 一成 京都大学, 数理解析研究所, 准教授 (70353422)
• 研究期間 (年度): 2009 – 2012
• キーワード: 数理論理学 / 線形論理 / 部分構造論理 / ルディクス / 再帰型

研究概要

(1) 代数的証明論の研究を部分構造論理の枠組みで推進した。部分構造論理の公理は階層性を成すことを示し、低い階層に属する論理について、カット除去定理と代数的な意味での完備化可能性が正確に対応することを示した。
(2) 線形論理から派生したゲーム意味論の一種であるルディクス理論を、余代数的・計算論的観点から再定式化した。構成的古典命題論理に相当する証明体系について対話的完全性定理を証明し、(プログラミング言語型理論の意味での)一般再帰型の解釈に応用した。

研究成果

• [雑誌論文] Semantic evaluation, intersection types and complexity of simply typed lambda calculus (2012)
  • 著者名/発表者名: K. Terui
  • 雑誌名: Proceedings of 23rd International Conference on Rewriting Techniques and Applications (RTA'12) ページ: 323-338
  • DOI: DOI:10.4230/LIPIcs.RTA.2012.323
• [雑誌論文] Algebraic proof theory for substrutural logics: cut-elimination and completions (2012)
  • 著者名/発表者名: A. Ciabattoni, N. Galatos and K. Terui
  • 雑誌名: Annals of Pure and Applied Logic 巻: 163(3) ページ: 266 - 290
  • DOI: DOI:10.1016/j.apal.2011.09.003
• [雑誌論文] Computational ludics (2011)
  • 著者名/発表者名: K. Terui
  • 雑誌名: Theoretical Computer Science 巻: 412(20) ページ: 2048-2071
  • DOI: DOI:10.1016/j.tcs.2010.12.026
• [雑誌論文] Disjunction property and complexity of substructural logics (2011)
  • 著者名/発表者名: R. Horcik and K. Terui
  • 雑誌名: Theoretical Computer Science 巻: 412(31) ページ: 3992-4006
  • DOI: DOI:10.1016/j.tcs.2011.04.004
• [雑誌論文] MacNeille completions of FL-algebras. (2011)
  • 著者名/発表者名: A. Ciabattoni, N. Galatos and K. Terui.
  • 雑誌名: Algebra Universalis 巻: 66(4) ページ: 405-420
  • DOI: DOI:10.1016/j.tcs.2011.04.004
• [雑誌論文] Church=>Scott = Ptime: an application of resource sensitive realizability (2010)
  • 著者名/発表者名: A. Brunel and K. Terui
  • 雑誌名: Proceedings of Developments in Implicit Computational Complexity (DICE'10) ページ: 31-46
  • DOI: DOI:10.4204/EPTCS.23.3
• [雑誌論文] Infitarycompleteness in ludics (2010)
  • 著者名/発表者名: M. Basaldella and K. Terui
  • 雑誌名: Proceedings of Logic in Computer Science (LICS'10) ページ: 294-303
  • DOI: DOI:10.1109/LICS.2010.47
• [雑誌論文] On the meaning of logical completeness (2010)
  • 著者名/発表者名: M. Basaldella and K. Terui
  • 雑誌名: Logical Methods in Computer Science 巻: 6(4:11) ページ: 1-35
  • DOI: DOI:10.2168/LMCS-6(4:11)2010
• [雑誌論文] Expanding the realm ofsystematic proof theory. (2009)
  • 著者名/発表者名: A. Ciabattoni, L. Strassburger and K. Terui
  • 雑誌名: Proceedings of Computer Science Logic (CSL'09) ページ: 163-178
  • DOI: DOI:10.1007/978-3-642-04027-6_14
• [雑誌論文] On the meaning of logical completeness (2009)
  • 著者名/発表者名: M. Basaldella and K. Terui
  • 雑誌名: Proceedings of Typed Lambda Calculus and its Applications (TLCA'09) ページ: 50-64
  • DOI: DOI:10.1007/978-3-642-02273-9_6
• [学会発表] Proof theory and algebra in substructural logics (2011)
  • 著者名/発表者名: K. Terui
  • 学会等名: 20th International Conference on Automated Reasoning with Analytic Tableaux andRelated Methods (TABLEAUX'11)
  • 発表場所: Bern(Switzerland)
  • 年月日: 2011-07-07
• [学会発表] MacNeille-type completions for residuated lattices and sequent-type proof systems for substructural logics (2011)
  • 著者名/発表者名: K. Terui
  • 学会等名: 2nd International Conference on Order
  • 発表場所: Algebra and Logics, Krakow (Poland)
  • 年月日: 2011-06-08
• [学会発表] 線形論理とラムダ計算の計算量. (2011)
  • 著者名/発表者名: 照井一成
  • 学会等名: 第13回プログラミングおよびプログラミング言語ワークショップ(PPL'11)
  • 発表場所: 札幌
  • 年月日: 2011-03-10
• [学会発表] Algebraic proof theory for nonclassical logics II (2009)
  • 著者名/発表者名: K. Terui
  • 学会等名: Topology,Algebra and Categories in Logic (TACL'09)
  • 発表場所: Amsterdam (Netherlands)
  • 年月日: 2009-07-08
• [学会発表] Semantic methods in substructural and fuzzy logics (2009)
  • 著者名/発表者名: K. Terui.
  • 学会等名: Conferene on Non-Classical Mathematics
  • 発表場所: Hejnice (Czech)
  • 年月日: 2009-06-20