Re:Trivial observation on resolution

Hello,

my intention is not to devise a faster method than resolution, nor to 
invent anything new in that area, and even less so to prove that NP = 
coNP.

What Paola and I are investigating is the performance of deep 
inference wrt proof complexity. So, we show how many formalisms 
(Frege, extended Frege, sequent, tableaux, resolution, ...) can be 
directly expressed in CoS system SKS without complexity penalty, and 
especially so in the cut-free fragment KS, for obvious reasons of 
analyticity. Having established that CoS performs as good as the 
others, we then show that in many cases it has speed-ups over the 
other methods.

One of the conclusions is that CoS has a complexity advantage over 
other formalisms like the sequent calculus. For example, it is 
well-known how to express resolution in the sequent calculus by using 
cut, but you cannot do so without the cut unless you pay for cut 
elimination. In KS, we don't have to pay this exponential price.

Regarding doing resolution on generic formulae: yes, there are tens 
of methods that do so, but most of them are heavily algorithmic. With 
this, I mean that they rely on complex data structures which look 
completely outside of the reach of simple proof theoretic methods 
like those we are interested in. In fact, their mutual relationship 
in terms of complexity is largely unknown and unexplored, due to the 
technical difficulty of dealing with complex structures.

I guess Steffen has in mind Tseitin's extension method (which I think 
Eder extended to predicate logic). In this case, the trick is to 
introduce new propositional variables to stand for subformulae. The 
problem with this method is that introducing new variables 
corresponds to using a cut rule, so, again, one has to give up 
analyticity, which we don't want to do.

If anybody knows of a simple generalisation of resolution, which 
speeds it up, and which doesn't involve using cut rules, then please 
let us know. By simple, I mean something that involves using formulae 
which can be simply generated by a small number of normal inference 
rules.

-Alessio


At 17:34 +1100 20.1.05, Rajeev.Gore-/hejbHI7ObxcYUQs2IXCwA@xxxxxxxxxxxxxxxx 
wrote:
> I recall a paper by Arnon Avron where he shows that propositional
> resolution is just a sequent calculus where the only rule is cut. I
> could be wrong in my recollections so please take this with a grain of
> salt. Would this not count as prior art for your idea ?
>
> Arnon: are you listening ?
>
> Roy: does this ring a bell with you ?

At 9:28 +0000 20.1.05, David Pym wrote:
>  > resolution is just a sequent calculus where the only rule is cut.
>
> This is completely standard knowledge in proof theory.

At 12:13 +0100 20.1.05, Steffen Hoelldobler wrote:
> you don't have to normalize formulas in order to apply resolution; 
> this is well-known.
> Normalization in the way I present it in my lectures may lead to an 
> exponential explosion; this is also well-known. There are other 
> normalization methods thanks to Eder, which avoid this explosion. 
> All this is mentioned in my Logic-book.