Name
Abstract | ||
|---|---|---|
It is well known how to use an intuitionistic meta-logic to specify natural deduction systems. It is also possible to use linear logic as a meta-logic for the specification of a variety of sequent calculus proof systems. Here, we show that if we adopt different focusingannotations for such linear logic specifications, a range of other proof systems can also be specified. In particular, we show that natural deduction (normal and non-normal), sequent proofs (with and without cut), tableaux, and proof systems using general elimination and general introduction rules can all be derived from essentially the same linear logic specification by altering focusing annotations. By using elementary linear logic equivalences and the completeness of focused proofs, we are able to derive new and modular proofs of the soundness and completeness of these various proofs systems for intuitionistic and classical logics. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-71070-7_42 | IJCAR |
Keywords | Field | DocType |
various proofs system,classical logic,focused proof,modular proof,linear logic,sequent proof,linear logic specification,linear meta-logic,sequent calculus proof system,elementary linear logic equivalence,proof system,sequent calculus,natural deduction | Discrete mathematics,Natural deduction,Computer science,Proof calculus,Sequent calculus,Algorithm,Proof theory,Sequent,Linear logic,Cut-elimination theorem,Curry–Howard correspondence | Conference |
Volume | ISSN | Citations |
5195 | 0302-9743 | 5 |
PageRank | References | Authors |
0.51 | 17 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vivek Nigam | 1 | 238 | 26.77 |
| Dale Miller | 2 | 2485 | 232.26 |