2021/05/17 by Stefan Hetzl, Hetzl, Stefan, Jannik Vierling +1 · 1 citation
Computer Science · #Cryptography and Data Security #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2105.07734
openalex publication_date 2021/05/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We consider a typical integration of induction in saturation-based theorem provers and investigate the effects of Skolem symbols occurring in the induction formulas. In a practically relevant setting we establish a Skolem-free characterization of refutation in saturation-based proof systems with induction. Finally, we use this characterization to obtain unprovability results for a concrete saturation-based induction prover.