Combinatorial Flows and Proof Compression

Lutz Straßburger 1
1 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
Résumé : Cet article introduit la notion de fleuves combinatoires comme généralisation des preuves combinatoires qui comprend également la coupure et la substitution comme méthodes de compression des preuves. Nous montrons un procédure de normalisation des fleuves combinatoires, et la traduction entre les preuves syntactiques du calcul de séquents, de l’inférence profonde, des systèmes de Frege, et les fleuves combinatoires.
Type de document :
Rapport
[Research Report] RR-9048, Inria Saclay. 2017
Liste complète des métadonnées

Littérature citée [45 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01498468
Contributeur : Lutz Straßburger <>
Soumis le : jeudi 30 mars 2017 - 10:15:59
Dernière modification le : mercredi 25 avril 2018 - 10:45:27

Fichier

RR-9048.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01498468, version 1

Citation

Lutz Straßburger. Combinatorial Flows and Proof Compression. [Research Report] RR-9048, Inria Saclay. 2017. 〈hal-01498468〉

Partager

Métriques

Consultations de la notice

444

Téléchargements de fichiers

220