Znn3bq.jpeg
ÉÇÍ·´óѧº£Ñó¿ÆÑ§½ÓÊܵ÷¼Á
²é¿´: 1778  |  »Ø¸´: 31
¡¾½±Àø¡¿ ±¾Ìû±»ÆÀ¼Û30´Î£¬×÷Õßstar_zhangÔö¼Ó½ð±Ò 23.6 ¸ö

[×ÊÔ´] ¡¾Ó¢ÃÀ¾­µä½Ì²Ä¡¿¡¶Proofs and Computations¡·¡¾ÒÑËÑË÷£¬ÎÞÖØ¸´¡¿

¡¾Ó¢ÃÀ¾­µä½Ì²Ä¡¿¡¶Proofs and Computations¡·¡¾ÒÑËÑË÷£¬ÎÞÖØ¸´¡¿


ÎÒµÄÕâ±¾Ê飺
×÷ÕߣºHelmut Schwichtenberg, Stanley S. Wainer
2012Ä꣬480 Ò³£¬PDF£¬2.8 MB¡£
Language: English

.
·âÃæ£º
¡£
¡¾Ó¢ÃÀ¾­µä½Ì²Ä¡¿¡¶Proofs and Computations¡·¡¾ÒÑËÑË÷£¬ÎÞÖØ¸´¡¿
¡£
¼ò½é£º
Driven by the question, 'What is the computational content of a (formal) proof?', this book studies fundamental interactions between proof theory and computability. It provides a unique self-contained text for advanced students and researchers in mathematical logic and computer science. Part I covers basic proof theory, computability and Gödel's theorems. Part II studies and classifies provable recursion in classical systems, from fragments of Peano arithmetic up to ¦°11-CA0. Ordinal analysis and the (Schwichtenberg-Wainer) subrecursive hierarchies play a central role and are used in proving the 'modified finite Ramsey' and 'extended Kruskal' independence results for PA and ¦°11-CA0. Part III develops the theoretical underpinnings of the first author's proof assistant MINLOG. Three chapters cover higher-type computability via information systems, a constructive theory TCF of computable functionals, realizability, Dialectica interpretation, computationally significant quantifiers and connectives and polytime complexity in a two-sorted, higher-type arithmetic with linear logic.

==========================================

¾´Çë¸÷λÅóÓÑ£¬ÏÂÔØÖ®ºó£¬¸ø¸ö»ØÌûÆÀ¼Û¡£ÎÒÒ²ºÃ¼ÌÐøÍÆ³öÏÂÒ»¸ö×îпƼ¼Êé¼®¡£
(²»ÏÂÔØ£¬Ò²¿ÉÒÔÆÀ¼Û¡£)
лл£¡
»Ø¸´´ËÂ¥

» ±¾Ìû¸½¼þ×ÊÔ´Áбí

  • »¶Ó­¼à¶½ºÍ·´À¡£ºÐ¡Ä¾³æ½öÌṩ½»Á÷ƽ̨£¬²»¶Ô¸ÃÄÚÈݸºÔð¡£
    ±¾ÄÚÈÝÓÉÓû§×ÔÖ÷·¢²¼£¬Èç¹ûÆäÄÚÈÝÉæ¼°µ½ÖªÊ¶²úȨÎÊÌ⣬ÆäÔðÈÎÔÚÓÚÓû§±¾ÈË£¬Èç¶Ô°æÈ¨ÓÐÒìÒ飬ÇëÁªÏµÓÊÏ䣺xiaomuchong@tal.com
  • ¸½¼þ 1 : Proofs_and_Computations_2012.pdf
  • 2014-06-25 03:20:15, 3.67 M

» ÊÕ¼±¾ÌûµÄÌÔÌûר¼­ÍƼö

רҵÊé¼®£¨ÍâÎİ棩WM ºÃÊ飡 Êé¼®

» ²ÂÄãϲ»¶

ÒÑÔÄ   »Ø¸´´ËÂ¥   ¹Ø×¢TA ¸øTA·¢ÏûÏ¢ ËÍTAºì»¨ TAµÄ»ØÌû

ypcainiao

