Znn3bq.jpeg
²é¿´: 1776  |  »Ø¸´: 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 µÄÖ÷Ìâ¸üÐÂ
¡î ÎÞÐǼ¶ ¡ï Ò»ÐǼ¶ ¡ï¡ï¡ï ÈýÐǼ¶ ¡ï¡ï¡ï¡ï¡ï ÎåÐǼ¶
×î¾ßÈËÆøÈÈÌûÍÆ¼ö [²é¿´È«²¿] ×÷Õß »Ø/¿´ ×îºó·¢±í
[¿¼ÑÐ] 271Çóµ÷¼Á +21 2261744733 2026-04-11 21/1050 2026-04-11 20:19 by Angchemist
[¿¼ÑÐ] 085410 273·Öµ÷¼Á +4 X1999 2026-04-09 4/200 2026-04-11 13:05 by pies112
[¿¼ÑÐ] 285Çóµ÷¼Á +8 ¶ñ·¨´ó¶þµÄÆøÎ¶ß 2026-04-05 11/550 2026-04-11 11:28 by ×ÏêØ×ÏÆå
[¿¼ÑÐ] Ò»Ö¾Ô¸¾©Çø985£¬085401£¬Óë±¾¿Æ×¨ÒµÒ»Ö£¬µç×ÓÐÅÏ¢¹¤³Ì£¬ +4 Ñô¹â¿ªÀʵÄÄк¢ 2026-04-10 4/200 2026-04-10 18:27 by shenrf
[¿¼ÑÐ] Ò»Ö¾Ô¸¿ó´ó£¬²ÄÁϹ¤³Ìר˶314·Ö£¬0856¿Éµ÷¶¼¿ÉÒÔ +15 ÎÞи¿É»÷µÄ¾ÞÈË 2026-04-09 15/750 2026-04-10 18:10 by hmn_wj
[¿¼ÑÐ] 307Çóµ÷¼Á +8 tzq94092 2026-04-10 8/400 2026-04-10 17:33 by 286640313
[¿¼ÑÐ] 085404 298·ÖÇóµ÷¼Á +10 ºôÀ²ºôÀ²ºôºôºô 2026-04-10 11/550 2026-04-10 16:44 by wangy0907
[¿¼ÑÐ] Ò»Ö¾Ô¸¾©Çø985£¬085401µç×ÓÐÅÏ¢£¬±¾¿Æµç×ÓÐÅÏ¢ +3 Ñô¹â¿ªÀʵÄÄк¢ 2026-04-10 3/150 2026-04-10 16:29 by sophia_93
[¿¼ÑÐ] 070300»¯Ñ§ Çóµ÷¼Á +13 73372112 2026-04-08 13/650 2026-04-09 20:22 by maddjdld
[¿¼ÑÐ] 332£¬085601Çóµ÷¼Á +12 ydfyh 2026-04-09 14/700 2026-04-09 17:28 by wp06
[¿¼ÑÐ] Çóµ÷¼Á²ÄÁÏ¿ÆÑ§Ó빤³ÌÒ»Ö¾Ô¸985³õÊÔ365·Ö +5 ²Ä»¯Àî¿É 2026-04-08 5/250 2026-04-09 17:00 by Lilly_Li
[¿¼ÑÐ] ¸´ÊÔµ÷¼Á£¬Ò»Ö¾Ô¸Ö£ÖÝ´óѧ²ÄÁÏÓ뻯¹¤289·Ö +31 ˶ÐǸ° 2026-04-08 31/1550 2026-04-09 16:54 by Delta2012
[¿¼ÑÐ] ²ÄÁϵ÷¼Á +14 Ò»ÑùYWY 2026-04-05 15/750 2026-04-09 13:36 by ¹ÊÈË??
[¿¼ÑÐ] 0703»¯Ñ§µ÷¼Á 348·Ö +14 °¦ÎÒ³¬ÕæÃ»ÕÐÁË 2026-04-06 15/750 2026-04-08 19:16 by ÎÒ¼õ·Ê1
[¿¼ÑÐ] 264Çóµ÷¼Á +11 ÂóС¶£µ± 2026-04-07 11/550 2026-04-08 16:05 by Ò»Ö»ºÃ¹û×Ó?
[¿¼ÑÐ] Çóµ÷¼Á +15 ÐܶþÏëÉϰ¶ 2026-04-06 15/750 2026-04-08 04:53 by Î޼ʵIJÝÔ­
[¿¼ÑÐ] 319·Ö085702°²È«¹¤³ÌÇóµ÷¼Á +6 rious 2026-04-05 6/300 2026-04-07 09:42 by jp9609
[¿¼ÑÐ] ¹¤¿Æ 22408 267ÇóÍÆ¼ö +4 wanwan00 2026-04-05 5/250 2026-04-06 22:47 by chenzhimin
[¿¼ÑÐ] 297·Ö083200ÇóÖú +9 aekx 2026-04-05 9/450 2026-04-06 20:57 by flysky1234
[¿¼ÑÐ] ¹¤¿Æ277·ÖÇóµ÷¼Á²ÄÁÏ +8 ÉÏÁËÉÏÁËÉÏŶ 2026-04-05 9/450 2026-04-05 13:05 by wwytracy
ÐÅÏ¢Ìáʾ
ÇëÌî´¦ÀíÒâ¼û