From Syntactic Proofs to Combinatorial Proofs

Abstract : In this paper we investigate Hughes’ combinatorial proofs as a notion of proof identity for classical logic. We show for various syntactic formalisms including sequent calculus, analytic tableaux, and resolution, how they can be translated into combinatorial proofs, and which notion of identity they enforce. This allows the comparison of proofs that are given in different formalisms.
Type de document :
Chapitre d'ouvrage
International Joint Conference on Automated Reasoning, IJCAR 2018, pp.481-497, 2018, 978-3-319-94204-9
Liste complète des métadonnées

https://hal.inria.fr/hal-01942275
Contributeur : Lutz Straßburger <>
Soumis le : lundi 3 décembre 2018 - 09:58:08
Dernière modification le : mercredi 5 décembre 2018 - 01:14:25

Fichier

tableau-def.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01942275, version 1

Citation

Matteo Acclavio, Lutz Straßburger. From Syntactic Proofs to Combinatorial Proofs. International Joint Conference on Automated Reasoning, IJCAR 2018, pp.481-497, 2018, 978-3-319-94204-9. 〈hal-01942275〉

Partager

Métriques

Consultations de la notice

29

Téléchargements de fichiers

7