Return to Question

added 65 characters in body

view source

edited May 29 2011 at 12:56

Countably Infinite

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

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

${\Gamma ${\Gamma \vdash A\quad \quad\Delta \vdash B \downarrow P } \over {\Gamma, \Gamma, \Delta \vdash A \rightarrow B \downarrow P}$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

edited title

edited May 25 2011 at 9:35

Countably Infinite

How establish that conversion of cut-free proof into uniform proofs existproof?

deleted 648 characters in body

view source

edited May 24 2011 at 21:25

Countably Infinite

Dear All

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

added 42 characters in body

view source

edited May 24 2011 at 19:46

Countably Infinite

Dear All

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 a 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.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

added 478 characters in body; added 8 characters in body; added 4 characters in body

view source

edited May 24 2011 at 19:40

Countably Infinite

Dear All

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 a relationship between cut-free proofs and uniform proofs:

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

Best Regards

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

added 412 characters in body; added 26 characters in body

view source

edited May 23 2011 at 23:29

Countably Infinite

view source

asked May 23 2011 at 18:03

Countably Infinite

Return to Question

How establish that conversion of cut-free proof into uniform proofs existproof?

How establish that uniform proofs exist?