| 作成者 |
|
|
|
|
|
|
|
|
|
| 本文言語 |
|
| 出版者 |
|
|
|
| 発行日 |
|
| 収録物名 |
|
| 巻 |
|
| 出版タイプ |
|
| アクセス権 |
|
| 関連DOI |
|
|
|
| 関連URI |
|
|
|
| 関連情報 |
|
|
|
| 概要 |
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.続きを見る
|
Mendeley出力
trcs178.ps
trcs178