<テクニカルレポート>
Case Calculus for Classical Logic

作成者
本文言語
出版者
発行日
雑誌名
出版タイプ
アクセス権
概要 After the work of Griffin in 1990, there have been many works to extend the Curry-Howard isomorphism for classical logic. Most of these research uses sequent calculus with multiple conclusions. In thi...s paper, we introduce a new natural deduction formulation with one conclusion for implicational classical logic. The idea of the formulation is based on proof by "case analysis". It is natural and captures our intuition in logical reasoning. We define reduction rules and prove weak normalization. As a corollary, we have the subformula property for normal proofs. The natural deduction systems proposed so far does not have subformula property. We also explain some computational meaning of our calculus by showing the simulation of \beta-reduction, disjunction and catch/throw.続きを見る

本文情報を非表示

trcs178.ps gz 54.2 KB 34  
trcs178 pdf 205 KB 50  

詳細

レコードID
査読有無
関連情報
タイプ
登録日 2009.04.22
更新日 2017.01.20