7

The same distinction exists in circuit complexity: tree-like circuits are known as formulas, and it is easier to prove lower bounds for them. For example, there are no superlinear lower bounds for circuits (for explicit functions), but for formulas there is an $\tilde\Omega(n^3)$ average-case lower bound, proved recently by Komargodski, Raz and Tal, ...


7

Unlike the question you threaten for inference rule, this has a nice, simple answer: Robinson (1965) A machine-oriented logic based on the resolution principle. Journal of the ACM. Resolution only applies to a subfragment of FOL, the Horn clauses, that lack disjunction and existential quantification, but combined with Herbrandisation, this is sufficient ...


6

With the caveat that I am posting this quickly in a sleep-deprived state, I think the answer is "no" to all three questions. Take the pigeonhole principle formulas PHP^m_n for m pigeons and n holes. The miniminal length of a resolution refutation for m = n+1 is exp(Omega(n)) by Haken. However, Buss and Pitassi proved that for m = exp(\sqrt(n log n)) pigeons ...


2

Your translation goes into Presburger arithmetic, which is decidable. You could take your translated formula, do quantifier elimination on it, and then hand it over to a proof-producing SMT solver. Since pretty much all SMT solvers are (fancy extensions of) DPLL, I would guess you can turn those proofs into resolution proofs without too much difficulty. ...


1

If I understood correctly the question, the so-called Buss-Pudlak game provides a simple transformation from a proof system to such a decision tree (see Buss-Pudlak '94 http://math.cas.cz/%7Epudlak/howtolie.ps). The queries are formulas (not just variables). The tree is also completely deterministic. Other decision trees that correspond to different ...


Only top voted, non community-wiki answers of a minimum length are eligible