书目信息

书名： 交互式定理证明与程序开发 
作者： 贝尔托 ， 卡斯特拉 著 ；顾明 译
出版信息： 北京   清华大学出版社  2010
开本页数： 26cm  19, 432页
丛书名： 国外经典教材
单 册：
中图分类： O141-39
科图分类：
主题词： 定理证明--ding li zheng ming--软件工具, Coq--教材
电子资源：
ISBN： 978-7-302-20813-6
000 01534nam 2200313 450
001 0100000683
010    @a978-7-302-20813-6@dCNY59.00
100    @a20091218d2010 em y0chiy50 ea
101 1  @achi@ceng
102    @aCN@b110000
105    @aak a 000yy
106    @ar
200 1  @a交互式定理证明与程序开发@Ajiao hu shi ding li zheng ming yu cheng xu kai fa@eCoq归纳构造演算的艺术@d= Interactive theorem proving and program development@ecoq'art: the calculus of inductive constructions@f贝尔托, 卡斯特拉著@g顾明等译@zeng
210    @a北京@c清华大学出版社@d2010
215    @a19, 432页@c图@d26cm
225 2  @a国外经典教材@Aguo wai jing dian jiao cai@i计算机科学与技术
314    @a责任者汉译姓：贝尔托；卡斯特拉
320    @a有书目 (第[427]-432页)
330    @a本书的主要目标是从实践的角度来理解Coq系统及其基本理论：归纳构造演算。因此，这本书中包含了大量的例子，所有这些例子都可以在计算机上执行。为了教学目的，一些例子解释了错误或笨拙的用法以及避免这些问题的准则。
410  0 @12001 @a国外经典教材@i计算机科学与技术
500 10 @aInteractive theorem proving and program development coq'art: the calculus of inductive constructions@mChinese
517 1  @aCoq归纳构造演算的艺术@ACoq gui na gou zao yan suan de yi shu
606 0  @a定理证明@Ading li zheng ming@x软件工具, Coq@j教材
690    @aO141-39@v4
701  1 @a贝尔托@Abei er tuo@g(Bertot, Yves)@4著
701  1 @a卡斯特拉@Aka si te la@g(Casteran, Pierre)@4著
702  0 @a顾明@Agu ming@4译
801  0 @aCN@c20100602
905    @b21002531-33@dO141-39@eB675
    
    交互式定理证明与程序开发：Coq归纳构造演算的艺术= Interactive theorem proving and program development：coq'art: the calculus of inductive constructions/贝尔托, 卡斯特拉著/顾明等译.-北京：清华大学出版社，2010
    19, 432页：图；26cm.-(国外经典教材.计算机科学与技术)
    
    
    ISBN 978-7-302-20813-6：CNY59.00
    本书的主要目标是从实践的角度来理解Coq系统及其基本理论：归纳构造演算。因此，这本书中包含了大量的例子，所有这些例子都可以在计算机上执行。为了教学目的，一些例子解释了错误或笨拙的用法以及避免这些问题的准则。
●
相关链接
在五车中查询图书 在当当中查询图书 在豆瓣中查询图书


正题名：交互式定理证明与程序开发     索取号：O141-39/B675         预约/预借

序号 登录号 条形码 馆藏地/架位号 状态 备注
1 1002531   210025319   自科库401/401自科库 40排2列5层/ [索取号:O141-39/B675] 在馆    
2 1002532   210025328   自科库401/401自科库 40排2列5层/ [索取号:O141-39/B675] 在馆    
3 1002533   210025337   自科库401/401自科库 40排2列5层/ [索取号:O141-39/B675] 在馆