| Creator |
|
|
|
|
|
|
|
|
|
| Language |
|
| Publisher |
|
|
|
| Date |
|
| Source Title |
|
| Vol |
|
| Publication Type |
|
| Access Rights |
|
| Related DOI |
|
|
|
| Related URI |
|
|
|
| Relation |
|
|
|
| Abstract |
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.show more
|
Export Mendeley
trcs178.ps
trcs178