About NLFIntp
Interpolation-based technique provides a powerful mechanism for local and modular reasoning, thus improving scalability of logic synthesis as well as various verification techniques, e.g. theorem proving, model checking and abstract interpretation, to name just a few.
The tool NLFIntp is dedicated to synthesizing (reverse) Craig interpolants for the quantifier-free theory
of nonlinear arithmetic and the equality theory over uninterpreted function symbols (EUF).
It takes as input a pair (φ, ψ) of mutually contradictory formulas over the reals, and generates an interpolant I
for (φ, ψ) in polynomial time.
NLFIntp consists of two components for synthesizing nonlinear interpolants. The first one is for conjunctions of
the conjunctive theory of concave quadratic polynomial inequalities and EUF. This is achieved
on account of a key observation that this theory can be linearized by showing a generalization of Motzkin's transposition theorem,
which yields an equivalent reduction of the interpolation problem to semi-definite programming (SDP).
The second is for general nonlinear polynomial inequalities (where φ and ψ share an identical set of variables),
based on the existence of a witness guaranteed by Stengle's Positivstellensatz that can be computed using SDP.
About the website
This online interface was created for an easy way of using the interpolant synthesizer that runs remotely on the cloud, thus avoiding compilation and installation, as well as potential issues e.g. compatibility and portability.
The style of the website is highly inspired by Diffchecker @ https://www.diffchecker.com.