Logic and computation : interactive proof with Cambridge LCF

＜図書＞
Logic and computation : interactive proof with Cambridge LCF

責任表示	Lawrence C. Paulson
シリーズ	Cambridge tracts in theoretical computer science ; 2
データ種別	図書
出版情報	Cambridge : Cambridge University Press , 1990, c1987
本文言語	英語
大きさ	xiii, 302 p. : ill. ; 25 cm
概要	This book is concerned with techniques for formal theorem-proving, with particular reference to Cambridge LCF (Logic for Computable Functions). Cambridge LCF is a computer program for reasoning about ...omputation. It combines the methods of mathematical logic with domain theory, the basis of the denotational approach to specifying the meaning of program statements. Cambridge LCF is based on an earlier theorem-proving system, Edinburgh LCF, which introduced a design that gives the user flexibility to use and extend the system. A goal of this book is to explain the design, which has been adopted in several other systems. The book consists of two parts. Part I outlines the mathematical preliminaries, elementary logic and domain theory, and explains them at an intuitive level, giving reference to more advanced reading; Part II provides sufficient detail to serve as a reference manual for Cambridge LCF. It will also be a useful guide for implementors of other programs based on the LCF approach.続きを見る

状態	巻次	所蔵場所	請求記号	刷年	文庫名称	資料番号	コメント	予約・取寄	複写申込	自動書庫
		中央図 2B	549.9/P 28/1	1990		068582190012407		予約・取寄			予約・取寄
		理系図自動書庫	007.63/P 28	1990		068252190009441		予約・取寄		出庫可能	予約・取寄		出庫可能

一般注記	"First paperback edition 1990" -- t.p. verso Bibliography: p. 289-295 Includes index
著者標目	*Paulson, Lawrence C.
件　名	LCSH:Cambridge LCF (Computer system) LCSH:Computable functions -- Data processing 全ての件名で検索
分　類	LCC:QA9.59 DC19:005.1
書誌ID	1001344358
ISBN	0521395607
NCID	BA29634901
巻冊次	: pbk ; ISBN:0521395607
登録日	2009.09.18
更新日	2009.09.18