7 citations · 23 across the 18 of their papers we have counts for
Showing 2021Show all
3 papers · 1 filter
cs.LO2021
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…
cs.LO2021★ 3 cited
A Fixed-point Theorem for Horn Formula Equations
Stefan Hetzl, Johannes Kloibhofer
We consider constrained Horn clause solving from the more general point of view of solving formula equations. Constrained Horn clauses correspond to the subclass of Horn formula eq…
math.LO2021
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…