This method computes interpolating proofs from propositional LK-proof containing at most atomic cuts. As arguments it expects a proof p and a partition of its end-sequent into two parts: a "negative" part and a "positive" part. For \Gamma |- \Delta being the negative and \Pi |- \Lambda being the positive part, it will compute an interpolant I and proofs of \Gamma |- \Delta, I and I, \Pi |- \Lambda
This method computes interpolating proofs from propositional LK-proof containing at most atomic cuts. As arguments it expects a proof p and a partition of its end-sequent into two parts: a "negative" part and a "positive" part. For \Gamma |- \Delta being the negative and \Pi |- \Lambda being the positive part, it will compute an interpolant I and proofs of \Gamma |- \Delta, I and I, \Pi |- \Lambda
Value parameters
color
indicates which formulas are in the positive part
p
the LK proof from which the interpolant is to be extracted
Attributes
Returns
a triple consisting of ( a proof of \Gamma |- \Delta, I, a proof of I, \Pi |- \Lambda, the FOLFormula I )