2017/05/15 by Jürgen Christ, Christ, Jürgen, Jochen Hoenicke +3
Computer Science · Mathematics · #Algorithm #Artificial intelligence #Combinatorics #Computer science #FOS: Computer and information sciences #Formal Methods in Verification #Integer (computer science) #Interpolation (computer graphics) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Mathematics #Polynomial and algebraic computation #Programming language #Satisfiability modulo theories #Scheme (mathematics) #Solver #Theoretical computer science #Tree (set theory) #cs.LO
paper · pdf · doi:10.48550/arxiv.1705.05309
published in arXiv (Cornell University) (Cornell University) · Improved and simplified version of the paper published in TACAS 2013
arxiv created 2017/05/15 · openalex publication_date 2017/05/15 · arxiv updated 2017/05/16 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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 formulae. In this paper, we present a scheme to compute Craig interpolants in the presence of mixed literals. Contrary to existing approaches, this scheme neither limits the inferences done by the SMT solver, nor does it transform the proof tree before extracting interpolants. Our scheme works for the combination of uninterpreted functions and linear arithmetic but is extendable to other theories. The scheme is implemented in the interpolating SMT solver SMTInterpol.