Induction and Skolemization in saturation theorem proving
Autor: | Hetzl, Stefan, Vierling, Jannik |
---|---|
Rok vydání: | 2021 |
Předmět: | |
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: |