Current browse context:
cs.LO
Change to browse by:
References & Citations
Mathematics > Logic
Title: Induction and Skolemization in saturation theorem proving
(Submitted on 17 May 2021 (v1), last revised 8 Aug 2022 (this version, v2))
Abstract: 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.
Submission history
From: Jannik Vierling [view email][v1] Mon, 17 May 2021 11:06:16 GMT (38kb)
[v2] Mon, 8 Aug 2022 14:21:41 GMT (42kb)
Link back to: arXiv, form interface, contact.