Re: Deeper Cuts in Deep Inference

Hello,

At 21:46 -0300 16/3/11, Bruno Woltzenlogel Paleo wrote:
>  > It's perhaps interesting to note that all the=20
>bureaucracy disappears when one turns to atomic=20
>flows [1]: all these rules generate the same=20
>atomic flows. However, we are still far from=20
>being able to use atomic flows for proof search=20
>(it's an open problem whether atomic flows are a=20
>proof system).

To clarify: the problem is whether an atomic flow=20
and a formula taken as its conclusion, together=20
with the association between edges in the flow=20
and atom occurrences in the formula, could be=20
tested in polynomial time such that the test=20
decides if the formula is a tautology.

In other words, the object would be a=20
Lamarche-Strassburger proof net with enriched=20
identity links, and the problem is to find a=20
polynomial-time correctness criterion for it.

>What are the arguments in favor of conjecturing that it is a proof system?

1) The flows extracted from proofs have the same=20
asymptotic size modulo polynomials (this is a=20
fact, the easy paper has been in progress for=20
four years but will finally see the light very=20
soon).

2) In similar situations in linear proof nets=20
polynomial correctness criteria exist.

3) No counterexample emerged yet (but I don't=20
know how much effort has been put into this, I=20
didn't work on it much myself).

>And what are the arguments against?

I can't think of any, but I don't understand=20
atomic flows very well, so perhaps I'm missing=20
something obvious.

>Anyway, being a proof system would only mean=20
>that its proofs could be checked in polynomial=20
>time. Proof search could still be very hard=20
>(i.e. if the proof system is not=20
>automatizable...)...

Yes, but I think that looking at the proof-search=20
problem from a radically different angle than the=20
usual one is potentially very fruitful. Flows=20
reduce proofs to purely topological objects, so=20
they get rid of quite a lot of syntactic chaff,=20
and they might help designing proof searchers=20
that just have to consider the only really worthy=20
matching configurations of atoms, instead of=20
pumping around atoms blindly.

>Are there deep inference proof systems that are=20
>as close as possible to natural deduction? I=20
>know the system of Kai Br=FCnnler and Richard=20
>McKinley. Are there others?

I don't know, but you can design your own,=20
depending on the properties you're after.

Ciao

-Alessio