2015/05/23 by Richard Bonichon, Bonichon, Richard, Olivier Hermant +1 · 1 citation
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.FL #cs.LO
paper · pdf · doi:10.48550/arxiv.1505.06376
arxiv created 2015/05/23 · openalex publication_date 2015/05/23 · arxiv updated 2015/05/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.