A framework for proof systems

Nigam Vivek 1 Dale Miller 1, 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : 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.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2010, 45 (2)
Liste complète des métadonnées

https://hal.inria.fr/hal-00772562
Contributeur : Dale Miller <>
Soumis le : jeudi 10 janvier 2013 - 17:15:29
Dernière modification le : jeudi 12 avril 2018 - 01:48:33
Document(s) archivé(s) le : jeudi 11 avril 2013 - 04:07:52

Fichier

nigam-ijcar.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00772562, version 1

Collections

Citation

Nigam Vivek, Dale Miller. A framework for proof systems. Journal of Automated Reasoning, Springer Verlag, 2010, 45 (2). 〈hal-00772562〉

Partager

Métriques

Consultations de la notice

184

Téléchargements de fichiers

98