A Proof-Sensitive Approach for Small Propositional Interpolants

VSTTE, pp. 1-18, 2015.

Cited by: 14|Bibtex|Views6|Links
EI

Abstract:

The labeled interpolation system LIS is a framework for Craig interpolation widely used in propositional-satisfiability-based model checking. Most LIS-based algorithms construct the interpolant from a proof of unsatisfiability and a fixed labeling determined by which part of the propositional formula is being over-approximated. While this...More

Code:

Data:

Your rating :
0

 

Tags
Comments