Induction and Skolemization in saturation theorem proving
Logic
2022-08-09 v2 Logic in Computer Science
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.
Cite
@article{arxiv.2105.07734,
title = {Induction and Skolemization in saturation theorem proving},
author = {Stefan Hetzl and Jannik Vierling},
journal= {arXiv preprint arXiv:2105.07734},
year = {2022}
}
Comments
Revised version