HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Book sections

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.
Document type :
Book sections
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:41:03 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00098993, version 1



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⟩



Record views