Focusing in Linear Meta-logic

9 years 7 days ago
Focusing in Linear Meta-logic
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 focusing annotations 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
Vivek Nigam, Dale Miller
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where CADE
Authors Vivek Nigam, Dale Miller
Comments (0)