15 citations · 15 across the 2 of their papers we have counts for
2 papers
cs.LO2019★ 15 cited
Ultimate TreeAutomizer (CHC-COMP Tool Description)
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke +2
We present Ultimate TreeAutomizer, a solver for satisfiability of sets of constrained Horn clauses. Constrained Horn clauses (CHC) are a fragment of first order logic with attracti…
cs.LO2017
Proof Tree Preserving Interpolation
Jürgen Christ, Jochen Hoenicke, Alexander Nutz
Craig interpolation in SMT is difficult because, e. g., theory combination and integer cuts introduce mixed literals, i. e., literals containing local symbols from both input formu…