A logic program for transforming sequent proofs to natural deduction proofs

Amy Felty 1
1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In this paper, we show that an intuitionistic logic with second-order function quantification, called hh² here, can serve as a meta-language to directly and naturally specify both sequent calculi and natural deduction inference systems for first-order logic. For the intuitionistic subset of first-order logic, we present a set of hh² formulas which simultaneously specifies both kinds of inference systems and provides a direct and concise account of the correspondence between cut-free sequential proofs and normal natural deductions proofs. The logic of hh² can be implemented using such logic programming techniques as providing operational interpretations to the connectives and implementing unification on lambda-terms. With respect to such an interpreter, our specification provides a description of how to convert a proof in one system to a proof in the other. The operation of converting a sequent proof to a natural deduction proof is functional in the sense that there is always one natural deduction proof corresponding to each sequent proof. Our specification, in fact, provides a direct implementation of the transformation in this direction.
Type de document :
Rapport
[Research Report] RR-1301, INRIA. 1990, pp.21
Liste complète des métadonnées

https://hal.inria.fr/inria-00075258
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 17:50:03
Dernière modification le : samedi 27 janvier 2018 - 01:31:24
Document(s) archivé(s) le : mardi 12 avril 2011 - 18:24:14

Fichiers

Identifiants

  • HAL Id : inria-00075258, version 1

Collections

Citation

Amy Felty. A logic program for transforming sequent proofs to natural deduction proofs. [Research Report] RR-1301, INRIA. 1990, pp.21. 〈inria-00075258〉

Partager

Métriques

Consultations de la notice

98

Téléchargements de fichiers

48