Vierling, J. (2018). Zyklische Superposition und Induktion [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.51282
In 2013 Kersani and Peltier introduced the n-clause calculus, a superposition calculus enriched with a cycle detection rule realizing a form of reasoning by mathematical induction. Until now it is not known which form of induction is captured by the n-clause calculus. An upper bound in terms of the quantifier complexity of the induction invariant can be obtained by a two step translation: in a first step we encode cyclic refutations in a cyclic sequent calculus introduced by Brotherston and Simpson in 2010; in a second step we translate cyclic proofs into inductive LK proofs.
