Logic in Computer Science
Námskeið
- T-505-ROKF Rökfræði í tölvunarfræði
Ensk lýsing:
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. The second edition of this successful textbook addresses both those requirements, by continuing to provide a clear introduction to formal reasoning which is both relevant to the needs of modern computer science and rigorous enough for practical application.
Improvements to the first edition have been made throughout, with extra and expanded sections on SAT solvers, existential/universal second-order logic, micro-models, programming by contract and total correctness. The coverage of model-checking has been substantially updated. Further exercises have been added. Internet support for the book includes worked solutions for all exercises for teachers, and model solutions to some exercises for students.
Lýsing:
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. The second edition of this successful textbook addresses both those requirements, by continuing to provide a clear introduction to formal reasoning which is both relevant to the needs of modern computer science and rigorous enough for practical application.
Improvements to the first edition have been made throughout, with extra and expanded sections on SAT solvers, existential/universal second-order logic, micro-models, programming by contract and total correctness. The coverage of model-checking has been substantially updated. Further exercises have been added. Internet support for the book includes worked solutions for all exercises for teachers, and model solutions to some exercises for students.
Annað
- Höfundar: Michael Huth, Mark Ryan
- Útgáfa:2
- Útgáfudagur: 26-08-2004
- Hægt að prenta út 5 bls.
- Hægt að afrita 5 bls.
- Format:ePub
- ISBN 13: 9781139636131
- Print ISBN: 9780521543101
- ISBN 10: 1139636138
Efnisyfirlit
- Cover
- Half Title
- Title Page
- Copyright
- Contents
- Foreword to the first edition
- Preface to the second edition
- Acknowledgements
- 1. Propositional logic
- 1.1 Declarative sentences
- 1.2 Natural deduction
- 1.2.1 Rules for natural deduction
- 1.2.2 Derived rules
- 1.2.3 Natural deduction in summary
- 1.2.4 Provable equivalence
- 1.2.5 An aside: proof by contradiction
- 1.3 Propositional logic as a formal language
- 1.4 Semantics of propositional logic
- 1.4.1 The meaning of logical connectives
- 1.4.2 Mathematical induction
- 1.4.3 Soundness of propositional logic
- 1.4.4 Completeness of propositional logic
- 1.5 Normal forms
- 1.5.1 Semantic equivalence, satisfiability and validity
- 1.5.2 Conjunctive normal forms and validity
- 1.5.3 Horn clauses and satisfiability
- 1.6 SAT solvers
- 1.6.1 A linear solver
- 1.6.2 A cubic solver
- 1.7 Exercises
- 1.8 Bibliographic notes
- 2. Predicate logic
- 2.1 The need for a richer language
- 2.2 Predicate logic as a formal language
- 2.2.1 Terms
- 2.2.2 Formulas
- 2.2.3 Free and bound variables
- 2.2.4 Substitution
- 2.3 Proof theory of predicate logic
- 2.3.1 Natural deduction rules
- 2.3.2 Quantifier equivalences
- 2.4 Semantics of predicate logic
- 2.4.1 Models
- 2.4.2 Semantic entailment
- 2.4.3 The semantics of equality
- 2.5 Undecidability of predicate logic
- 2.6 Expressiveness of predicate logic
- 2.6.1 Existential second-order logic
- 2.6.2 Universal second-order logic
- 2.7 Micromodels of software
- 2.7.1 State machines
- 2.7.2 Alma – re-visited
- 2.7.3 A software micromodel
- 2.8 Exercises
- 2.9 Bibliographic notes
- 3. Verification by model checking
- 3.1 Motivation for verification
- 3.2 Linear-time temporal logic
- 3.2.1 Syntax of LTL
- 3.2.2 Semantics of LTL
- 3.2.3 Practical patterns of specifications
- 3.2.4 Important equivalences between LTL formulas
- 3.2.5 Adequate sets of connectives for LTL
- 3.3 Model checking: systems, tools, properties
- 3.3.1 Example: mutual exclusion
- 3.3.2 The NuSMV model checker
- 3.3.3 Running NuSMV
- 3.3.4 Mutual exclusion revisited
- 3.3.5 The ferryman
- 3.3.6 The alternating bit protocol
- 3.4 Branching-time logic
- 3.4.1 Syntax of CTL
- 3.4.2 Semantics of CTL
- 3.4.3 Practical patterns of specifications
- 3.4.4 Important equivalences between CTL formulas
- 3.4.5 Adequate sets of CTL connectives
- 3.5 CTL* and the expressive powers of LTL and CTL
- 3.5.1 Boolean combinations of temporal formulas in CTL
- 3.5.2 Past operators in LTL
- 3.6 Model-checking algorithms
- 3.6.1 The CTL model-checking algorithm
- 3.6.2 CTL model checking with fairness
- 3.6.3 The LTL model-checking algorithm
- 3.7 The fixed-point characterisation of CTL
- 3.7.1 Monotone functions
- 3.7.2 The correctness of SATEG
- 3.7.3 The correctness of SATEU
- 3.8 Exercises
- 3.9 Bibliographic notes
- 4. Program verification
- 4.1 Why should we specify and verify code?
- 4.2 A framework for software verification
- 4.2.1 A core programming language
- 4.2.2 Hoare triples
- 4.2.3 Partial and total correctness
- 4.2.4 Program variables and logical variables
- 4.3 Proof calculus for partial correctness
- 4.3.1 Proof rules
- 4.3.2 Proof tableaux
- 4.3.3 A case study: minimal-sum section
- 4.4 Proof calculus for total correctness
- 4.5 Programming by contract
- 4.6 Exercises
- 4.7 Bibliographic notes
- 5. Modal logics and agents
- 5.1 Modes of truth
- 5.2 Basic modal logic
- 5.2.1 Syntax
- 5.2.2 Semantics
- 5.3 Logic engineering
- 5.3.1 The stock of valid formulas
- 5.3.2 Important properties of the accessibility relation
- 5.3.3 Correspondence theory
- 5.3.4 Some modal logics
- 5.4 Natural deduction
- 5.5 Reasoning about knowledge in a multi-agent system
- 5.5.1 Some examples
- 5.5.2 The modal logic KT45n
- 5.5.3 Natural deduction for KT45n
- 5.5.4 Formalising the examples
- 5.6 Exercises
- 5.7 Bibliographic notes
- 6. Binary decision diagrams
- 6.1 Representing boolean functions
- 6.1.1 Propositional formulas and truth tables
- 6.1.2 Binary decision diagrams
- 6.1.3 Ordered BDDs
- 6.2 Algorithms for reduced OBDDs
- 6.2.1 The algorithm reduce
- 6.2.2 The algorithm apply
- 6.2.3 The algorithm restrict
- 6.2.4 The algorithm exists
- 6.2.5 Assessment of OBDDs
- 6.3 Symbolic model checking
- 6.3.1 Representing subsets of the set of states
- 6.3.2 Representing the transition relation
- 6.3.3 Implementing the functions pre∃ and pre∀
- 6.3.4 Synthesising OBDDs
- 6.4 A relational mu-calculus
- 6.4.1 Syntax and semantics
- 6.4.2 Coding CTL models and specifications
- 6.5 Exercises
- 6.6 Bibliographic notes
- 6.1 Representing boolean functions
- Bibliography
- Index
UM RAFBÆKUR Á HEIMKAUP.IS
Bókahillan þín er þitt svæði og þar eru bækurnar þínar geymdar. Þú kemst í bókahilluna þína hvar og hvenær sem er í tölvu eða snjalltæki. Einfalt og þægilegt!Rafbók til eignar
Rafbók til eignar þarf að hlaða niður á þau tæki sem þú vilt nota innan eins árs frá því bókin er keypt.
Þú kemst í bækurnar hvar sem er
Þú getur nálgast allar raf(skóla)bækurnar þínar á einu augabragði, hvar og hvenær sem er í bókahillunni þinni. Engin taska, enginn kyndill og ekkert vesen (hvað þá yfirvigt).
Auðvelt að fletta og leita
Þú getur flakkað milli síðna og kafla eins og þér hentar best og farið beint í ákveðna kafla úr efnisyfirlitinu. Í leitinni finnur þú orð, kafla eða síður í einum smelli.
Glósur og yfirstrikanir
Þú getur auðkennt textabrot með mismunandi litum og skrifað glósur að vild í rafbókina. Þú getur jafnvel séð glósur og yfirstrikanir hjá bekkjarsystkinum og kennara ef þeir leyfa það. Allt á einum stað.
Hvað viltu sjá? / Þú ræður hvernig síðan lítur út
Þú lagar síðuna að þínum þörfum. Stækkaðu eða minnkaðu myndir og texta með multi-level zoom til að sjá síðuna eins og þér hentar best í þínu námi.
Fleiri góðir kostir
- Þú getur prentað síður úr bókinni (innan þeirra marka sem útgefandinn setur)
- Möguleiki á tengingu við annað stafrænt og gagnvirkt efni, svo sem myndbönd eða spurningar úr efninu
- Auðvelt að afrita og líma efni/texta fyrir t.d. heimaverkefni eða ritgerðir
- Styður tækni sem hjálpar nemendum með sjón- eða heyrnarskerðingu
- Gerð : 208
- Höfundur : 6162
- Útgáfuár : 2004
- Leyfi : 379