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

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}{(Id\downarrow)}$$

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

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

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

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

P.S.: I guess I could do the following detour: Define some calculus that does extract proof objects. And then look at the proof objects, and further normalize them. But let's assume that we don't invoke the device of proof objects.

P.S.S.: Here is an example of a cut free proof, in the Gentzen system, that has some noise.

 ------ (Id)  --------- (Id)
 p |- p       q, p |- p
 ---------------------- (L->)
 p -> q, p |- p

It applies the (L->) to p -> q, although the head of p -> q does not match p. The uniform proof, and in this case also shorter proof, would be:

 --------------- (Id)
 p -> q, p |- p

(*) 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

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