10.23638/LMCS-16(4:11)2020
https://lmcs.episciences.org/5832
Hetzl, Stefan
Stefan
Hetzl
Vierling, Jannik
Jannik
Vierling
Clause Set Cycles and Induction
In this article we relate a family of methods for automated inductive theorem
proving based on cycle detection in saturation-based provers to well-known
theories of induction. To this end we introduce the notion of clause set cycles
-- a formalism abstracting a certain type of cyclic dependency between clause
sets. We first show that the formalism of clause set cycles is contained in the
theory of $\exists_1$ induction. Secondly we consider the relation between
clause set cycles and the theory of open induction. By providing a finite
axiomatization of a theory of triangular numbers with open induction we show
that the formalism of clause set cycles is not contained in the theory of open
induction. Furthermore we conjecture that open induction and clause set cycles
are incomparable. Finally, we transfer these results to a concrete method of
automated inductive theorem proving called the n-clause calculus.
episciences.org
Computer Science - Logic in Computer Science
Mathematics - Logic
Attribution 4.0 International (CC BY 4.0)
2020-10-04
2020-11-30
2020-11-30
eng
journal article
arXiv:1910.03917
10.48550/arXiv.1910.03917
1860-5974
10.48550/arxiv.1910.03917
https://lmcs.episciences.org/5832/pdf
VoR
application/pdf
Logical Methods in Computer Science
Volume 16, Issue 4
Researchers
Students