Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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.
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Olivier Hermant Connect in order to contact the contributor
Submitted on : Saturday, May 23, 2015 - 3:34:50 PM
Last modification on : Wednesday, November 17, 2021 - 12:33:00 PM
Long-term archiving on: : Thursday, April 20, 2017 - 8:00:59 AM


Files produced by the author(s)


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


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



Record views


Files downloads