000			03614nam a22004455i 4500
001			978-1-4471-4129-7
003			DE-He213
005			20140220083237.0
007			cr nn 008mamaa
008			120615s2012 xxk| s |||| 0|eng d
020			_a9781447141297 _9978-1-4471-4129-7
024	7		_a10.1007/978-1-4471-4129-7 _2doi
050		4	_aQA8.9-QA10.3
072		7	_aUYA _2bicssc
072		7	_aMAT018000 _2bisacsh
072		7	_aCOM051010 _2bisacsh
082	0	4	_a005.131 _223
100	1		_aBen-Ari, Mordechai. _eauthor.
245	1	0	_aMathematical Logic for Computer Science _h[electronic resource] / _cby Mordechai Ben-Ari.
250			_a3rd ed. 2012.
264		1	_aLondon : _bSpringer London : _bImprint: Springer, _c2012.
300			_aXV, 346 p. 79 illus. _bonline resource.
336			_atext _btxt _2rdacontent
337			_acomputer _bc _2rdamedia
338			_aonline resource _bcr _2rdacarrier
347			_atext file _bPDF _2rda
505	0		_aPreface -- Introduction -- Propositional Logic: Formulas, Models, Tableaux -- Propositional Logic: Deductive Systems -- Propositional Logic: Resolution -- Propositional Logic: Binary Decision Diagrams -- Propositional Logic: SAT Solvers -- First-Order Logic: Formulas, Models, Tableaux -- First-Order Logic: Deductive Systems -- First-Order Logic: Terms and Normal Forms -- First-Order Logic: Resolution -- First-Order Logic: Logic Programming -- First-Order Logic: Undecidability and Model Theory -- Temporal Logic: Formulas, Models, Tableaux -- Temporal Logic: A Deductive System -- Verification of Sequential Programs -- Verification of Concurrent Programs -- Set Theory -- Index of Symbols -- Index of Names -- Subject Index.
520			_aMathematical Logic for Computer Science is a mathematics textbook with theorems and proofs, but the choice of topics has been guided by the needs of students of computer science. The method of semantic tableaux provides an elegant way to teach logic that is both theoretically sound and easy to understand. The uniform use of tableaux-based techniques facilitates learning advanced logical systems based on what the student has learned from elementary systems. The logical systems presented are: propositional logic, first-order logic, resolution and its application to logic programming, Hoare logic for the verification of sequential programs, and linear temporal logic for the verification of concurrent programs. The third edition has been entirely rewritten and includes new chapters on central topics of modern computer science: SAT solvers and model checking. There are 150 exercises with answers available to qualified instructors. Documented, open-source, Prolog source code for the algorithms is available at http://code.google.com/p/mlcs/ Mordechai (Moti) Ben-Ari is with the Department of Science Teaching at the Weizmann Institute of Science. He is a Distinguished Educator of the ACM and has received the ACM/SIGCSE Award for Outstanding Contributions to Computer Science Education. His other textbooks published by Springer are: Ada for Software Engineers (Second Edition) and Principles of the Spin Model Checker.
650		0	_aComputer science.
650		0	_aLogic, Symbolic and mathematical.
650	1	4	_aComputer Science.
650	2	4	_aMathematical Logic and Formal Languages.
650	2	4	_aMathematical Logic and Foundations.
710	2		_aSpringerLink (Online service)
773	0		_tSpringer eBooks
776	0	8	_iPrinted edition: _z9781447141280
856	4	0	_uhttp://dx.doi.org/10.1007/978-1-4471-4129-7
912			_aZDB-2-SCS
999			_c100770 _d100770