选择你的颜色：SMT中用于量化公式的树插值
摘要：在SMT环境中，我们提出了一种通用的树插值算法。该算法使用分辨率和量化实例化的不可满足性证明，并计算插值（可能包含量化）。支持任意的SMT理论，只要每个理论本身支持其引理的树插值。特别地，我们展示了对带有未解释函数和线性算术的等式理论组合的支持。通过将证明中的每个文字进行虚拟分配，可以调整插值的效果（对文字进行涂色）。该算法在SMTInterpol中实现。
作者：Elisabeth Henkel, Jochen Hoenicke, Tanja Schindler
论文ID：2305.11667
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-05-22