collaborators

1 paper

cs.LO2023

Choose your Colour: Tree Interpolation for Quantified Formulas in SMT

Elisabeth Henkel, Jochen Hoenicke, Tanja Schindler

We present a generic tree-interpolation algorithm in the SMT context with quantifiers. The algorithm takes a proof of unsatisfiability using resolution and quantifier instantiation…