2 citations · 2 across the 4 of their papers we have counts for
4 papers
Quantifier-free induction for lists
Stefan Hetzl, Jannik Vierling
We investigate quantifier-free induction for Lisp-like lists constructed inductively from the empty list and the operation , that adds an element to t…
Unprovability results for clause set cycles
Stefan Hetzl, Jannik Vierling
The notion of clause set cycle abstracts a family of methods for automated inductive theorem proving based on the detection of cyclic dependencies between clause sets. By discernin…
Induction and Skolemization in saturation theorem proving
Stefan Hetzl, Jannik Vierling
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 practical…
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 t…