Instantiation-Based Interpolation for Quantified Formulae in CSIsat
The paper describes an implementation of instantiation-based Craig interpolation for quantified formulae. The implementation is based on the CSIsat interpolating solver. The tool supports interpolation for formulae with linear real arithmetic, uninterpreted functions and quantifiers. The paper sugge...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Series: | Труды Института системного программирования РАН |
| Subjects: | |
| Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/1016 |