Focusing in linear meta-logic: extended report

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 {\em 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 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.
Type de document :
Rapport
[Research Report] Maybe this file need a better style. Specially the proofs., 2008
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00281631
Contributeur : Vivek Nigam <>
Soumis le : samedi 24 mai 2008 - 11:06:58
Dernière modification le : jeudi 11 janvier 2018 - 06:19:44
Document(s) archivé(s) le : vendredi 28 mai 2010 - 19:59:44

Fichiers

techreport.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00281631, version 1

Collections

Citation

Vivek Nigam, Dale Miller. Focusing in linear meta-logic: extended report. [Research Report] Maybe this file need a better style. Specially the proofs., 2008. 〈inria-00281631〉

Partager

Métriques

Consultations de la notice

255

Téléchargements de fichiers

77