Name
Abstract | ||
|---|---|---|
A natural deduction system NDIL described here admits normalization and has subformula prop- erty. It has standard axioms A ' A, ' 1, standard introduction and elimination rules for &; (linear implication), and quantiers. The rules for are now standard too. Structural rules are (implicit) permutation plus contraction and weakening for m-formulas. The rules for ! use an idea of D. Prawitz. By a m-formula we mean 1, any formula beginning with !, and any expression < >!A ,w here is a list of formulas and m-formulas, and A is a formula. Derivable objects are sequents ' A where is a multiset of formulas and m-formulas, and A is a formula. The rules for !, weakening and contraction are as follows: <> I '!A < >!A'!A !E |
Year | DOI | Venue |
|---|---|---|
1998 | 10.1007/s001530050106 | Arch. Math. Log. |
Keywords | Field | DocType |
natural deduction,linear logic | Discrete mathematics,Normalization (statistics),Multiplicative function,Algebra,Natural deduction,Sequent,Linear logic,Mathematics,Curry–Howard correspondence | Journal |
Volume | Issue | ISSN |
37 | 5-6 | 0933-5846 |
Citations | PageRank | References |
4 | 0.69 | 7 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Grigori Mints | 1 | 235 | 72.76 |