Fiche du document
2019
- handle: 10670/1.tz5zxd
- hal: hal-01621420
info:eu-repo/semantics/OpenAccess
Mots-clés
normalisation logic of proofs cut-elimination proof sequents 2010 MSC: 03F05 ,03B60 ACM: I.: Computing Methodologies/I.2: ARTIFICIAL INTELLIGENCE/I.2.4: Knowledge Representation Formalisms and Methods/I.2.4.1: Modal logic ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGESCiter ce document
Brian Hill et al., « An Analytic Calculus for the Intuitionistic Logic of Proofs », HAL-SHS : philosophie, ID : 10670/1.tz5zxd
Métriques
Partage / Export
Résumé
The goal of this paper is to take a step towards the resolution of the problem of finding an analytic sequent calculus for the logic of proofs. For this, we focus on the system Ilp, the intuitionistic version of the logic of proofs. First we present the sequent calculus Gilp that is sound and complete with respect to the system Ilp; we prove that Gilp is cut-free and contraction-free, but it still does not enjoy the subformula property. Then, we enrich the language of the logic of proofs and we formulate in this language a second Gentzen calculus Gilp *. We show that Gilp * is a conservative extension of Gilp, and that Gilp * satisfies the subformula property.