Resolution is Cut-Free

Abstract : In this article, we show that the extension of the resolution proof system to deduction modulo is equivalent to the cut-free fragment of the sequent calculus modulo. The result is obtained through a syntactic translation, without using any cut-elimination procedure. Additionally, we show Skolem theorem and inversion/focusing results. Thanks to the expressiveness of deduction modulo, all these results also apply to the cases of higher-order resolution, Peano's arithmetic and Gentzen's LK.
Type de document :
Article dans une revue
Liste complète des métadonnées

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

https://hal-mines-paristech.archives-ouvertes.fr/hal-00743218
Contributeur : Claire Medrala <>
Soumis le : jeudi 18 octobre 2012 - 14:48:03
Dernière modification le : jeudi 7 février 2019 - 17:55:54
Document(s) archivé(s) le : samedi 19 janvier 2013 - 03:38:02

Fichier

Resolution_CutFree-3.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Olivier Hermant. Resolution is Cut-Free. Journal of Automated Reasoning, Springer Verlag, 2010, 44 (3), pp.245-276. ⟨10.1007/s10817-009-9153-6⟩. ⟨hal-00743218⟩

Partager

Métriques

Consultations de la notice

151

Téléchargements de fichiers

181