000			02766cam a22003494a 4500
001			0000028550
005			20230921140048.0
008			040407s2004 enkm b a001 0 eng
010			_a2004045921
020			_a052154310X (pbk.) : _c$85.98
020			_a9780521543101 (pbk.) :
035			_a54960031
050	0	0	_aQA 76.9 .L63 _bH88 2004
100	1		_aHuth, Michael, _d1962-.
245	1	0	_aLogic in computer science : _bmodelling and reasoning about systems / _cMichael Huth, Mark Ryan.
250			_asecond edition.
260			_aCambridge [U.K.] ; _aNew York : _bCambridge University Press, _c2004.
264			_aCambridge [U.K.] ; _bCambridge University Press, _c2004
300			_axiv, 427 pages : _billustrations ; _c25 cm.
504			_aIncludes bibliographical references (p. 414-417) and index.
505	0	0	_g1. _tPropositional logic -- _g2. _tPredicate logic -- _g3. _tVerification by model checking -- _g4. _tProgram verification -- _g5. _tModal logics and agents -- _g6. _tBinary decision diagrams.
520	1		_a"Recent years have seen the development of powerful tools for verifying hardware and software systems, as companies worldwide realise the need for improved means of validating their products. There is increasing demand for training in basic methods in formal reasoning so that students can gain proficiency in logic-based verification methods. At the same time, the shift towards internet-based distributed computing creates the need for individuals who are able to reason about sophisticated autonomous agent-oriented software acting on large networks.".
520	8		_a"The second edition of this successful textbook addresses both those requirements, by continuing to provide an introduction to formal reasoning that is both relevant to the needs of modern computer science and rigorous enough for practical application. The presentation is clear and simple, with core material being described early in the book, and further technicalities introduced only where they are needed by the applications. A key feature is the full exposition of model-checking, and the new edition supports the most up-to--date versions of the tools NuSMV and Alloy.
520	8		_aImprovements to the first edition have been made throughout, with extra and expanded sections on linear-time temporal logic model checking, SAT solvers, second-order logic, the Alloy specification tool, and programming by contract. The coverage of model-checking has been substantially updated. Further exercises have been added."--BOOK JACKET.
650		0	_aComputer logic.
650		0	_aLogic programming.
700	1		_aRyan, Mark, _d1962-.
908			_a151027
913			_aN
989		7	_a20230822095114.0
999			_c14851 _d14851