ľ³æ (ÕýʽдÊÖ)


¡ï¡ï¡ï¡ï¡ï ÎåÐǼ¶,ÓÅÐãÍÆ¼ö

лл¥Ö÷µÄÐÁÇÚ¹¤×÷£¬¶ÔÎÒÃǰïÖúºÜ´ó
13Â¥2014-06-26 15:59:46
ÒÑÔÄ   »Ø¸´´ËÂ¥   ¹Ø×¢TA ¸øTA·¢ÏûÏ¢ ËÍTAºì»¨ TAµÄ»ØÌû

neugena

ľ³æ (ÕýʽдÊÖ)


¡ï¡ï¡ï¡ï¡ï ÎåÐǼ¶,ÓÅÐãÍÆ¼ö

¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
ºÜºÃлл
15Â¥2014-06-26 17:55:26
ÒÑÔÄ   »Ø¸´´ËÂ¥   ¹Ø×¢TA ¸øTA·¢ÏûÏ¢ ËÍTAºì»¨ TAµÄ»ØÌû
¼òµ¥»Ø¸´
hainangod2Â¥
2014-06-25 04:14   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡ [ ·¢×ÔÊÖ»ú°æ http://muchong.com/3g ]
konexgsp3Â¥
2014-06-25 08:24   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
2014-06-25 08:32   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
alazong5Â¥
2014-06-25 10:01   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
supervb6Â¥
2014-06-25 14:12   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
22620066477Â¥
2014-06-25 14:26   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
2014-06-26 09:08   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
2014-06-26 10:14   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
lantianbihb10Â¥
2014-06-26 12:38   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
springcxliu11Â¥
2014-06-26 12:40   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
qzma12Â¥
2014-06-26 13:57   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
meixiangling14Â¥
2014-06-26 16:33   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
lanlandeyue16Â¥
2014-06-26 18:06   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
qqchun17Â¥
2014-06-26 18:16   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
httpftp18Â¥
2014-06-26 22:46   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
baiplf19Â¥
2014-06-27 06:36   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
yinxzy20Â¥
2014-06-27 16:09   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
Jeffreyak21Â¥
2014-06-27 18:37   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
jh0522Â¥
2014-06-27 23:19   »Ø¸´  
ÈýÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
anmingkang23Â¥
2014-06-28 08:13   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
sunbin_bsu24Â¥
2014-07-01 05:36   »Ø¸´  
ÈýÐÇºÃÆÀ  ¸Ðл·ÖÏí£¡
locustzhang25Â¥
2014-07-01 07:28   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
peteryoung26Â¥
2014-07-01 09:03   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
yumujj27Â¥
2014-07-01 19:41   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
httpftp28Â¥
2014-08-11 11:51   »Ø¸´  
¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
zhengj198029Â¥
2016-05-07 22:10   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
guli052030Â¥
2016-05-08 20:36   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
hwjok31Â¥
2016-05-08 20:48   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
void41432Â¥
2016-05-13 15:16   »Ø¸´  
ÎåÐÇºÃÆÀ  ¶¥Ò»Ï£¬¸Ðл·ÖÏí£¡
Ïà¹Ø°æ¿éÌø×ª ÎÒÒª¶©ÔÄÂ¥Ö÷ star_zhang µÄÖ÷Ìâ¸üÐÂ
¡î ÎÞÐǼ¶ ¡ï Ò»ÐǼ¶ ¡ï¡ï¡ï ÈýÐǼ¶ ¡ï¡ï¡ï¡ï¡ï ÎåÐǼ¶
×î¾ßÈËÆøÈÈÌûÍÆ¼ö [²é¿´È«²¿] ×÷Õß »Ø/¿´ ×îºó·¢±í
[¿¼ÑÐ] 211±¾¿Æ²ÄÁÏ»¯¹¤Çóµ÷¼Á +19 YHLAH 2026-04-11 23/1150 2026-04-14 22:25 by fenglj492
[¿¼ÑÐ] ²ÄÁϹ¤³Ì281»¹Óе÷¼Á»ú»áÂð +41 xaw. 2026-04-11 42/2100 2026-04-14 20:05 by honglizhao
[¿¼ÑÐ] Ò»Ö¾Ô¸211£¬»¯Ñ§310·Ö£¬±¾¿ÆÖصãË«·Ç£¬Çóµ÷¼Á +24 ŬÁ¦·Ü¶·112 2026-04-08 24/1200 2026-04-14 18:02 by lhj2009
[¿¼ÑÐ] 291·Öµ÷¼Á +6 Éϰ¶Ð¡Ó¨¼ÓÓÍ 2026-04-09 7/350 2026-04-14 17:58 by lhj2009
[¿¼ÑÐ] ²ÄÁÏÀà284µ÷¼Á +41 Ïë»»ÊÖ»ú²»Ïë½âÊ 2026-04-08 49/2450 2026-04-14 17:53 by lhj2009
[¿¼ÑÐ] »¯¹¤Ñ§Ë¶294·Ö£¬Çóµ¼Ê¦ÊÕÁô +32 yzyzx 2026-04-12 36/1800 2026-04-14 17:45 by lhj2009
[¿¼ÑÐ] 26ҩѧר˶105500Çóµ÷¼Á +6 à¶¹þ¼ÓÓÍ 2026-04-13 6/300 2026-04-14 16:40 by zhouxiaoyu
[¿¼ÑÐ] 297£¬¹¤¿Æµ÷¼Á?ºÓÄÏũҵ´óѧ±¾¿Æ +9 ºÓÄÏũҵ´óѧ-ÄÜ 2026-04-14 9/450 2026-04-14 16:03 by Art1977
[¿¼ÑÐ] »úе»¹Óл¹ÓÐÃû¶îÂð£¿Ì«ÄÑÁË +8 ЦЦԬ 2026-04-10 8/400 2026-04-14 08:44 by screening
[¿¼ÑÐ] 297¹¤¿Æ£¬Çóµ÷¼Á? +13 ºÓÄÏũҵ´óѧ-ÄÜ 2026-04-12 13/650 2026-04-13 14:12 by dingyanbo1
[¿¼ÑÐ] 295·ÖÇóµ÷¼Á +13 ?ÒªÉϰ¶? 2026-04-10 13/650 2026-04-12 15:37 by laoshidan
[¿¼ÑÐ] ¹¤¿Æ273µ÷¼Á +6 X1999 2026-04-09 7/350 2026-04-11 10:23 by zhq0425
[¿¼ÑÐ] Ò»Ö¾Ô¸985»úеѧ˶380Çóµ÷¼Á +5 ¹Ø¹ØöÂð¯10 2026-04-11 5/250 2026-04-11 10:10 by ÖªÄî¡£A
[¿¼ÑÐ] 297Çóµ÷¼Á +9 Kwgyz 2026-04-09 9/450 2026-04-11 10:09 by zhq0425
[¿¼ÑÐ] 22408 352·ÖÇóµ÷¼Á0854Àà +4 ŬÁ¦µÄÏÄÄ© 2026-04-09 4/200 2026-04-11 09:57 by zhq0425
[¿¼ÑÐ] 368Çóµ÷¼Á +3 17385968172 2026-04-10 3/150 2026-04-10 20:12 by µç×Ӱµ±ë
[¿¼ÑÐ] 314Çóµ÷¼Á +14 weltZeng 2026-04-09 14/700 2026-04-09 23:14 by wolf97
[¿¼ÑÐ] Çóµ÷¼Á²ÄÁÏ¿ÆÑ§Ó빤³ÌÒ»Ö¾Ô¸985³õÊÔ365·Ö +5 ²Ä»¯Àî¿É 2026-04-08 5/250 2026-04-09 17:00 by Lilly_Li
[¿¼ÑÐ] 311Çóµ÷¼Á +6 surte 2026-04-08 13/650 2026-04-09 14:00 by surte
[¿¼ÑÐ] 286Çóµ÷¼Á +19 Faune 2026-04-08 20/1000 2026-04-09 08:36 by ŶŶ123
ÐÅÏ¢Ìáʾ
ÇëÌî´¦ÀíÒâ¼û