Cuts in interpolation

[gebner]

import at.logic.gapt.formats.prover9.Prover9TermParserLadrStyle.parseFormula
import at.logic.gapt.proofs.lk.algorithms.ExtractInterpolant
import at.logic.gapt.proofs.lk.base.FSequent
import at.logic.gapt.provers.eqProver.EquationalProver

ExtractInterpolant(FSequent(Seq(), Seq()), FSequent(Seq(
  "m(a3, a3) = a3",
  "m(m(x, a1), a0) = m(a0, m(x, a1))",
  "m(x, a3) = m(a3, x)", "m(a0, a1) = m(a1, a0)",
  "m(a1, a2) = m(a2, a1)",
  "m(m(a3, a2), a1) = m(a1, m(a3, a2))", "m(a3, a0) = m(a0, a3)",
  "m(m(x, a1), a0) = m(x, m(a1, a0))",
  "m(m(a3, x), a1) = m(a3, m(x, a1))",
  "m(m(a3, a2), a0) = m(a3, m(a2, a0))",
  "m(a2, a3) = a2",
  "m(a3, a0) = a3",
  "m(a0, a1) = a0",
  "m(a1, a2) = a1",
  "m(m(a2, a3), a1) = m(a3, m(a2, a1)) & m(a2, m(a1, a0)) = m(a0, m(a2, a1))",
  "m(m(a3, a3), a1) = m(a3, m(a3, a1)) & m(a3, m(a1, a0)) = m(a0, m(a3, a1))") map parseFormula,
  Seq(parseFormula("a0=a1 & a1=a2 & a2=a3"))), new EquationalProver)

fails with

at.logic.gapt.proofs.lk.algorithms.InterpolationException: Unknown inference rule.
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.apply(interpolation.scala:230)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.applyUpUnary(interpolation.scala:236)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.apply(interpolation.scala:72)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.applyUpUnary(interpolation.scala:236)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.apply(interpolation.scala:72)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.applyUpUnary(interpolation.scala:236)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.apply(interpolation.scala:72)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.applyUpUnary(interpolation.scala:236)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.apply(interpolation.scala:72)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.applyUpUnary(interpolation.scala:236)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.apply(interpolation.scala:72)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.applyUpUnary(interpolation.scala:236)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.apply(interpolation.scala:72)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.applyUpUnary(interpolation.scala:236)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.apply(interpolation.scala:72)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.applyUpUnary(interpolation.scala:236)
    at at.logic.gapt.proofs.lk.algorithms.Interpolate$.apply(interpolation.scala:72)
    at at.logic.gapt.proofs.lk.algorithms.ExtractInterpolant$.apply(interpolation.scala:13)
    at at.logic.gapt.proofs.lk.algorithms.ExtractInterpolant$.apply(interpolation.scala:31)

Apparently the proof returned by EquationalProver and passed to Interpolate contains a cut. I tried to apply cut elimination, but apparently that chokes on equation rules:

at.logic.gapt.proofs.lk.algorithms.ReductiveCutElimException: Can't match the case: Cut(EquationRight1RuleType, EquationLeft1RuleType)
    at at.logic.gapt.proofs.lk.algorithms.ReductiveCutElim$.reduceBinaryRight(ReductiveCutElim.scala:446)

[quicquid]

Yes, in general cut-elimination does not work in presence of equality rules. What is possible is to permute the equality rules upwards, such that there is a layer of equational rules working on axioms only, followed by a layer of pure logical reasoning. Then the cut can be pushed out of the logical layer.

[frehn]

I think that our interpolation algorithm can be extended to handle the proofs returned by EquationalProver, i.e. I think it is possible to extend the algorithm to handle equational rules and atomic cuts. It should be possible to adapt the techniques described in Bernhard's master thesis.

[quicquid]

I'm afraid, the link has expired... this one should stay valid: http://permalink.obvsg.at/AC12110884 (B. Mallinger: Interpolation in first-order logic with equality )

[frehn]

Thanks, Martin! Edited my comment with the permalink.

[shetzl]

I have worked out an interpolation algorithm in detail (on paper) which extends the currently implemented one by being able to treat atomic cuts and our equality rules. This algorithm will produce an interpolant which contains only predicate symbols that appear on both sides of the partition. The interpolant may always contain equality-atoms (which is unavoidable) and the constant and function symbols are not restricted in any way (which would require quantified interpolants).

If anybody wants to implement it, let me know.

[seimes]

Thus far, the interpolation algorithm only works if all axioms in the proof are of the form A :- A. Since this was already the case in the previous version, I was wondering whether this behaviour is intended or should the algorithm also be able to handle proofs containing instances of the reflexivity axiom?

This question arose because I tried to test the above example with the new version of the interpolation algorithm.