Accéder directement au contenu Accéder directement à la navigation
Pré-publication, Document de travail

A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization

Abstract : We prove the syntactic soundness of classical tableaux with free variables and on-the-fly Skolemization. Soundness proofs are usually built from semantic arguments, and this is to our knowledge, the first proof that appeals to syntactic means. We actually prove the soundness property with respect to cut-free sequent calculus. This requires great care because of the additional liberty in freshness checking allowed by the use of Skolem terms. In contrast to semantic soundness, we gain the possibility to state a cut elimination theorem for sequent calculus, under the proviso that completeness of the method holds. We believe that such techniques can be applied to tableaux in other logics as well.
Type de document :
Pré-publication, Document de travail
Liste complète des métadonnées

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

https://hal-mines-paristech.archives-ouvertes.fr/hal-01154799
Contributeur : Olivier Hermant <>
Soumis le : samedi 23 mai 2015 - 15:34:50
Dernière modification le : jeudi 24 septembre 2020 - 16:00:37
Archivage à long terme le : : jeudi 20 avril 2017 - 08:00:59

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01154799, version 1
  • ARXIV : 1505.06376

Citation

Richard Bonichon, Olivier Hermant. A syntactic soundness proof for free-variable tableaux with on-the-fly Skolemization. 2015. ⟨hal-01154799⟩

Partager

Métriques

Consultations de la notice

465

Téléchargements de fichiers

595