We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

math.LO
< prev | next >
new | recent | 2105

Change to browse by:

cs
cs.LO
math

References & Citations

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo

Mathematics > Logic

Title: Induction and Skolemization in saturation theorem proving

Authors: Stefan Hetzl, Jannik Vierling
(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.
Comments: Revised version
Subjects: Logic (math.LO); Logic in Computer Science (cs.LO)
Cite as: arXiv:2105.07734 [math.LO]
  (or arXiv:2105.07734v2 [math.LO] for this version)

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)
Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)

Link back to: arXiv, form interface, contact.