Dear All

Gentzen (*) claimed that through cut-elimination, he can normalize proofs. It is well known that cut-eliminated proofs might still contain some unnecessary noise. I am trying to show that cut-eliminated proofs can be further converted into so called uniform proofs. Uniform proofs are not only cut-eliminated, but also focused.

Focused proofs are currently actively researched. Chaudhuri (**) shows for example some good behaviour in planning problems formulated with linear logic.

I am currently working with minimal logic and horn clauses. I am using the following helper derivation, which should model the clause picking and makes up the focusing:

${}\over{\vdash P \downarrow P}$

${\Gamma \vdash A[x/t] \downarrow P} \over {\Gamma \vdash \forall x A \downarrow P}$

${\Gamma \vdash A\quad \quad\Delta \vdash B \downarrow P} \over {\Gamma, \Delta \vdash A \rightarrow B \downarrow P}$

I am stuck with the following lemma, which establishes some preliminary relationship between cut-free proofs and uniform proofs. P denotes a prime formula:

If $\Gamma \vdash P$ then $\Gamma' \vdash A \downarrow P$ for some $A$ in $\Gamma$ and some $\Gamma'$ subset $\Gamma$

Best Regards

(*) Gerhard Genzen, "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift 39 (2): 176–210. 1934. http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375508.

(**) Kaustuv Chaudhuri, "The Focused Inverse Method for Linear Logic", Thesis, Carnegie Mellon University Pittsburgh, 2006. http://reports-archive.adm.cs.cmu.edu/anon/2006/CMU-CS-06-162.pdf