古典論理計算系から直観主義論理計算系への翻訳

2015 年度 研究成果報告書

• 研究課題/領域番号: 24650002
• 研究種目: 挑戦的萌芽研究
• 配分区分: 基金
• 研究分野: 情報学基礎
• 研究機関: 千葉大学
• 研究代表者: 桜井 貴文 千葉大学, 理学(系)研究科(研究院), 教授 (60183373)
• 研究協力者: 佐藤 雅彦 ; 菊池 健太郎
• 研究期間 (年度): 2012-04-01 – 2016-03-31
• キーワード: 古典論理 / 直観主義論理 / 簡約保存 / CPS変換 / 強正規化性

研究成果の概要

本研究では、古典論理の計算系から直観主義論理の計算系への簡約を保存する翻訳を与える。本研究で考察する古典論理の計算系は、lambda-bar-mu、名前呼びlambda-bar-mu-tilde、値呼びlambda-bar-mu-tildeおよびlambda-muであり、いくつかの簡単な翻訳を合成することにより、新規および既知の翻訳を統一的に導くことができる。そしてこれより上記の古典論理計算系の強正規化性を導くことができる。

自由記述の分野

計算系の論理学的基礎理論