Induction and Skolemization in saturation theorem proving
Stefan Hetzl, Jannik Vierling
TL;DR
This paper explores how induction and Skolem symbols interact in saturation theorem proving, providing a Skolem-free characterization of refutation and demonstrating unprovability results for certain provers.
Contribution
It introduces a Skolem-free characterization of refutation in saturation-based systems with induction, advancing understanding of their limitations.
Findings
Skolem symbols impact induction in saturation theorem proving
A Skolem-free characterization of refutation is established
Unprovability results are demonstrated for a specific prover
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Cryptography and Data Security · Logic, programming, and type systems