eng
episciences.org
Logical Methods in Computer Science
1860-5974
2020-11-30
Volume 16, Issue 4
10.23638/LMCS-16(4:11)2020
5832
journal article
Clause Set Cycles and Induction
Stefan Hetzl
Jannik Vierling
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.
https://lmcs.episciences.org/5832/pdf
Computer Science - Logic in Computer Science
Mathematics - Logic