Interpolation Tutorial @IITB 2015

Instructor : Ashutosh Gupta

This two-part tutorial presents an interpolation procedure along with proof generation in SMT solvers for the theory of linear rational arithmatic and equality with uninterpreted functions.

Lectures

2015-11-05 : Lecture 1 - Proof generation

• Recall: SMT solving
• CDCL proof generation
• Theory proof generation in LRA and EUF
• Slides

2015-11-06 : Lecture 2 - Interpolants

• Interpolants
• Interpolants in LRA
• Interpolants in propositional logic
• Slides