A framework for proof systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Journal of Automated Reasoning Année : 2010

A framework for proof systems

Résumé

Linear logic can be used as a meta-logic to specify a range of object-level proof systems. In particular, we show that by providing different polarizations within a focused proof system for linear logic, one can account for natural deduction (normal and non-normal), sequent proofs (with and without cut), and tableaux proofs. Armed with just a few, simple variations to the linear logic encodings, more proof systems can be accommodated, including proof system using generalized elimination and generalized introduction rules. In general, most of these proof systems are developed for both classical and intuitionistic logics. By using simple results about linear logic, we can also give simple and modular proofs of the soundness and relative completeness of all the proof systems we consider.
Fichier principal
Vignette du fichier
nigam-ijcar.pdf (311.62 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-00772562 , version 1 (10-01-2013)

Identifiants

  • HAL Id : hal-00772562 , version 1

Citer

Nigam Vivek, Dale Miller. A framework for proof systems. Journal of Automated Reasoning, 2010, 45 (2). ⟨hal-00772562⟩
132 Consultations
73 Téléchargements

Partager

Gmail Facebook X LinkedIn More