7 events
when toggle format what by license comment
Apr 13 '17 at 12:32 history edited CommunityBot
replaced http://cstheory.stackexchange.com/ with https://cstheory.stackexchange.com/
Jan 3 '11 at 6:27 comment added Kaveh Andrej Bauer has a new interesting post on his blog in which he proves Godel's Dialectica Interpretation in Coq.
Jan 2 '11 at 22:33 history edited Kaveh CC BY-SA 2.5
added 389 characters in body
Jan 2 '11 at 22:10 comment added Kaveh @Radu: thanks for pointing out that it can be done automatically in Coq. As you mentioned one can also extract some constructive information and therefore programs from classical proofs of theorem using proof mining for some classes of formulas (interested people can check Ulrich Kuhlenbach's papers for details). Another possibly related result is that if a $\Pi^0_2$ theorem is proven in $PA$, it is also provable constructively in $HA$ by Harvey Friedman's translation. _
Jan 2 '11 at 21:53 comment added Radu GRIGore Nice answer! You mention that one way is to extract programs from proofs, which is something one can do automatically in Coq, for example. A related area is proof mining, where people (working usually in mathematical logic) try to extract information from a given proof. For example, it's possible in some cases to (automatically) find an intuitionistic proof given a classical one.
Jan 2 '11 at 19:43 history edited Kaveh CC BY-SA 2.5
added 963 characters in body; deleted 1 characters in body
Jan 2 '11 at 19:20 history answered Kaveh CC BY-SA 2.5