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

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Vivek Nigam, Dale Miller
• Keywords: CADE 2008, Linear Logic, Logical Reasoning, Natural Deduction, Natural Deduction Systems