000 02369nam a22003738i 4500
001 CR9780511526602
003 UkCbUP
005 20200124160235.0
006 m|||||o||d||||||||
007 cr||||||||||||
008 090407s1987||||enk o ||1 0|eng|d
020 _a9780511526602 (ebook)
020 _z9780521346320 (hardback)
020 _z9780521395601 (paperback)
040 _aUkCbUP
_beng
_erda
_cUkCbUP
050 0 0 _aQA9.59
_b.P38 1987
082 0 0 _a005.1
_219
100 1 _aPaulson, Lawrence C.,
_eauthor.
245 1 0 _aLogic and computation :
_binteractive proof with Cambridge LCF /
_cLawrence C. Paulson.
246 3 _aLogic & Computation
264 1 _aCambridge :
_bCambridge University Press,
_c1987.
300 _a1 online resource (xiii, 302 pages) :
_bdigital, PDF file(s).
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
490 1 _aCambridge tracts in theoretical computer science ;
_v2
500 _aTitle from publisher's bibliographic system (viewed on 05 Oct 2015).
520 _aThis 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 computation. 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.
650 0 _aCambridge LCF (Computer system)
650 0 _aComputable functions
_xData processing.
776 0 8 _iPrint version:
_z9780521346320
830 0 _aCambridge tracts in theoretical computer science ;
_v2.
856 4 0 _uhttps://doi.org/10.1017/CBO9780511526602
999 _c518047
_d518045