Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Does Z3 Support Craig Interpolation

Tags:

z3

Can Z3 generate Craig interpolants (at least for propositional logic ?). I have not found it in the documentation of Z3.

like image 920
Andreas Morgenstern Avatar asked Oct 10 '22 07:10

Andreas Morgenstern


1 Answers

No, Z3 does not support Craig interpolants, but it generates proofs. The interpolants can be extracted from the proofs. Ken Mcmillan is developing an interpolant generator on top of Z3 using this approach.

like image 182
Leonardo de Moura Avatar answered Oct 18 '22 06:10

Leonardo de Moura