Labelled Proof Systems for Intuitionistic Provability

Didier Galmiche 1 Vincent Balat
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this paper, we propose new labelled proof systems to analyse the intuitionistic provability in classical and linear logics. An important point is to understand how search in a non-classical logic can be viewed as a perturbation of search in classical logic. Therefore, suitable characterizations of intuitionistic provability and related labelled sequent calculi are defined for linear logic. An alternative approach, based on the notion of proof-net and on the definition of suitable labelled classical proof-nets, allows to directly study the intuitionistic provability by constructing intuitionistic proof-nets for sequents of classical linear logic.
Mots-clés : théorie de la démonstration automated deduction proof theory intuitionistic logic linear logic labelled sequent calculus proof nets logique intuitionniste logique linéaire réseaux de preuve deéduction automatique
Type de document :
Chapitre d'ouvrage
D. Basin, M. D'Agostino, D.M. Gabbay, S. Matthews, L. Vigano. Labelled Deduction, 17 (17), Kluwer Academic Publishers, 31 p, 2000, Applied Logic Series, 0-7923-6237-3
Liste complète des métadonnées
https://hal.inria.fr/inria-00098993
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:41:03
Dernière modification le : mardi 24 avril 2018 - 13:34:45

Identifiants

  • HAL Id : inria-00098993, version 1

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Didier Galmiche, Vincent Balat. Labelled Proof Systems for Intuitionistic Provability. D. Basin, M. D'Agostino, D.M. Gabbay, S. Matthews, L. Vigano. Labelled Deduction, 17 (17), Kluwer Academic Publishers, 31 p, 2000, Applied Logic Series, 0-7923-6237-3. 〈inria-00098993〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

120

Contact


archive-ouverte@inria.fr