Induction and Skolemization in saturation theorem proving

Autor:	Hetzl, Stefan, Vierling, Jannik
Rok vydání:	2021
Předmět:	Mathematics - Logic Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	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. Comment: Revised version
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2105.07734 Zobrazit plný text záznamu View this record from Arxiv